Static Safety Guarantees for a Low-level Multithreaded Language with Regions

We present the design of a formal low-level multithreaded language with advanced region-based memory management and thread synchronization primitives, where well-typed programs are memory safe and race free. In our language, regions and locks are combined in a single hierarchy and are subject to uniform ownership constraints imposed by this hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is read/write-protected, then its sub-regions inherit the same access rights. We discuss aspects of the integration and implementation of the formal language within Cyclone and eval-uate the performance of code produced by the modified Cyclone compiler against highly optimized C programs using pthreads. Our results show that the perfor-mance overhead for guaranteed race freedom and memory safety is in most cases acceptable