Document Open Access Logo

AMECOS: A Modular Event-Based Framework for Concurrent Object Specification

Authors Timothé Albouy , Antonio Fernández Anta , Chryssis Georgiou , Mathieu Gestin , Nicolas Nicolaou , Junlang Wang

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2024.4.pdf
  • Filesize: 0.92 MB
  • 29 pages

Document Identifiers

Author Details

Timothé Albouy
  • Univ Rennes, Inria, CNRS, IRISA, France
Antonio Fernández Anta
  • IMDEA Networks Institute, Madrid, Spain
Chryssis Georgiou
  • University of Cyprus, Nicosia, Cyprus
Mathieu Gestin
  • Univ Rennes, Inria, CNRS, IRISA, France
Nicolas Nicolaou
  • Algolysis Ltd, Nicosia, Cyprus
Junlang Wang
  • IMDEA Networks Institute, Madrid, Spain
  • Universidad Carlos III de Madrid, Spain

Funding

This work has been partially supported by Région Bretagne, the French ANR project ByBloS (ANR-20-CE25-0002-01), the H2020 project SOTERIA, the Spanish Ministry of Science and Innovation under grants SocialProbing (TED2021-131264B-I00) and DRONAC (PID2022-140560OB-I00), the ERDF "A way of making Europe", NextGenerationEU, and the Spanish Government’s "Plan de Recuperación, Transformación y Resiliencia".

Cite As Get BibTex

Timothé Albouy, Antonio Fernández Anta, Chryssis Georgiou, Mathieu Gestin, Nicolas Nicolaou, and Junlang Wang. AMECOS: A Modular Event-Based Framework for Concurrent Object Specification. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.OPODIS.2024.4

Abstract

In this work, we introduce a modular framework for specifying distributed systems that we call AMECOS. Specifically, our framework departs from the traditional use of sequential specification, which presents limitations both on the specification expressiveness and implementation efficiency of inherently concurrent objects, as documented by Castañeda, Rajsbaum and Raynal in CACM 2023. Our framework focuses on the interactions between the various system components, specified as concurrent objects. Interactions are described with sequences of object events. This provides a modular way of specifying distributed systems and separates legality (object semantics) from other issues, such as consistency. We demonstrate the usability of our framework by (i) specifying various well-known concurrent objects, such as registers, shared memory, message-passing, reliable broadcast, and consensus, (ii) providing hierarchies of ordering semantics (namely, consistency hierarchy, memory hierarchy, and reliable broadcast hierarchy), and (iii) presenting a novel axiomatic proof of the impossibility of the well-known Consensus problem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
Keywords
  • Concurrency
  • Object specification
  • Consistency conditions
  • Consensus impossibility

Metrics

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

