22 citations · 44 across the 9 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…
A wide-spectrum language for verification of programs on weak memory models
Robert J. Colvin, Graeme Smith
Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program t…