2026-07-24T19:05:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24878 2026-02-09T07:42:19Z ddc:004 open_access

Brief Announcement: Time, Fences and the Ordering of Events in TSO Nataf, Raïssa Moses, Yoram TSO linearizability happens before fences synchronization actions Total Store Order (TSO) is one of the most popular relaxed memory model in multiprocessor architectures, widely implemented, for example, in Intel’s x86 and x64 platforms. It delays write visibility via store buffers, thereby allowing a significant improvement in efficiency. This, however, complicates reasoning about correctness, as executions may violate sequential consistency. We present a semantic framework that provides effective tools that can pinpoint when such synchronization is necessary under TSO. We define a TSO-specific occurs-before relation, adapting Lamport’s happens-before to TSO, and prove that events at different sites can be temporally ordered only via an occurs-before chain. Analyzing how fences and RMWs create these chains lets us identify when they are unavoidable. We present in this BA how these results impact linearizable implementations of registers, capturing information flow and causality in TSO. The full version of this work provides details as well as results regarding the need for synchronization in linearizable implementations of additional objects. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Raïssa Nataf and Yoram Moses 2025 Is Part Of LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.DISC.2025.62 urn:nbn:de:0030-drops-248784 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.62 eng https://creativecommons.org/licenses/by/4.0/legalcode