Episodic Loops: Finitary Event Structures and Operational Semantics for C11 Programs with Retries

Christian Kissig, Jay Richards, Mark Batty

Lock-free synchronisation algorithms are often implemented with fallible operations, such as compare-and-swap (CAS), wrapped in unbounded retry loops. Verifying such algorithms req…