liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Counter-Example Guided Fence Insertion under TSO
Uppsala University, Sweden.
Uppsala University, Sweden.
Academia Sinica, Taiwan.
Uppsala University, Sweden.
Show others and affiliations
2012 (English)In: TACAS 2012, 2012Conference paper (Refereed)
Abstract [en]

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
National Category
Computer and Information Science
URN: 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: 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
Available from: 2012-05-10 Created: 2012-05-10 Last updated: 2015-05-28

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Rezine, Ahmed
By organisation
ESLAB - Embedded Systems LaboratoryThe Institute of Technology
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 365 hits
ReferencesLink to record
Permanent link

Direct link