Paper Info
Title
Simulation and Invariance for Weak Consistency.
Abstract
We aim at developing correct algorithms for a wide variety of weak consistency models M-0,..., M-n. Given an algorithm A and a consistency model M is an element of{M-0,..., M-n}, at quite a high-level examining the correctness of the algorithm A under M amounts to asking, for example, "can these executions happen?", or "are these the only possible executions?". Since a few years, Luc Maranget and myself have been designing and developing the herd7 simulation tool: given a litmus test, i.e. a small piece of code and a consistency model, i.e. a set of constraints defining the valid executions of a program, the herd7 tool outputs all the possible executions of the litmus test under the consistency model. In recent works with Patrick Cousot, we have developed an invariance method for proving the correctness of algorithms under weak consistency models. In this paper I would like to give a general overview of these works.
Year
DOI
Venue
2016
10.1007/978-3-662-53413-7_1
Lecture Notes in Computer Science
Field
DocType
Volume
Shared variables,Invariant (physics),Computer science,Critical section,Correctness,Litmus,Theoretical computer science,Weak consistency,Consistency model
Conference
9837
ISSN
Citations 
PageRank 
0302-9743
2
0.37
References 
Authors
7
1
Name
Order
Citations
PageRank
Jade Alglave160826.53