Document Open Access Logo

What Cannot Be Implemented on Weak Memory?

Authors Armando Castañeda , Gregory Chockler , Brijesh Dongol , Ori Lahav

PDF
Thumbnail PDF

File

LIPIcs.DISC.2024.11.pdf
  • Filesize: 1 MB
  • 22 pages

Document Identifiers

Author Details

Armando Castañeda
  • Instituto de Matemáticas, Universidad Nacional Autónoma de México, Mexico
Gregory Chockler
  • Department of Computer Science, University of Surrey, Guildford, UK
Brijesh Dongol
  • Department of Computer Science, University of Surrey, Guildford, UK
Ori Lahav
  • School of Computer Science, Tel Aviv University, Israel

Funding

  • Castañeda, Armando: Supported by DGAPA PAPIIT project IN108723 and Royal Society grant IES\R1\221226.
  • Chockler, Gregory: Supported by Royal Society grant: IES\R1\221226; CHIST-ERA project REDONDA EP/Y036425/1; and EPSRC grants: EP/X037142/1 and EP/X015149/1.
  • Dongol, Brijesh: Supported by VeTSS; Royal Society grant: IES\R1\221226; CHIST-ERA project REDONDA EP/Y036425/1; and EPSRC grants: EP/X037142/1, EP/X015149/1, EP/V038915/1, and EP/R025134/2.
  • Lahav, Ori: Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 851811) and the Israel Science Foundation (grant number 814/22).

Cite AsGet BibTex

Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav. What Cannot Be Implemented on Weak Memory?. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.DISC.2024.11

Abstract

We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties, identifying restrictions under which independent memory traces can be merged into a single valid memory trace. In turn, we show that the mergeability properties of the underlying memory model entail similar mergeability requirements on the specifications of objects that can be implemented on that memory model. We demonstrate the applicability of our approach to establish the impossibility of implementing standard distributed objects with different restrictions on memory traces on three memory models: strictly consistent memory, total store order, and release-acquire. These impossibility results allow us to identify tight and almost tight bounds for some objects, as well as new separation results between weak memory models, and between well-studied objects based on their implementability on weak memory models.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Concurrent algorithms
Keywords
  • Impossibility
  • Weak Memory Models
  • Total-Store Order
  • Release-Acquire

Metrics

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

Related Versions

