268
R. Hamers and S.-S. Jongmans
Contributions. To simplify shared-memory concurrent programming in languages with channels, we aim to consolidate strengths #1 and #2 (page 267),
but alleviate MPST’s expressiveness issues. Specifically, this paper is founded on
two tenets that depart from existing work in significant ways (Fig. 2).
First, we exploit the fact that in our context, channels serve “merely” as programming abstractions for shared memory; there is no distribution whatsoever.
Thus, whereas MPST-based verification for distributed computing requires projection, this is not the case in our setting, opening the door to fully automated
projection-free MPST and eliminating a significant source of restrictions.
Second, instead of adopting MPST-based verification through static typechecking at compile-time, we explore MPST-based verification through dynamic
monitoring at run-time. This enables soundness and completeness, while it also
supports value-dependent protocols in a generally implementable way (i.e., we are
not aware of a mainstream GPL that does not support our monitoring approach).
In this paper, we present our practical embodiment of these ideas: Discourje
(pronounced “discourse”), a runtime verification framework for communication
protocols in Clojure [17,26]. Discourje consists of two components: a DSL to specify protocols and construct monitors, and an API to implement protocols (supplementing Clojure) and add instrumentation. While we could have developed
this framework for any language with channel-based programming abstractions,
including Go and Rust, Clojure is particularly interesting, because: (1) Clojure
has a powerful macro system that enabled us to develop the Discourje DSL as
an extension to Clojure, thereby offering programmers a seamless specification–
implementation experience; (2) contrasting Go and Rust, Clojure is not a systems language but an applications language, so runtime verification overheads
might be more tolerable. We summarize our contributions as follows:
– Overview (Sect. 2): Discourje guarantees safety of protocol implementations, it provides freedom from data races in pure Clojure, and it is more
expressive than existing MPST tools, as demonstrated through examples.
– Design (Sect. 3): We developed core calculi, including operational semantics,
for Clojure and the Discourje DSL as a theoretical foundation.
– Implementation (Sect. 4): We implemented Discourje fully in Clojure. The
Discourje DSL comprises Clojure macros, while the Discourje API is a wrapper around Clojure functions to add instrumentation, non-invasively.
– Evaluation (Sect. 5): Through benchmarks, we show that Discourje’s overhead can be less than 5% for real/existing concurrent programs.
Our artifact is available at https://github.com/discourje.
2 Overview
Clojure (in a nutshell). Clojure [17,26] is a general-purpose, impure functional language that compiles to Java bytecode. As a dialect of Lisp, Clojure follows the code-as-data philosophy, provides a powerful macro system, and adopts
R. Hamers and S.-S. Jongmans
Contributions. To simplify shared-memory concurrent programming in languages with channels, we aim to consolidate strengths #1 and #2 (page 267),
but alleviate MPST’s expressiveness issues. Specifically, this paper is founded on
two tenets that depart from existing work in significant ways (Fig. 2).
First, we exploit the fact that in our context, channels serve “merely” as programming abstractions for shared memory; there is no distribution whatsoever.
Thus, whereas MPST-based verification for distributed computing requires projection, this is not the case in our setting, opening the door to fully automated
projection-free MPST and eliminating a significant source of restrictions.
Second, instead of adopting MPST-based verification through static typechecking at compile-time, we explore MPST-based verification through dynamic
monitoring at run-time. This enables soundness and completeness, while it also
supports value-dependent protocols in a generally implementable way (i.e., we are
not aware of a mainstream GPL that does not support our monitoring approach).
In this paper, we present our practical embodiment of these ideas: Discourje
(pronounced “discourse”), a runtime verification framework for communication
protocols in Clojure [17,26]. Discourje consists of two components: a DSL to specify protocols and construct monitors, and an API to implement protocols (supplementing Clojure) and add instrumentation. While we could have developed
this framework for any language with channel-based programming abstractions,
including Go and Rust, Clojure is particularly interesting, because: (1) Clojure
has a powerful macro system that enabled us to develop the Discourje DSL as
an extension to Clojure, thereby offering programmers a seamless specification–
implementation experience; (2) contrasting Go and Rust, Clojure is not a systems language but an applications language, so runtime verification overheads
might be more tolerable. We summarize our contributions as follows:
– Overview (Sect. 2): Discourje guarantees safety of protocol implementations, it provides freedom from data races in pure Clojure, and it is more
expressive than existing MPST tools, as demonstrated through examples.
– Design (Sect. 3): We developed core calculi, including operational semantics,
for Clojure and the Discourje DSL as a theoretical foundation.
– Implementation (Sect. 4): We implemented Discourje fully in Clojure. The
Discourje DSL comprises Clojure macros, while the Discourje API is a wrapper around Clojure functions to add instrumentation, non-invasively.
– Evaluation (Sect. 5): Through benchmarks, we show that Discourje’s overhead can be less than 5% for real/existing concurrent programs.
Our artifact is available at https://github.com/discourje.
2 Overview
Clojure (in a nutshell). Clojure [17,26] is a general-purpose, impure functional language that compiles to Java bytecode. As a dialect of Lisp, Clojure follows the code-as-data philosophy, provides a powerful macro system, and adopts