Discourje
The Discourje project aims to help programmers cope with channels and concurrency bugs in Clojure programs (that use core.async
), based on dynamic analysis. The idea is that programmers write not only implementations of communication protocols in their Clojure programs, but also specifications. Discourje then offers a run-time verification library to ensure that channel actions in implementations are safe relative to specifications.
Rationale
Back in 2015 I decided to take on the challenge of getting a Master’s degree. I was already working full-time and thus I needed to find a University that allowed part-time study all from the comfort of your home. I found this university called Open Universiteit in The Netherlands. They have been focused on remote learning ever since they started. Luckily they also have a Computer Science degree, even one of the best ones and highest graded ones in the country!
So I enrolled in the Master Software Engineering and as with any degree, you end it with a thesis. I chose to write my thesis about so called “protocol languages”. Protocol languages are domain specific languages to express communication flow. This way you can separate the logic form the communication protocol. These languages became somewhat popular during the 90s when all of the sudden, “old” software needed to be connected to the internet. Now all this software needed to communicate with each other and thus all kinds of middle-ware were invented. Such middle-ware often provided users with DSL’s to express the communication flows, in a textual format or even visually like MSBizTalk.
But these languages can be used on a lower level of abstraction too. Concurrent entities can mean many things, even individual threads. So, for my thesis I chose to write a protocol language that focused on these lower levels of abstraction. I’ve always been fascinated with concurrency and parallelism. There’s just so much locked (pun intended) potential in a program when it’s not used or implemented poorly. And even when implemented correctly, things can mess up.
I remember reading the book “Java Concurrency, by Brian Goetz”. I think somewhere in chapter 2 he talks about the implementation of BigInteger. He talks about how BigInt is simply 2 normal integers under the hood. And thus, when you manipulate it concurrently, you might actually have changed 1 underlying int, but not the other. Thus you end up with all kinds of very intricate locking mechanisms, which are fun when you write them but not when you need to explain them or refactor them a month later.
But by recognizing this can be done better I chose my subject to be on concurrency, parallelism and protocol languages.
The professor I talked to about my probable thesis project explained how he was using and instrumenting Java to add special kinds of analysis to for example formally prove concurrent communication protocols. This was also fascinating to me but I quickly suggested we should take a look at Clojure, and fortunately he agreed.
Clojure is a language fully oriented towards data-driven programming and designed with concurrency and parallelism in mind. It’s a functional language based on a LISP syntax. I will save you my enthusiasm for the Clojure language but, I still think it’s my all-time favorite language to write code in (, so there you go).
Thus we set out to define a cool thesis subject and project for my graduation and came up with the following. A common thread (hA!) in modern protocol languages is that they are dependent on a specific IDE e.g. eclipse. Researchers tend to write special plugins for IDE’s to add extra compilation or static analysis steps for example. This makes such languages bound to one specific IDE, which can break the end user’s devcycle / environment. Also, these protocol languages require the programmer to learn a new language. It’s a DSL so the language is rather minimal, but still, they need to learn a new language which can be a threshold just too high for some. And the last thing I want to mention, and one I hinted at before, is that protocol languages often involve additional compilation steps, which will impact modern CI/CD pipelines.
The main goal of my protocol language was to improve the usability of such language by fully integrating it into the language. Fortunately, Clojure allows all of this. By using Clojure’s excellent Macro system we were able to extend the language with our communication constructs. This leads to devs not needing to learn a new language, no use custom of compilers, and no additional compilation steps. It’s all built-in natively into the language 🙂 I can talk about this for hours but I’m going to refer you to a couple of video’s and research papers that spawned after my thesis was done. You can read them below! Have fun!
Resources
Suggested resources to get an overview of Discourje: talk 2 and/or paper 1.
Talks
-
Sung-Shik Jongmans. Automated Correctness Analysis for core.async. Dutch Clojure Days (DCD), 2022.
-
Sung-Shik Jongmans. Automated Correctness Analysis for core.async. Clojure conference in Germany (:clojureD), 2022. [link]
-
Sung-Shik Jongmans. dcj-lint: Analysis of Specifications of Multiparty Sessions. ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2021. [link]
-
Sung-Shik Jongmans. Discourje: Runtime Verification of Communication Protocols in Clojure. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2020. [link]
-
Ruben Hamers. Discourje: Automatically validated message exchange patterns in Clojure. Dutch Clojure Day (DCD), 2019. [link]
Papers
-
Ruben Hamers, Erik Horlings, and Sung-Shik Jongmans. The Discourje Project: Run-Time Verification of Communication Protocols in Clojure. International Journal on Software Tools for Technology Transfer, 2022. [link, pdf]
-
Erik Horlings and Sung-Shik Jongmans. dcj-lint: Analysis of Specifications of Multiparty Sessions. Proceedings of ESEC/FSE’21. [link, pdf]
-
Ruben Hamers and Sung-Shik Jongmans. Discourje: Runtime Verification of Communication Protocols in Clojure. Proceedings of TACAS’20. [link, pdf]