References

  1. Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. J. ACM, 40(4):873-890, 1993. URL: https://doi.org/10.1145/153724.153741.
  2. James Aspnes. Time-and space-efficient randomized consensus. In PODC, pages 325-331, New York, NY, USA, 1990. ACM. URL: https://doi.org/10.1145/93385.93433.
  3. James Aspnes, Hagit Attiya, and Keren Censor-Hillel. Polylogarithmic concurrent data structures from monotone circuits. J. ACM, 59(1):2:1-2:24, 2012. URL: https://doi.org/10.1145/2108242.2108244.
  4. James Aspnes and Maurice Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 11(3):441-461, 1990. URL: https://doi.org/10.1016/0196-6774(90)90021-6.
  5. James Aspnes and Maurice Herlihy. Wait-free data structures in the asynchronous PRAM model. In SPAA, pages 340-349. ACM, 1990. URL: https://doi.org/10.1145/97444.97701.
  6. Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, and Martin T. Vechev. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In POPL, pages 487-498. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926442.
  7. Mirza Ahad Baig, Danny Hendler, Alessia Milani, and Corentin Travers. Long-lived counters with polylogarithmic amortized step complexity. Distributed Comput., 36(1):29-43, 2023. URL: https://doi.org/10.1007/S00446-022-00439-5.
  8. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In POPL, pages 55-66, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1926385.1926394.
  9. Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. Checking and enforcing robustness against TSO. In ESOP, volume 7792 of LNCS, pages 533-553. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_29.
  10. Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, and Serdar Tasiran. Reasoning about TSO programs using reduction and abstraction. In CAV, pages 336-353, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-96142-2_21.
  11. Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann. Deciding robustness against total store ordering. In ICALP (2), pages 428-440, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_34.
  12. Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. Concurrent library correctness on the TSO memory model. In ESOP, pages 87-107, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-28869-2_5.
  13. James E. Burns and Nancy A. Lynch. Bounds on shared memory for mutual exclusion. Inf. Comput., 107(2):171-184, 1993. URL: https://doi.org/10.1006/INCO.1993.1065.
  14. Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav. What cannot be implemented on weak memory? CoRR, abs/2405.16611, 2024. URL: https://doi.org/10.48550/arXiv.2405.16611.
  15. Armando Castañeda and Miguel Piña. Read/write fence-free work-stealing with multiplicity. J. Parallel Distributed Comput., 186:104816, 2024. URL: https://doi.org/10.1016/J.JPDC.2023.104816.
  16. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Set-linearizable implementations from read/write operations: Sets, fetch &increment, stacks and queues with multiplicity. Distributed Comput., 36(2):89-106, 2023. URL: https://doi.org/10.1007/s00446-022-00440-y.
  17. Edsger W. Dijkstra. EWD123: Cooperating Sequential Processes. Technical report, University of Texas, 1965. URL: http://www.cs.utexas.edu/~EWD/transcriptions/EWD01xx/EWD123.html.
  18. Eli Gafni and Leslie Lamport. Disk paxos. Distrib. Comput., 16(1):1-20, February 2003. URL: https://doi.org/10.1007/S00446-002-0070-8.
  19. Seth Gilbert and Nancy A. Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2):51-59, 2002. URL: https://doi.org/10.1145/564585.564601.
  20. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124-149, 1991. URL: https://doi.org/10.1145/114005.102808.
  21. Maurice Herlihy, Victor Luchangco, and Mark Moir. Obstruction-free synchronization: Double-ended queues as an example. In ICDCS, pages 522-529, 2003. URL: https://doi.org/10.1109/ICDCS.2003.1203503.
  22. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: https://doi.org/10.1145/78969.78972.
  23. Intel. Intelregistered 64 and IA-32 architectures software developer’s manual. Volume 3B: system programming guide, Part, 2(11):1-64, 2011. Google Scholar
  24. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising semantics for relaxed-memory concurrency. In POPL, pages 175-189, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009850.
  25. J. Y. Kawash. Limitation and capabilities of weak memory consistency systems. PhD thesis, University of Calgary, 2000. doi:10.11575/PRISM/19939. Google Scholar
  26. Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming release-acquire consistency. In POPL, pages 649-662, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837643.
  27. Ori Lahav and Roy Margalit. Robustness against release/acquire semantics. In PLDI, pages 126-141, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3314221.3314604.
  28. Leslie Lamport. A new solution of Dijkstra’s concurrent programming problem. Commun. ACM, 17(8):453-455, 1974. URL: https://doi.org/10.1145/361082.361093.
  29. Roy Margalit and Ori Lahav. Verifying observational robustness against a C11-style memory model. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434285.
  30. Adam Morrison and Yehuda Afek. Fence-free work stealing on bounded TSO processors. In ASPLOS, pages 413-426. ACM, 2014. URL: https://doi.org/10.1145/2541940.2541987.
  31. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs, pages 391-407, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-03359-9_27.
  32. Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290381.
  33. Michel Raynal. Distributed universal construcitons: a guided tour. Bulleting of EATCS: Distributed Computing Column, (121), 2011. Google Scholar
  34. Arik Rinberg and Idit Keidar. Intermediate value linearizability: A quantitative correctness criterion. In DISC, volume 179 of LIPIcs, pages 2:1-2:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.DISC.2020.2.
  35. Abhishek Kr Singh and Ori Lahav. An operational approach to library abstraction under relaxed memory concurrency. Proc. ACM Program. Lang., 7(POPL):1542-1572, 2023. URL: https://doi.org/10.1145/3571246.
  36. SPARC International Inc. The SPARC architecture manual (version 9). Prentice-Hall, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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