Abstract

This paper proposes a new type system for concurrent pro- grams, allowing threads to exchange complex object graphs without risking destructive data races. While this goal is shared by a rich history of past work, existing solutions ei- ther rely on strictly enforced heap invariants that prohibit natural programming patterns or demand pervasive annota- tions even for simple programming tasks. As a result, past systems cannot express intuitively simple code without un- natural rewrites or substantial annotation burdens. Our work avoids these pitfalls through a novel type system that pro- vides sound reasoning about separation in the heap while remaining flexible enough to support a wide range of desir- able heap manipulations. This new sweet spot is attained by enforcing a heap domination invariant similarly to prior work, but tempering it by allowing complex exceptions that add little annotation burden. Our results include: (1) code examples showing that common data structure manipula- tions which are difficult or impossible to express in prior work are natural and direct in our system, (2) a formal proof of correctness demonstrating that well-typed programs can- not encounter destructive data races at run time, and (3) an efficient type checker implemented in Gallina and OCaml.

Read in full here:

https://www.cs.cornell.edu/andru/papers/gallifrey-types/

This thread was posted by one of our members via one of our news source trackers.