Counter-Example Guided Fence Insertion under TSO
2012 (English)In: TACAS 2012, 2012Conference paper (Refereed)
We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.
Place, publisher, year, edition, pages
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 7214
Computer and Information Science
IdentifiersURN: urn:nbn:se:liu:diva-77285DOI: 10.1007/978-3-642-28756-5_15ISI: 000342900100015ISBN: 978-3-642-28755-8ISBN: 978-3-642-28756-5OAI: oai:DiVA.org:liu-77285DiVA: diva2:526205
18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia, March 24 - April 1, 2012