41 citations · 93 across the 15 of their papers we have counts for
15 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…
Do Your Cores Play Nicely? A Portable Framework for Multi-core Interference Tuning and Analysis
Dan Iorga, Tyler Sorensen, Alastair F. Donaldson
Multi-core architectures can be leveraged to allow independent processes to run in parallel. However, due to resources shared across cores, such as caches, distinct processes may i…
Cooperative Kernels: GPU Multitasking for Blocking Algorithms (Extended Version)
Tyler Sorensen, Hugues Evrard, Alastair F. Donaldson
There is growing interest in accelerating irregular data-parallel algorithms on GPUs. These algorithms are typically blocking, so they require fair scheduling. But GPU programming…
Implementing and Evaluating Candidate-Based Invariant Generation
Adam Betts, Nathan Chong, Pantazis Deligiannis +2
The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions to inductive invariant generation are inflexible, only a…
Integrating a large-scale testing campaign in the CK framework
Andrei Lascu, Alastair F. Donaldson
We consider the problem of conducting large experimental campaigns in programming languages research. Most research efforts require a certain level of bookkeeping of results. This…
Certified Roundoff Error Bounds Using Semidefinite Programming
Victor Magron, George Constantinides, Alastair Donaldson
Roundoff errors cannot be avoided when implementing numerical programs with finite precision. The ability to reason about rounding is especially important if one wants to explore a…
Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
Alastair F. Donaldson, Vasco T. Vasconcelos
This volume contains the post-proceedings of PLACES 2014, the seventh Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, which was held…
PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs
Riyadh Baghdadi, Albert Cohen, Serge Guelton +9
We motivate the design and implementation of a platform-neutral compute intermediate language (PENCIL) for productive and performance-portable accelerator programming.
Automatic Verification of Message-Based Device Drivers
Sidney Amani, Peter Chubb, Alastair F. Donaldson +3
We develop a practical solution to the problem of automatic verification of the interface between device drivers and the OS. Our solution relies on a combination of improved driver…
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report)
Alastair Donaldson, Alexander Kaiser, Daniel Kroening +1
Predicate abstraction is a key enabling technology for applying finite-state model checkers to programs written in mainstream languages. It has been used very successfully for debu…