22 citations · 44 across the 9 of their papers we have counts for
11 papers
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…
Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model (extended version)
Robert J. Colvin
The C/C++ memory model provides an interface and execution model for programmers of concurrent (shared-variable) code. It provides a range of mechanisms that abstract from underlyi…
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…
An abstract semantics of speculative execution for reasoning about security vulnerabilities
Robert J. Colvin, Kirsten Winter
Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class o…
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…
Correctness of Concurrent Objects under Weak Memory Models
Graeme Smith, Kirsten Winter, Robert J. Colvin
In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when eff…