Document Open Access Logo

Brief Announcement: Time, Fences and the Ordering of Events in TSO

Authors Raïssa Nataf , Yoram Moses

PDF

File

Thumbnail PDF
PDF
LIPIcs.DISC.2025.62.pdf
  • Filesize: 0.68 MB
  • 7 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Concurrent algorithms
Keywords
  • TSO
  • linearizability
  • happens before
  • fences
  • synchronization actions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Raïssa Nataf and Yoram Moses. Brief Announcement: Time, Fences and the Ordering of Events in TSO. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 62:1-62:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.DISC.2025.62

Author Details

Raïssa Nataf
  • Technion, Haifa, Israel
Yoram Moses
  • Technion, Haifa, Israel

References

  1. Mustaque Ahamad, Gil Neiger, James E Burns, Prince Kohli, and Phillip W Hutto. Causal memory: Definitions, implementation, and programming. Distributed Computing, 9(1):37-49, 1995. URL: https://doi.org/10.1007/BF01784241.
  2. Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. Don’t sit on the fence: A static analysis approach to automatic fence insertion. ACM Trans. Program. Lang. Syst., 39(2), May 2017. URL: https://doi.org/10.1145/2994593.
  3. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Fences in weak memory models. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 258-272. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_25.
  4. Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, and Martin Vechev. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In 38th POPL, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1926385.1926442.
  5. Gérard Boudol and Gustavo Petri. Relaxed memory models: an operational approach. In 36th POPL, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1480881.1480930.
  6. Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, and Ori Lahav. What cannot be implemented on weak memory? In DISC 2024, LIPIcs, 2024. URL: https://doi.org/10.4230/LIPICS.DISC.2024.11.
  7. Cormac Flanagan and Stephen N Freund. Fasttrack: Efficient and precise dynamic race detection. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 121-133. ACM, 2009. URL: https://doi.org/10.1145/1542476.1542490.
  8. Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, july 1990. URL: https://doi.org/10.1145/78969.78972.
  9. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. SIGPLAN Not., 52(6):618-632, June 2017. URL: https://doi.org/10.1145/3140587.3062352.
  10. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, july 1978. URL: https://doi.org/10.1145/359545.359563.
  11. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers c-28, 9:690-691, 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  12. Friedemann Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms, pages 215-226. North-Holland, 1989. Google Scholar
  13. Yoram Moses. Relating knowledge and coordinated action: The knowledge of preconditions principle. In R. Ramanujam, editor, 15th TARK, pages 231-245, 2015. URL: https://doi.org/10.4204/EPTCS.215.17.
  14. Raïssa Nataf and Yoram Moses. Communication Requirements for Linearizable Registers. In DISC 2024, Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2024. URL: https://doi.org/10.4230/LIPIcs.DISC.2024.33.
  15. Raïssa Nataf and Yoram Moses. Time, fences and the ordering of events in TSO, 2025. URL: https://arxiv.org/abs/2508.11415.
  16. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pages 391-407, Berlin, Heidelberg, 2009. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-03359-9_27.
  17. Viktor Vafeiadis and Francesco Zappa Nardelli. Verifying fence elimination optimisations. In Proceedings of the 18th International Conference on Static Analysis, SAS'11, pages 146-162, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-23702-7_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact