Context-Bounded Analysis of TSO Systems
2014 (English)In: From Programs to Systems: The Systems perspective in Computing / [ed] Bensalem, S; Lakhneck, Y; Legay, A, Springer, 2014, 21-38 p.Conference paper (Other academic)
We address the state reachability problem in concurrent programs running over the TSO weak memory model. This problem has been shown to be decidable with non-primitive recursive complexity in the case of finite-state threads. For recursive threads this problem is undecidable. The aim of this paper is to provide under-approximate analyses for TSO systems that are decidable and have better (elementary) complexity. We propose three bounding concepts for TSO behaviors that are inspired from the concept of bounding the number of context switches introduced by Qadeer and Rehof for the sequentially consistent (SC) model. We investigate the decidability and the complexity of the state reachability problems under these three bounding concepts for TSO, and provide reduction of these problems to known reachability problems of concurrent systems under the SC semantics.
Place, publisher, year, edition, pages
Springer, 2014. 21-38 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8415
weak memory models, under-approximation techniques
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-238133DOI: 10.1007/978-3-642-54848-2ISI: 000348370400002ISBN: 978-3-642-54847-5ISBN: 978-3-642-54848-2OAI: oai:DiVA.org:uu-238133DiVA: diva2:770097
Workshop on From Programs to Systems - The Systems Perspective in Computing (FPS) held in Honor of Joseph Sifakis, April 6, 2014, Grenoble, France
ProjectsUPMARCWeak Memory Models