Thread and Memory-Safe Programming with CLASS

TL;DR

This paper introduces CLASS, a linear programming language that guarantees thread safety, memory safety, deadlock freedom, and termination through an expressive type system based on Linear Logic, demonstrated with practical concurrent programming examples.

Contribution

It presents a practical implementation of a linear language with strong safety guarantees, bridging theoretical foundations and real-world concurrent programming applications.

Findings

Ensures no resource misuse or memory leaks

Guarantees deadlock freedom and termination

Supports complex concurrent programming patterns

Abstract

CLASS is a proof-of-concept general purpose linear programming language, flexibly supporting realistic concurrent programming idioms, and featuring an expressive linear type system ensuring that programs (1) never misuse or leak stateful resources or memory, (2) never deadlock, and (3) always terminate. The design of CLASS and the strong static guarantees of its type system originates in its Linear Logic and proposition-as-types foundations. However, instead of focusing on its theoretical foundations, this paper briefly illustrates, in a tutorial form, an identifiable CLASS session-based programming style where strong correctness properties are automatically ensured by type-checking. Our more challenging examples include concurrent thread and memory-safe mutable ADTs, lazy stream programming, and manipulation of linear digital assets as used in smart contracts.