Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project

Sung-Shik Jongmans, R. (Ruben) Hamers

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation:
Subtitle of host publication Verification Principles
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer Nature Switzerland AG
Pages489-508
Number of pages10
ISBN (Electronic)978-3-030-61362-4
ISBN (Print)978-3-030-61361-7
DOIs
Publication statusPublished - 2020
Event9th International Symposium on Leveraging Applications of Formal Methods - Online, Rhodes, Greece
Duration: 20 Oct 202030 Oct 2020

Publication series

SeriesLecture Notes in Computer Science
ISSN0302-9743

Symposium

Symposium9th International Symposium on Leveraging Applications of Formal Methods
Abbreviated titleISoLA 2020
CountryGreece
CityRhodes
Period20/10/2030/10/20

Fingerprint Dive into the research topics of 'Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project'. Together they form a unique fingerprint.

Cite this