uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Context-Bounded Analysis of TSO Systems
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
LIAFA, CNRS and University of Paris Diderot. (Modeling and Verification)
University of Southampton.
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)
Abstract [en]

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
Keyword [en]
weak memory models, under-approximation techniques
National Category
Computer Systems
Research subject
Computer Science
URN: 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
UPMARCWeak Memory Models
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2015-03-11Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Atig, Mohamed Faouzi
By organisation
Computer Systems
Computer Systems

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: 218 hits
ReferencesLink to record
Permanent link

Direct link