P4214R0 — Composable Correctness and Progress Guarantees
SG1
Correctness is usually harder to discuss than the individual properties from which it is built. Following Lamport’s division of correctness into safety and liveness [[Lamport77]](https://lamport.azurewebsites.net/pubs/proving.pdf), this paper argues that C++ standardization should treat progress guarantees as part of the correctness contract of concurrency facilities.