Safe Concurrent Programming with Sessions and Shared State

Papers

Abstract. Software construction depends on imperative state sharing and concurrency, which are naturally present in several application domains and are also exploited to improve the structure and efficiency of computer programs. However, reasoning about concurrency and shared mutable state is hard, error-prone and the source of many programming bugs, such as memory leaks, data corruption, deadlocks and non-termination. In this thesis, we develop CLASS: a core session-based language with a lightweight substructural type system, that results from a principled extension of the propositions-as- types correspondence with second-order classical linear logic. More concretely, CLASS offers support for session-based communication, mutex-protected first-class reference cells, dynamic state sharing, generic polymorphic algorithms, data abstraction and primitive recursion. CLASS expresses and types significant realistic programs, that manipulate memory- efficient linked data structures (linked lists, binary search trees) with support for updates in-place, shareable concurrent ADTs (counters, stacks, functional and imperative queues), resource synchronisation methods (fork-joins, barriers, dining philosophers, generic core- cursive protocols). All of these examples are guaranteed to be safe, a result that follows by the logical approach. The linear logical foundations guarantee that well-typed CLASS programs do not go wrong: they never deadlock on communication or reference cell acquisition, do not leak memory and always terminate, even if they share complex data structures protected by synchronisation primitives. Furthermore, since we follow a propositions-as-types approach, we can reason about the behaviour of concurrent stateful processes by algebraic program manipulation. The feasibility of our approach is witnessed by the implementation of a type checker and interpreter for CLASS, which validates and guides the development of many realistic programs. The implementation is available with an open-source license, together with several examples.

Safe Session-Based Concurrency with Shared Linear State , Pedro Rocha and Luís Caires
(submitted paper with supplementary material - to appear at ESOP23).

Abstract. We introduce CLASS, a session-typed, higher-order, core language that sup- ports concurrent computation with shared linear state. We believe that CLASS is the first proposal for a foundational language able to flexibly express realistic concurrent programming idioms, with a type system ensuring all the following three key properties: CLASS programs never misuse or leak stateful resources or memory, they never deadlock, and they always terminate. CLASS owes these strong properties to a propositions-as-types foundation based on Linear Logic, which we conservatively extend with logically motivated constructs for shareable affine state. We illustrate CLASS expressiveness with several examples involving memory-efficient linked data structures, sharing of resources with linear usage protocols, and sophisticated thread synchronisation, which may be type-checked with a perhaps surprisingly light type annotation burden.

Abstract. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

Software

• basic examples, including those in the papers
• basic linked data structures (linked lists, binary search trees, queues, ...)
• shareable concurrent mutable ADTs (stacks, queues, dictionaries, ...)
• resource synchronisation (dining philosophers, barriers, fork-join, sharing ADT wrappers, Hoare-style monitiors with conditions, ...)
• System-F style encodings of data types
• several test suites

From version 5.0 up the system supports light type annotations via type inference, the language only requires process definition parameters and cut-bound names to be type annotated, and performs implicit activation of affine and exponential resources.

Download CLASS Implementation v7 (zip) [22NOV22] (Creative Commons License). To build, execute script ./makeit.

Minimum requirements: Java 8 + JavaCC

"Hello World" example: A concurrent inc/reset counter.

type Counter { state lint };;

proc counter(c: Counter){
    cell c(42)
};;

proc reset(c: ~Counter){
    take c(n);
    println("GOT "+n+" and RESET");
    put c(0);
    release c
};;

proc inc(c: ~Counter){
    take c(n);
    println "INC";
    put c(n+1);
    release c
};;

proc main(){
    cut{
        counter(c)
        |c: ~Counter|
        share c {
            inc(c) || reset(c) || inc(c) || reset(c)
        }
}};;