Document Open Access Logo

Brief Announcement: How Complex Can Sequential Consistency Be?

Author Dimitar Dimitrov

PDF

File

Thumbnail PDF
PDF
LIPIcs.DISC.2026.60.pdf
  • Filesize: 0.64 MB
  • 6 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Complexity theory and logic
Keywords
  • Distributed systems
  • Consistency
  • Complexity

Metrics

Abstract

Sequential consistency (SC) is the prototypical correctness criterion for shared-memory systems. Deciding whether a finite execution history is SC is NP-complete [Gibbons and Korach, 1997]. In this brief announcement, we study the complexity of SC over infinite execution histories. It is known that SC is not among the safety properties [Glusman and Katz, 2001], which sit at the lowest level of the Borel hierarchy. We show that, under finite arrival, SC is in fact a liveness property. We further demonstrate that no deterministic transducer can compute sequential witnesses for all SC histories, nor can any infinite-state deterministic Büchi acceptor recognize SC. Finally, we establish that, under infinite arrival, SC for memories with unbounded registers and DCAS (double compare-and-swap) is 𝚺¹₁-complete.

Cite As Get BibTex

Dimitar Dimitrov. Brief Announcement: How Complex Can Sequential Consistency Be?. In 40th International Symposium on Distributed Computing (DISC 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 397, pp. 60:1-60:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.DISC.2026.60

Author Details

Dimitar Dimitrov
  • INSAIT, Sofia University "St. Kliment Ohridski", Bulgaria

Funding

This research was partially funded by the Ministry of Education and Science of Bulgaria (support for INSAIT, part of the Bulgarian National Roadmap for Research Infrastructure).

References

  1. Yehuda Afek, Geoffrey Brown, and Michael Merritt. Lazy caching. ACM Trans. Program. Lang. Syst., 15(1):182-205, January 1993. URL: https://doi.org/10.1145/151646.151651.
  2. Marcos K. Aguilera. A pleasant stroll through the land of infinitely many creatures. ACM SIGACT News, 35(2):36-59, June 2004. URL: https://doi.org/10.1145/992287.992298.
  3. 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, March 1995. URL: https://doi.org/10.1007/BF01784241.
  4. Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181-185, October 1985. URL: https://doi.org/10.1016/0020-0190(85)90056-0.
  5. Rajeev Alur, Ken McMillan, and Doron Peled. Model-checking of correctness conditions for concurrent objects. Information and Computation, 160(1):167-188, July 2000. URL: https://doi.org/10.1006/inco.1999.2847.
  6. K. R. Apt and G. D. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM (JACM), 33(4):724-767, August 1986. URL: https://doi.org/10.1145/6490.6494.
  7. Hagit Attiya and Jennifer L. Welch. Sequential consistency versus linearizability. ACM Trans. Comput. Syst., 12(2):91-122, May 1994. URL: https://doi.org/10.1145/176575.176576.
  8. Jesse D. Bingham, Anne Condon, and Alan J. Hu. Toward a decidable notion of sequential consistency. In Proceedings of the Fifteenth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA '03, pages 304-313, New York, NY, USA, June 2003. Association for Computing Machinery. URL: https://doi.org/10.1145/777412.777467.
  9. Ivana Filipović, Peter O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theoretical Computer Science, 411(51):4379-4398, December 2010. URL: https://doi.org/10.1016/j.tcs.2010.09.021.
  10. Rob Gerth. Sequential consistency and the lazy caching algorithm. Distributed computing, 12(2):57-59, May 1999. URL: https://doi.org/10.1007/s004460050057.
  11. Phillip B. Gibbons and Ephraim Korach. Testing shared memories. SIAM Journal on Computing, 26(4):1208-1244, August 1997. URL: https://doi.org/10.1137/S0097539794279614.
  12. Marcelo Glusman and Shmuel Katz. Extending memory consistency of finite prefixes to infinite computations. In Kim G. Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, pages 411-425, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-44685-0_28.
  13. Rachid Guerraoui and Eric Ruppert. Linearizability is not always a safety property. In Guevara Noubir and Michel Raynal, editors, Networked Systems, pages 57-69, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-09581-3_5.
  14. 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.
  15. Alexander S. Kechris. Classical Descriptive Set Theory, volume 156 of Graduate Texts in Mathematics. Springer, New York, NY, 1995. URL: https://doi.org/10.1007/978-1-4612-4190-4.
  16. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, March 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  17. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28(9):690-691, September 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  18. Zohar Manna and Amir Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(3):257-289, December 1984. URL: https://doi.org/10.1016/0167-6423(84)90003-0.
  19. Susan Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319-340, December 1976. URL: https://doi.org/10.1007/BF00268134.
  20. Susan Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455-495, July 1982. URL: https://doi.org/10.1145/357172.357178.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact