SHF: Medium: Formal Analysis of Concurrent Software on Relaxed Memory Models

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

Programmers are increasingly designing concurrent software to effectively harness the computational power of multi-processor and multi-core architectures. Writing correct concurrent software is challenging, and system-specific concurrency libraries are particularly vulnerable in that they are affected by the subtle and complex rules governing the relationship among reads and writes to shared memory in multi-processor systems. The goal of this project is to develop technology that will assist programmers in building high-performance and correct system-level concurrent software with respect to precise modeling of the essential details of the underlying architecture. The investigators will explore specifications for accurate machine-readable descriptions of experimental and commercial memory models in both constraint-based and operational styles. To allow developers to understand subtleties of specific memory models, this project will investigate algorithms and tools for checking equivalence between two specifications and for automatically generating test programs that exhibit the differences. Tools for verifying concurrency libraries with respect to memory model specifications and for automatic insertion of memory ordering fences, will be developed and evaluated on lock-free implementations of commonly used data structures. The proposed research will be integrated in a new upper-level course on multiprocessor programming.