TC:Small: Formal Reasoning about Concurrent Programs for Multicore and Multiprocessor Machines

Yale University, New Haven CT

Investigators

Abstract

Formal reasoning about concurrent programs is usually done at a high-level with strong assumptions such as built-in thread primitives (e.g., locks) and simplified memory models (e.g., sequential consistency). Existing formal techniques (including Hoare logic and type system) have consistently ignored important issues such as relaxed memory models, hardware interrupts, implementation of synchronization primitives, and support for software transactional memory and privatization. This severely limits their applicability. This research focuses on extending and adapting existing formal techniques so that they can also support realistic low-level concurrent programs running on modern multicore and multiprocessor machines. The PI is developing a new operational approach for reasoning about programs running under relaxed memory models; designing new program logics for certifying both weak and strong memory operations (including the memory-fence and compare-and-swap instructions); and showing how to scale his approach to real-world thread implementation and to machines with relaxed memory models. If successful, this research will help improve the reliability of concurrent software components, which form the backbone of many critical systems in the world. It will also facilitate the community-wide effort for finding new programming models for safe and scalable multicore computing.