A Rust-like Type System for Cooperative Threads

EasyChair Preprint 8434

Abstract

Rust is a multi-paradigm, low-level, well-typed and a static programming language that focuses on software for a safety and performance. The current design of Rust allows secure memory management without the need for garbage collection. This is met in view of the notions of ownership, borrowing and lifetime. It therefore eliminates runtime bugs due to poor memory management. This feature is advantageous for the development of operating systems, and especially for the development of embedded operating systems, where recovery and debugging are particularly difficult. Even for concurrent programming, Rust provides memory security between threads. The type system provides powerful means to achieve this goal. Specifically, the use of synchronization mechanisms to safely mutate a shared value between threads. However, in a cooperative context, the use of these mechanisms is not obvious. For this purpose, we present MSSL, a memory safe synchronous language close to Rust at the source level. This presentation introduces a new extension, Trc, which allows safe memory sharing between threads not having the need to the use of synchronization mechanisms. Moreover, MSSL offers a cooperate construct that does not exist in Rust. This construct adds the notion of logical instant to our language. Our type system is able to ensure the properties of Trc through a flow-sensitive substructural typing judgment for which we prove syntactic type and borrow safety between threads-safe using progression and preservation.

Keyphrases: Cooperative Scheduling, Rust, memory safety, reactive programming

@booklet{EasyChair:8434,
  author    = {Darine Rammal and Wadoud Bousdira and Frédéric Dabrowski},
  title     = {A Rust-like Type System for Cooperative Threads},
  howpublished = {EasyChair Preprint 8434},
  year      = {EasyChair, 2022}}