Abstract
To simplify shared-memory concurrent programming, in addition to low-level synchronisation primitives, several modern programming languages have started to offer core support for higher-level communication primitives as well, in the guise of message passing through channels. Yet, a growing body of evidence suggests that channel-based programming abstractions for shared memory also have their issues.
The Discourje project aims to help programmers cope with message-passing concurrency bugs in Clojure programs, based on run-time verification and dynamic monitoring. The idea is that programmers write not only implementations, but also specifications (of sessions of channel actions). Discourje then offers a library to ensure that implementations run safely relative to specifications (= “bad” channel actions never happen).
This paper gives a tour of the current state of Discourje, by example; it is intended to serve both as a general overview for readers who are unfamiliar with previous work on Discourje, and as an introduction to new features for readers who are familiar.
The Discourje project aims to help programmers cope with message-passing concurrency bugs in Clojure programs, based on run-time verification and dynamic monitoring. The idea is that programmers write not only implementations, but also specifications (of sessions of channel actions). Discourje then offers a library to ensure that implementations run safely relative to specifications (= “bad” channel actions never happen).
This paper gives a tour of the current state of Discourje, by example; it is intended to serve both as a general overview for readers who are unfamiliar with previous work on Discourje, and as an introduction to new features for readers who are familiar.
| Original language | English |
|---|---|
| Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation: |
| Subtitle of host publication | Verification Principles |
| Editors | Tiziana Margaria, Bernhard Steffen |
| Place of Publication | Cham |
| Publisher | Springer Nature Switzerland AG |
| Pages | 489-508 |
| Number of pages | 10 |
| ISBN (Electronic) | 978-3-030-61362-4 |
| ISBN (Print) | 978-3-030-61361-7 |
| DOIs | |
| Publication status | Published - 2020 |
| Event | 9th International Symposium on Leveraging Applications of Formal Methods - Online, Rhodes, Greece Duration: 20 Oct 2020 → 30 Oct 2020 |
Publication series
| Series | Lecture Notes in Computer Science |
|---|---|
| ISSN | 0302-9743 |
Symposium
| Symposium | 9th International Symposium on Leveraging Applications of Formal Methods |
|---|---|
| Abbreviated title | ISoLA 2020 |
| Country/Territory | Greece |
| City | Rhodes |
| Period | 20/10/20 → 30/10/20 |