Detail

The Type Discipline of Behavioral Separation

We introduce the concept of *behavioral separation* as a general
principle for disciplining interference in higher-order imperative
concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives.

Behavioral separation builds on notions originally introduced for
behavioral type systems and separation logics, but shifts the focus
from the separation of static program state properties towards the
separation of dynamic usage behaviors of runtime values. Behavioral
separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexibility.

We illustrate how our type system, even if based on a small set of
general primitives, is already able to tackle fairly challenging
program idioms, involving aliasing at various types, concurrency with
first-class threads, manipulation of linked data structures,
behavioral borrowing, and invariant-based separation.

Luís Caires (joint work with João C. Seco)