22 citations · 44 across the 9 of their papers we have counts for
7 papers · 1 filter
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
Robert J. Colvin, Ian J. Hayes, Scott Heiner +3
Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A partic…
Parallelized sequential composition, pipelines, and hardware weak memory models
Robert J. Colvin
Since the introduction of the CDC 6600 in 1965 and its `scoreboarding' technique processors have not (necessarily) executed instructions in program order. Programmers of high-level…
A high-level operational semantics for hardware weak memory models
Robert J. Colvin, Graeme Smith
Modern processors deploy a variety of weak memory models, which for efficiency reasons may execute instructions in an order different to that specified by the program text. The con…
A sound and complete definition of linearizability on weak memory models
Graeme Smith, Kirsten Winter, Robert J. Colvin
Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory m…
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter +1
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, i…
An algebra of synchronous atomic steps
Ian J. Hayes, Robert Colvin, Larissa Meinicke +2
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, i…