A Rely-Guarantee-Based Simulation for Cooperative Semantics.

Compared to semantics with preemptively executing threads, ones with cooperative threads permit easier specification of atomicity in concurrent programs. We introduce a semantics of cooperative programs, and a simulation notion compatible with rely-guarantee proofs. We prove our simulation composes in parallel and sequentially, and that it can establish a standard trace-based notion of refinement.