A Type System for Race-free and Memory-safe Multithreading Using Region Hierarchies

A current challenge for programming language research is to design and implement multithreaded low-level languages providing static guarantees for memory safety and freedom from data races. Towards this goal, in this paper we present such a language and its type system. Our language guarantees memory safety by employing region-based memory management. Unlike other similar languages employing regions, our regions are organized in a hierarchical manner so that each region is owned by a single parent region and may contain multiple children regions. This structure imposes constraints over region capability manipulation. In this setting, we allow early region deallocation and thus overcome the restrictions of LIFO region lifetimes. Our type system combines fractional, aliasable capabilities and hierarchy abstraction in a multithreaded setting. Regions may remain thread-local, migrate to another thread or become shared between threads. Implicit locks are used to protect each region from data races. Both lock and region capabilities are treated uniformly. Locking also follows a hierarchical scheme as a parent lock subsumes children locks