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

Direct link
What's decidable about weak memory models?
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2012 (English)In: Programming Languages and Systems, Springer Berlin/Heidelberg, 2012, 26-46 p.Conference paper (Refereed)
Abstract [en]

We investigate the decidability of the state reachability problem in finite-state programs running under weak memory models. In [3], we have shown that this problem is decidable for TSO and its extension with the write-to-write order relaxation, but beyond these models nothing is known to be decidable. Moreover, we have shown that relaxing the program order by allowing reads or writes to overtake reads leads to undecidability. In this paper, we refine these results by sharpening the (un)decidability frontiers on both sides. On the positive side, we introduce a new memory model NSW (for non-speculative writes) that extends TSO with the write-to-write relaxation, the read-to-read relaxation, and support for partial fences. We present a backtrack-free operational model for NSW, and prove that it does not allow causal cycles (thus barring pathological out-of-thin-air effects). On the negative side, we show that adding the read-to-write relaxation to TSO causes undecidability, and that adding non-atomic writes to NSW also causes undecidability. Our results establish that NSW is the first known hardware-centric memory model that is relaxed enough to permit both delayed execution of writes and early execution of reads for which the reachability problem is decidable.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2012. 26-46 p.
, Lecture Notes in Computer Science, 7211
National Category
Computer Engineering
URN: urn:nbn:se:uu:diva-190162DOI: 10.1007/978-3-642-28869-2_2ISI: 000310871200002ISBN: 978-3-642-28868-5OAI: oai:DiVA.org:uu-190162DiVA: diva2:583188
21st European Symposium on Programming (ESOP) held as Part of the 15th European Joint Conferences on Theory and Practice of Software (ETAPS)
UPMARCWeak Memory Models
Available from: 2012-03-22 Created: 2013-01-07 Last updated: 2014-12-13

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 Engineering

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

Direct link