Christian Kissig

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

Lock-free synchronisation algorithms are often implemented with fallible operations, such as compare-and-swap (CAS), wrapped in unbounded retry loops. Verifying such algorithms requires considering arbitrarily many failing iterations, yielding large state spaces, compounded by the interleavings of concurrent threads. P...