11 citations · 39 across the 8 of their papers we have counts for
11 papers
Formalising CXL Cache Coherence
Chengsong Tan, Alastair F. Donaldson, John Wickerson
We report our experience formally modelling and verifying CXL.cache, the inter-device cache coherence protocol of the Compute Express Link standard. We have used the Isabelle proof…
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
Luke Geeson, James Brotherston, Wilco Dijkstra +4
The correctness of complex software depends on the correctness of both the source code and the compilers that generate corresponding binary code. Compilers must do more than preser…
Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis +2
Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency m…
Specifying and Testing GPU Workgroup Progress Models
Tyler Sorensen, Lucas F. Salvador, Harmit Raval +4
As GPU availability has increased and programming support has matured, a wider variety of applications are being ported to these platforms. Many parallel applications contain fine-…
A report on the first virtual PLDI conference
Alastair F. Donaldson
This is a report on the PLDI 2020 conference, for which I was General Chair, which was held virtually for the first time as a result of the COVID-19 pandemic. The report contains:…
A Systematic Impact Study for Fuzzer-Found Compiler Bugs
Michaël Marcozzi, Qiyi Tang, Alastair F. Donaldson +1
Despite much recent interest in compiler randomized testing (fuzzing), the practical impact of fuzzer-found compiler bugs on real-world applications has barely been assessed. We pr…