The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO
2015 (English)In: Programming Languages and Systems: ESOP 2015, Springer Berlin/Heidelberg, 2015, 308-332 p.Conference paper (Refereed)
We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving (SC) semantics. We instantiate our framework for the Total Store Ordering (TSO) memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes. Based on our method, we have implemented a tool and run it successfully on a wide range benchmarks.
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015. 308-332 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9032
weak memory, correctness, verification, TSO, concurrent program
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-253645DOI: 10.1007/978-3-662-46669-8_13ISI: 000361751400013ISBN: 978-3-662-46668-1OAI: oai:DiVA.org:uu-253645DiVA: diva2:815351
24th European Symposium on Programming, ESOP 2015, April 11–18, London, UK