Showing cs.PLShow all
2 papers · 1 filter
cs.PL2018
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…
cs.PL2018
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…