swMATH ID: 18521
Software Authors: Travkin, Oleg; Wehrheim, Heike
Description: Verification of concurrent programs on weak memory models. Modern multi-core processors equipped with weak memory models seemingly reorder instructions (with respect to program order) due to built-in optimizations. For concurrent programs, weak memory models thereby produce interleaved executions which are impossible on sequentially consistent (SC) memory. Verification of concurrent programs consequently needs to take the memory model of the executing processor into account. This, however, makes most standard software verification tools inapplicable.{par}In this paper, we propose a technique (and present its accompanying tool {sc Weak2SC}) for reducing the verification problem for weak memory models to the verification on SC. The reduction proceeds by generating – out of a given program and weak memory model (here, TSO or PSO) – a new program containing all reorderings, thus already exhibiting the additional interleavings on SC. Our technique is compositional in the sense that program generation can be carried out on single processes without ever needing to inspect the state space of the concurrent program. We formally prove compositionality as well as soundness of our technique.{par}{sc Weak2SC} takes standard C programs as input and produces program descriptions which can be fed into automatic model checking tools (like SPIN) as well as into interactive provers (like KIV). Thereby, we allow for a wide range of verification options. We demonstrate the effectiveness of our technique by evaluating {sc Weak2SC} on a number of example programs, ranging from concurrent data structures to software transactional memory algorithms.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-319-46750-4_1
Related Software: LLVM; GitHub; Lazy-CSeq; UMM; Checkfence; CBMC; SPIN
Cited in: 1 Document

Cited in 0 Serials

Citations by Year