94 citations · 97 across the 4 of their papers we have counts for
7 papers
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…
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
Daniel Wright, Mark Batty, Brijesh Dongol
Deductive verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly…
PrideMM: A Solver for Relaxed Memory Models
Simon Cooksey, Sarah Harris, Mark Batty +2
Relaxed memory models are notoriously delicate. To ease their study, several ad hoc simulators have been developed for axiomatic memory models. We show how axiomatic memory models…
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…