UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Stability in weak memory models

Alglave, J; Maranget, L; (2011) Stability in weak memory models. In: (pp. pp. 50-66).

Full text not available from this repository.


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. © 2011 Springer-Verlag.

Type: Proceedings paper
Title: Stability in weak memory models
ISBN-13: 9783642221095
DOI: 10.1007/978-3-642-22110-1_6
URI: http://discovery.ucl.ac.uk/id/eprint/1366411
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item