2020-10-29
Safe sessions of channel actions in Clojure: A tour of the Discourje Project
Publication
Publication
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.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-030-61362-4_28 | |
| Lecture Notes in Computer Science | |
| International Symposium on Leveraging Applications of Formal Methods | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Hamers, R, & Jongmans, S.-S.T.Q. (2020). Safe sessions of channel actions in Clojure: A tour of the Discourje Project. In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (pp. 489–508). doi:10.1007/978-3-030-61362-4_28
|
|
