Scalable reasoning about complex concurrent programs interacting with shared memory is a fundamental, open research problem. Developers manage the complexity of concurrent software systems by designing software components that are compositional and modular. With compositionality, a developer designs local subcomponents with well-understood interfaces that connect to the rest of the system. With modularity, a developer designs reusable subcomponents with abstract software interfaces that can hide the complexity of the subcomponents from the rest of the system. The challenge is to develop compositional, modular reasoning of concurrent programs, which follows the intuitions of the developer in how to structure their software components with precisely defined specifications of software interfaces. These specifications should not leak implementation details and should be expressed at the level of abstraction of the client. I will describe the work done by my group and others on compositional and modular reasoning about concurrent programs using modern concurrent separation logics. I will present work on reasoning about safety properties, highlighting the CAP logic [ECOOP'10] which introduced logical abstraction (the fiction of separation) to concurrent separation logics and the TaDA logic [ECOOP'14] which introduced abstract atomicity (the fiction of atomicity). I will also present new work on progress properties, introducing the TaDA-Live logic for reasoning about the termination of blocking programs. I will demonstrate the subtlety of the reasoning using a simple lock module, and also compare this work with linearizability, contextual refinement and other concurrent separation logics.
展开▼
