94 citations · 97 across the 4 of their papers we have counts for
5 papers · 1 filter
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…
Spegion: Implicit and Non-Lexical Regions with Sized Allocations
Jack Hughes, Michael Vollmer, Mark Batty
Region based memory management is a powerful tool designed with the goal of ensuring memory safety statically. The region calculus of Tofte and Talpin is a well known example of a…
Memory Consistency and Program Transformations
Akshay Gopalakrishnan, Clark Verbrugge, Mark Batty
A memory consistency model specifies the allowed behaviors of shared memory concurrent programs. At the language level, these models are known to have a non-trivial impact on the s…
Compositional Verification of Compiler Optimisations on Relaxed Memory
Mike Dodds, Mark Batty, Alexey Gotsman
A valid compiler optimisation transforms a block in a program without introducing new observable behaviours to the program as a whole. Deciding which optimisations are valid can be…
Overhauling SC Atomics in C11 and OpenCL
Mark Batty, Alastair F. Donaldson, John Wickerson
Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convolu…