Discourje: Runtime Verification of
Communication Protocols in Clojure
Ruben Hamers
1 and Sung-Shik Jongmans
1,2
1 Open University, Heerlen, the Netherlands
2 CWI, Amsterdam, the Netherlands
Abstract. This paper presents Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety
of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a
formal foundation and is itself implemented in Clojure to offer a seamless
specification–implementation experience. Benchmarks show Discourje’s
overhead can be less than 5% for real/existing concurrent programs.
1 Introduction
Background. To take advantage of today’s and tomorrow’s multi-core processors, shared-memory concurrent programming—a notoriously complex enterprise—is becoming increasingly important. To alleviate some of the complexities,
in addition to low-level synchronization 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 (e.g., Go [25],
Rust [42], Clojure [17]). The idea is that, beyond their usage in distributed computing, channels can also serve as a programming abstraction for shared memory,
supposedly less prone to concurrency bugs than locks, semaphores, and the like.
However, in a recent study of 171 concurrency bugs in popular open source Go
programs [48], Tu et al. found that “message passing does not necessarily make
multi-threaded programs less error-prone than shared memory.”
From a programmer’s perspective, a key problem is this: if we already know
which roles (threads), infrastructure (channels between threads), and protocols
(communications through channels) our program should consist of, then how can
we ensure our implementation is indeed safe relative to our specification? Safety
means “bad” channel actions never occur: if a send, receive, or close happens
in the implementation, then it is allowed by the protocol in the specification.
For instance, typical protocols rule out common message-passing concurrency
bugs [48], such as sends without receives, receives without sends, and type mismatches (actual type sent = expected type received). Essentially, thus, we face
a classical verification problem, with classical ingredients: an implementation
language I, a specification language S, and an inclusion relation .
Over the past years, a significant body of research in this area has been based
on multiparty session types (MPST) [27]. The idea is to specify protocols as behavioral types [1,30] against which threads are subsequently type-checked; the
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 266–284, 2020.
https://doi.org/10.1007/978-3-030-45190-5 15
TACAS
Evaluation
Artifact
2020
Accepted
Communication Protocols in Clojure
Ruben Hamers
1 and Sung-Shik Jongmans
1,2
1 Open University, Heerlen, the Netherlands
2 CWI, Amsterdam, the Netherlands
Abstract. This paper presents Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety
of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a
formal foundation and is itself implemented in Clojure to offer a seamless
specification–implementation experience. Benchmarks show Discourje’s
overhead can be less than 5% for real/existing concurrent programs.
1 Introduction
Background. To take advantage of today’s and tomorrow’s multi-core processors, shared-memory concurrent programming—a notoriously complex enterprise—is becoming increasingly important. To alleviate some of the complexities,
in addition to low-level synchronization 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 (e.g., Go [25],
Rust [42], Clojure [17]). The idea is that, beyond their usage in distributed computing, channels can also serve as a programming abstraction for shared memory,
supposedly less prone to concurrency bugs than locks, semaphores, and the like.
However, in a recent study of 171 concurrency bugs in popular open source Go
programs [48], Tu et al. found that “message passing does not necessarily make
multi-threaded programs less error-prone than shared memory.”
From a programmer’s perspective, a key problem is this: if we already know
which roles (threads), infrastructure (channels between threads), and protocols
(communications through channels) our program should consist of, then how can
we ensure our implementation is indeed safe relative to our specification? Safety
means “bad” channel actions never occur: if a send, receive, or close happens
in the implementation, then it is allowed by the protocol in the specification.
For instance, typical protocols rule out common message-passing concurrency
bugs [48], such as sends without receives, receives without sends, and type mismatches (actual type sent = expected type received). Essentially, thus, we face
a classical verification problem, with classical ingredients: an implementation
language I, a specification language S, and an inclusion relation .
Over the past years, a significant body of research in this area has been based
on multiparty session types (MPST) [27]. The idea is to specify protocols as behavioral types [1,30] against which threads are subsequently type-checked; the
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 266–284, 2020.
https://doi.org/10.1007/978-3-030-45190-5 15
TACAS
Evaluation
Artifact
2020
Accepted