Discourje: Runtime Verification of Communication Protocols in Clojure
281
by MPST, and verify the implementation against the specification using deductive verification tools (VCC [18] and Why3 [21]). However, this approach does
not support push-button verification: considerable manual effort is required. In
contrast, our approach is fully automated.
We are aware of only two other works that use formal techniques to reason
about Clojure programs: Bonnaire-Sergeant et al. [6] formalized the optional type
system for Clojure and proved soundness, while Pinzaru et al. [41] developed a
translation from Clojure to Boogie [2] to verify Clojure programs annotated with
pre/post-conditions. Ours is the first paper that targets concurrency in Clojure.
Verification of shared-memory concurrency with channels has received attention in the context of Go [40,32,33,45]. However, emphasis in these works is
on checking deadlock-freedom, liveness, and generic safety properties, while we
focus on program-specific protocol compliance. Castro et al. [14] also consider
protocol compliance, but their specification language (of global types) is less
expressive than ours and does not support this paper’s examples.
7 Conclusion
We presented Discourje: a runtime verification framework for channel-based communication protocols in Clojure. Discourje is based on a projection-free interpretation of multiparty session types, trading static type-checking for dynamic
runtime monitoring to alleviate expressiveness issues. A key design principle of
Discourje has been ergonomics: we aim to make Discourje’s use as comfortable
as possible. Specifically, programmers can decide to start using Discourje at any
stage of development (and doing so requires little effort); Discourje is itself implemented in Clojure (so no need to use a different IDE, learn completely new syntax, or install special compilers); and Discourje can be used seamlessly alongside
other concurrency libraries. The framework has a formal foundation, and benchmarks indicate that monitoring overhead can be less than 5% for real/existing
concurrent programs. This makes Discourje suitable both as a testing/debugging
tool in development, and as a fail-safe mechanism in production.
We list two interesting avenues for future work. First, we want to refine our
lock-free synchronization algorithm to enhance the way parallel composition is
handled. Second, a much more profound extension pertains to feedback and recovery. Specifically, we want to explore the idea that whenever a monitor detects
a violation, instead of throwing an exception, it should simply delay the violating action as a corrective measure, in an attempt to steer the implementation
toward safe behavior. When done naively, such delays can easily yield deadlocks,
so our plan is to combine this with runtime model-checking/reachability analysis
to check if eventually, the violating action is allowed (if yes, delay; if no, throw).
Acknowledgments. Funded by the Netherlands Organisation of Scientific Research (NWO): 016.Veni.192.103. This work was carried out on the Dutch national e-infrastructure with the support of SURF Cooperative.
281
by MPST, and verify the implementation against the specification using deductive verification tools (VCC [18] and Why3 [21]). However, this approach does
not support push-button verification: considerable manual effort is required. In
contrast, our approach is fully automated.
We are aware of only two other works that use formal techniques to reason
about Clojure programs: Bonnaire-Sergeant et al. [6] formalized the optional type
system for Clojure and proved soundness, while Pinzaru et al. [41] developed a
translation from Clojure to Boogie [2] to verify Clojure programs annotated with
pre/post-conditions. Ours is the first paper that targets concurrency in Clojure.
Verification of shared-memory concurrency with channels has received attention in the context of Go [40,32,33,45]. However, emphasis in these works is
on checking deadlock-freedom, liveness, and generic safety properties, while we
focus on program-specific protocol compliance. Castro et al. [14] also consider
protocol compliance, but their specification language (of global types) is less
expressive than ours and does not support this paper’s examples.
7 Conclusion
We presented Discourje: a runtime verification framework for channel-based communication protocols in Clojure. Discourje is based on a projection-free interpretation of multiparty session types, trading static type-checking for dynamic
runtime monitoring to alleviate expressiveness issues. A key design principle of
Discourje has been ergonomics: we aim to make Discourje’s use as comfortable
as possible. Specifically, programmers can decide to start using Discourje at any
stage of development (and doing so requires little effort); Discourje is itself implemented in Clojure (so no need to use a different IDE, learn completely new syntax, or install special compilers); and Discourje can be used seamlessly alongside
other concurrency libraries. The framework has a formal foundation, and benchmarks indicate that monitoring overhead can be less than 5% for real/existing
concurrent programs. This makes Discourje suitable both as a testing/debugging
tool in development, and as a fail-safe mechanism in production.
We list two interesting avenues for future work. First, we want to refine our
lock-free synchronization algorithm to enhance the way parallel composition is
handled. Second, a much more profound extension pertains to feedback and recovery. Specifically, we want to explore the idea that whenever a monitor detects
a violation, instead of throwing an exception, it should simply delay the violating action as a corrective measure, in an attempt to steer the implementation
toward safe behavior. When done naively, such delays can easily yield deadlocks,
so our plan is to combine this with runtime model-checking/reachability analysis
to check if eventually, the violating action is allowed (if yes, delay; if no, throw).
Acknowledgments. Funded by the Netherlands Organisation of Scientific Research (NWO): 016.Veni.192.103. This work was carried out on the Dutch national e-infrastructure with the support of SURF Cooperative.