Stability in Weak Memory Models

International audienceConcurrent programs running on weak memory models exhibit re-laxed behaviours, making them hard to understand and to debug. To use stan-dard 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 ensur-ing stability to a program, and show that Power's locks and read-modify-write primitives meet them. Second, we minimise the amount of required synchronisa-tion by characterising which parts of a given execution should be synchronised. Third, we characterise the programs stable from a weak architecture to SC. Fi-nally, we present our offence tool which places either lock-based or lock-free synchronisation in a x86 or Power program to ensure its stability. Concurrent programs running on modern multiprocessors exhibit subtle behaviours, making them hard to understand and to debug: modern architectures (e.g. x86 or Power) provide weak memory models, allowing optimisations such as instruction reordering, store buffering or write atomicity relaxation [2]. Thus an execution of a program may not be an interleaving of its instructions, as it would be on a Sequentially Consistent (SC) architecture [18]. Hence standard analyses for concurrent programs might be un-sound, as noted by M. Rinard in [25]. Memory model aware verification tools exist, e.g. [24, 11, 15, 30], but they often focus on one model at a time, or cannot handle the write atomicity relaxation exhibited e.g. by Power: generality remains a challenge. Fortunately, we can force a program running on a weak architecture to behave as if it were running on a stronger one (e.g. SC) by using synchronisation primitives; this underlies the data race free guarantee (DRF guarantee) of S. Adve and M. Hill [3]. Hence, as observed e.g. by S. Burckhart and M. Musuvathi in [12], "we can sensi-bly verify the relaxed executions [. . . ] by solving the following two verification problems separately: 1. Use standard verification methodology for concurrent programs to show that the [SC] executions [. . . ] are correct. 2. Use specialized methodology for memory model safety verification". Here, memory model safety means checking that the execu-tions of a program, although running on a weak architecture, are actually SC. To apply standard verification techniques to concurrent programs running on weak memory mod-els, we thus first need to ensure that our programs have a SC behaviour. S. Burckhart and M. Musuvathi focus in [12] on the Total Store Order (TSO) [28] memory model. We generalise their idea to a wider class of models (defined in [5], and recalled in Sec. 1): we examine how to force a program running on a weak architecture A 1 to behave as if running on a stronger one A 2 , a property that we call stability from A 1 to A 2 . To ensure stability to a program, we examine the problem of placing lock-based or lock-free synchronisation primitives in a program. We call synchronisation mapping a