Document Open Access Logo

Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs That Use Concurrent Objects

Authors Hagit Attiya , Constantin Enea

PDF
Thumbnail PDF

File

LIPIcs.DISC.2019.2.pdf
  • Filesize: 0.64 MB
  • 17 pages

Document Identifiers

Author Details

Hagit Attiya
  • Technion - Israel Institute of Technology, Haifa, Israel
Constantin Enea
  • Université de Paris, IRIF, CNRS, F-75013 Paris, France

Funding

  • Attiya, Hagit: Partially supported by the Israel Science Foundation (1749/14 and 380/18).
  • Enea, Constantin: Supported in part by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 678177).

Cite As Get BibTex

Hagit Attiya and Constantin Enea. Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs That Use Concurrent Objects. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.DISC.2019.2

Abstract

It has been observed that linearizability, the prevalent consistency condition for implementing concurrent objects, does not preserve some probability distributions. A stronger condition, called strong linearizability has been proposed, but its study has been somewhat ad-hoc. This paper investigates strong linearizability by casting it in the context of observational refinement of objects. We present a strengthening of observational refinement, which generalizes strong linearizability, obtaining several important implications.
When a concrete concurrent object refines another, more abstract object - often sequential - the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This means that trace properties of a program using the concrete object can be proved by considering the program with the abstract object. This, however, does not hold for hyperproperties, including many security properties and probability distributions of events.
We define strong observational refinement, a strengthening of refinement that preserves hyperproperties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability. This implies that strong linearizability is also equivalent to forward simulation, and shows that strongly linearizable implementations can be composed both horizontally (i.e., locality) and vertically (i.e., with instantiation).
For situations where strongly linearizable implementations do not exist (or are less efficient), we argue that reasoning about hyperproperties of programs can be simplified by strong observational refinement of non-atomic abstract objects.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Program specifications
  • General and reference → Verification
Keywords
  • Concurrent Objects
  • Linearizability
  • Hyperproperties
  • Forward Simulations

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. Yehuda Afek, Eli Gafni, and Adam Morrison. Common2 extended to stacks and unbounded concurrency. Distributed Computing, 20(4):239-252, 2007. URL: https://doi.org/10.1007/s00446-007-0023-3.
  3. Rajeev Alur, Pavol Cerný, and Steve Zdancewic. Preserving Secrecy Under Refinement. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 107-118. Springer, 2006. URL: https://doi.org/10.1007/11787006_10.
  4. James Aspnes. Randomized protocols for asynchronous consensus. Distributed Computing, 16(2-3):165-175, 2003. URL: https://doi.org/10.1007/s00446-002-0081-5.
  5. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Tractable Refinement Checking for Concurrent Objects. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 651-662. ACM, 2015. URL: https://doi.org/10.1145/2676726.2677002.
  6. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. Proving Linearizability Using Forward Simulations. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 542-563. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_28.
  7. 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.
  8. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal Logics for Hyperproperties. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  9. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  10. Oksana Denysyuk and Philipp Woelfel. Wait-Freedom is Harder Than Lock-Freedom Under Strong Linearizability. In Yoram Moses, editor, Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings, volume 9363 of Lecture Notes in Computer Science, pages 60-74. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48653-5_5.
  11. Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A Scalable, Correct Time-Stamped Stack. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 233-246. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676963.
  12. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379-4398, 2010. URL: https://doi.org/10.1016/j.tcs.2010.09.021.
  13. Joseph A. Goguen and José Meseguer. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  14. Wojciech M. Golab, Lisa Higham, and Philipp Woelfel. Linearizable implementations do not suffice for randomized distributed computation. In Lance Fortnow and Salil P. Vadhan, editors, Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, pages 373-382. ACM, 2011. URL: https://doi.org/10.1145/1993636.1993687.
  15. Maryam Helmi, Lisa Higham, and Philipp Woelfel. Strongly linearizable implementations: possibilities and impossibilities. In Darek Kowalski and Alessandro Panconesi, editors, ACM Symposium on Principles of Distributed Computing, PODC '12, Funchal, Madeira, Portugal, July 16-18, 2012, pages 385-394. ACM, 2012. URL: https://doi.org/10.1145/2332432.2332508.
  16. 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.
  17. Nancy A. Lynch and Frits W. Vaandrager. Forward and Backward Simulations: I. Untimed Systems. Inf. Comput., 121(2):214-233, 1995. URL: https://doi.org/10.1006/inco.1995.1134.
  18. John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, USA, May 16-18, 1994, pages 79-93. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/RISP.1994.296590.
  19. Sean Ovens and Philipp Woelfel. Strongly Linearizable Implementations of Snapshots and Other Types. In 38th ACM Symposium on Principles of Distributed Computing (PODC 2019), 2019. Google Scholar
  20. Amgad Sadek Rady. Characterizing Implementations that Preserve Properties of Concurrent Randomized Algorithms. Master’s thesis, York University, Toronto, Canada, 2017. Google Scholar
  21. Gerhard Schellhorn, Heike Wehrheim, and John Derrick. How to Prove Algorithms Linearisable. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 243-259. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_21.
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