I’ll present the first stages of an investigation into how simple we can get away with making the foundations of modular correctness reasoning for shared-memory concurrent programs. Today’s most popular tools for this problem are program logics, but we adopt a different approach, within the Coq proof assistant. Namely, as the core of the framework, we define a simple instrumented operational semantics with one kind of ghost state: monitors, a kind of process that observes execution and enforces adherence to a protocol. On that foundation, we develop some “opt-in” machinery in service of proving stylized correctness theorems. We define connectives and rules for deriving correctness of programs. With our Coq implementation, we have verified a Treiber lock-free stack and a Harris-Michael lock-free set, as well as client programs, proved mostly automatically and parametrically in implementation details of the data structures.

This is joint work with C.J. Bell, Mohsen Lesani, Gregory Malecha, Stephan Boyer, and Peng Wang.