15 citations · 24 across the 5 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…