SHF: Small: Separation Principles for Concurrent Programs: Semantics, Logics, and Methodology

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Concurrent programs are widely used, in real-world applications with safety-critical requirements, so it is vital to ensure their correctness. Such programs are difficult to get right and hard to analyze, because of the huge number of ways in which concurrent threads may interact dynamically. We need to guarantee that program behavior is free of race conditions, such as concurrent attempts to update the same piece of state, since racy programs may behave erratically. Further, programs that operate on mutable data structures are prone to safety faults, such as attempts to access a previously deallocated pointer, and this is a leading cause of crashes in operating system code. This project addresses these concerns by building a theory of concurrency based on resource separation principles. This theory will offer resource-sensitive logics for program correctness, with solid semantic foundations. The project will significantly expand the scope of the author's work on concurrent separation logic, to encompass a wider range of program properties and concurrency paradigms, and combine concurrency with procedures. The project will introduce semantic models and logics for networks of communicating processes, based on a principle of channel separation. The intellectual merits of this proposal include the development of a unifying framework of semantic models and methodologies, with rigorous mathematical and logical underpinnings, embodying practically useful principles. In the broader setting this project aims to improve the state-of-the-art in programming methodology, facilitate the writing of reliable concurrent code, and enable formal reasoning about a wider range of problems. The project will contribute to general understanding, by informing the design of new logics, and the discovery of proof techniques, that cross paradigm barriers. The project will foster the development of improved semantically-based analysis tools for concurrent programs, to be made available for widespread use and experimentation, and to be used for real-world safety-critical applications in which concurrency is both a feature and a problem.