Name
Abstract | ||
|---|---|---|
Concurrent programs running on weak memory models exhibit relaxed behaviours, making them hard to understand and to debug. To use standard verification techniques on such programs, we can force them to behave as if running on a Sequentially Consistent (SC) model. Thus, we examine how to constrain the behaviour of such programs via synchronisation to ensure what we call their stability, i.e. that they behave as if they were running on a stronger model than the actual one, e.g. SC. First, we define sufficient conditions ensuring stability to a program, and show that Power's locks and read-modify-write primitives meet them. Second, we minimise the amount of required synchronisation by characterising which parts of a given execution should be synchronised. Third, we characterise the programs stable from a weak architecture to SC. Finally, we present our offence tool which places either lock-based or lock-free synchronisation in a x86 or Power program to ensure its stability. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22110-1_6 | CAV |
Keywords | Field | DocType |
concurrent program,lock-free synchronisation,weak architecture,power program,offence tool,sequentially consistent,read-modify-write primitive,stronger model,weak memory models exhibit,required synchronisation | x86,Synchronization,Architecture,Computer science,Lock (computer science),Memory model,Embedded system,Debugging | Conference |
Citations | PageRank | References |
36 | 1.20 | 24 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jade Alglave | 1 | 608 | 26.53 |
| Luc Maranget | 2 | 808 | 49.83 |