94 citations · 138 across the 11 of their papers we have counts for
11 papers
A High-level Synthesis Toolchain for the Julia Language
Benedict Short, Ian McInerney, John Wickerson
With the push towards Exascale computing and data-driven methods, problem sizes have increased dramatically, increasing the computational requirements of the underlying algorithms.…
Hardware.jl - An MLIR-based Julia HLS Flow (Work in Progress)
Benedict Short, Ian McInerney, John Wickerson
Co-developing scientific algorithms and hardware accelerators requires domain-specific knowledge and large engineering resources. This leads to a slow development pace and high pro…
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…
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version)
Azalea Raad, Ori Lahav, John Wickerson +2
Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of b…
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav +2
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about…
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-…
ARCHITECT: Arbitrary-precision Hardware with Digit Elision for Efficient Iterative Compute
He Li, James J. Davis, John Wickerson +1
Many algorithms feature an iterative loop that converges to the result of interest. The numerical operations in such algorithms are generally implemented using finite-precision ari…
The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
Nathan Chong, Tyler Sorensen, John Wickerson
Weak memory models provide a complex, system-centric semantics for concurrent programs, while transactional memory (TM) provides a simpler, programmer-centric semantics. Both have…
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…