References

  1. Ali E. Abdallah, Cliff B. Jones, and Jeff W. Sanders, editors. Communicating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, volume 3525 of Lecture Notes in Computer Science. Springer, 2005. Google Scholar
  2. Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. Causal memory: Definitions, implementation, and programming. Distributed Comput., 9(1):37-49, 1995. URL: https://doi.org/10.1007/BF01784241.
  3. Timothé Albouy, Davide Frey, Michel Raynal, and François Taïani. Asynchronous Byzantine reliable broadcast with a message adversary. Theor. Comput. Sci., 978:114110, 2023. URL: https://doi.org/10.1016/J.TCS.2023.114110.
  4. Hagit Attiya and Jennifer L. Welch. Distributed computing - Fundamentals, simulations, and advanced topics (2. ed.). Wiley series on parallel and distributed computing. Wiley, 2004. Google Scholar
  5. Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google Scholar
  6. Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda – A Functional Language with Dependent Types. In Theorem Proving in Higher Order Logics, pages 73-78, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  7. Gabriel Bracha. Asynchronous Byzantine agreement protocols. Inf. Comput., 75(2):130-143, 1987. URL: https://doi.org/10.1016/0890-5401(87)90054-X.
  8. Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang., 1(1-2):1-150, 2014. URL: https://doi.org/10.1561/2500000011.
  9. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: specification, verification, optimality. In Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), pages 271-284. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535848.
  10. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Unifying concurrent objects and distributed tasks: Interval-linearizability. J. ACM, 65(6):45:1-45:42, 2018. URL: https://doi.org/10.1145/3266457.
  11. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. A linearizability-based hierarchy for concurrent specifications. Commun. ACM, 66(1):86-97, 2023. URL: https://doi.org/10.1145/3546826.
  12. Shir Cohen and Idit Keidar. Tame the wild with Byzantine linearizability: Reliable broadcast, snapshots, and asset transfer. In Proc. 35th Int'l Symposium on Distributed Computing (DISC'21), volume 209 of LIPIcs, pages 18:1-18:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.DISC.2021.18.
  13. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "not never" revisited: On branching versus linear time. In Proc. 10th ACM Symposium on Principles of Programming Languages (POPL'83), pages 127-140. ACM Press, 1983. URL: https://doi.org/10.1145/567067.567081.
  14. Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, 1985. URL: https://doi.org/10.1145/3149.214121.
  15. Eli Gafni and Giuliano Losa. Invited paper: Time is not a healer, but it sure makes hindsight 20:20. In Proc. 25th Int'l Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'23), volume 14310 of Lecture Notes in Computer Science, pages 62-74. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44274-2_6.
  16. Vassos Hadzilacos and Sam Toueg. A modular approach to fault-tolerant broadcasts and related problems. Technical report, Cornell University, 1994. Google Scholar
  17. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124-149, 1991. URL: https://doi.org/10.1145/114005.102808.
  18. Maurice Herlihy, Sergio Rajsbaum, and Mark R. Tuttle. Unifying synchronous and asynchronous message-passing models. In Proc 17th ACM Symposium on Principles of Distributed Computing (PODC'98), pages 133-142. ACM, 1998. URL: https://doi.org/10.1145/277697.277722.
  19. Maurice Herlihy and Nir Shavit. The topological structure of asynchronous computability. J. ACM, 46(6):858-923, 1999. URL: https://doi.org/10.1145/331524.331529.
  20. 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.
  21. Gunnar Hoest and Nir Shavit. Towards a topological characterization of asynchronous complexity (preliminary version). In Proc. 16th ACM Symposium on Principles of Distributed Computing (PODC'97), pages 199-208. ACM, 1997. URL: https://doi.org/10.1145/259380.259440.
  22. Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The Coq proof assistant a tutorial. Rapport Technique, 178, 1997. URL: http://www.itpro.titech.ac.jp/coq.8.2/Tutorial.pdf.
  23. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. URL: https://doi.org/10.1145/359545.359563.
  24. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  25. Leslie Lamport. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 16(3):872-923, 1994. URL: https://doi.org/10.1145/177492.177726.
  26. Richard J. Lipton and Jonathan S. Sandberg. PRAM: A scalable shared memory. Technical Report TR-180-88, Princeton University, 1988. Google Scholar
  27. Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996. Google Scholar
  28. Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 16th ACM Symposium on Principles of Distributed Computing (PODC'87), pages 137-151. ACM, 1987. URL: https://doi.org/10.1145/41840.41852.
  29. Gil Neiger. Set-linearizability. In Proc. 13th ACM Symposium on Principles of Distributed Computing (PODC'94), page 396. ACM, 1994. URL: https://doi.org/10.1145/197917.198176.
  30. Matthieu Perrin. Spécification des objets partagés dans les systèmes répartis sans-attente. (Specification of shared objects in wait-free distributed systems). PhD thesis, University of Nantes, France, 2016. URL: https://tel.archives-ouvertes.fr/tel-01390700.
  31. Matthieu Perrin, Achour Mostéfaoui, and Claude Jard. Causal consistency: beyond memory. In Proc. 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'16), pages 26:1-26:12. ACM, 2016. URL: https://doi.org/10.1145/2851141.2851170.
  32. Amir Pnueli. The temporal logic of programs. In Proc. 18th Symposium on Foundations of Computer Science (FOCS'77), pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  33. Michel Raynal. Fault-Tolerant Message-Passing Distributed Systems - An Algorithmic Approach. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94141-7.
  34. Nicola Santoro and Peter Widmayer. Time is not a healer. In Proc. 6th Symposium on Theoretical Aspects of Computer Science (STACS'89), volume 349 of Lecture Notes in Computer Science, pages 304-313. Springer, 1989. URL: https://doi.org/10.1007/BFB0028994.
  35. Nir Shavit. Data structures in the multicore age. Commun. ACM, 54(3):76-84, 2011. URL: https://doi.org/10.1145/1897852.1897873.
  36. Robert C. Steinke and Gary J. Nutt. A unified theory of shared memory consistency. J. ACM, 51(5):800-849, 2004. URL: https://doi.org/10.1145/1017460.1017464.
  37. Gadi Taubenfeld. On the nonexistence of resilient consensus protocols. Inf. Process. Lett., 37(5):285-289, 1991. URL: https://doi.org/10.1016/0020-0190(91)90221-3.
  38. Paolo Viotti and Marko Vukolic. Consistency in non-transactional distributed storage systems. ACM Comput. Surv., 49(1):19:1-19:34, 2016. URL: https://doi.org/10.1145/2926965.
  39. Roman Vitenberg and Roy Friedman. On the locality of consistency conditions. In Proc. 17th Int'l Conference on Distributed Computing (DISC'03), volume 2848 of Lecture Notes in Computer Science, pages 92-105. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39989-6_7.
  40. Hagen Völzer. A constructive proof for FLP. Inf. Process. Lett., 92(2):83-87, 2004. URL: https://doi.org/10.1016/J.IPL.2004.06.008.
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 About DROPS Imprint Privacy Contact