Document Open Access Logo

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement

Authors Brijesh Dongol , Gerhard Schellhorn, Heike Wehrheim

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2022.31.pdf
  • Filesize: 0.96 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Concurrency
  • Security and privacy → Formal methods and theory of security
Keywords
  • Strong Observational Refinement
  • Hyperproperties
  • Forward Simulation
  • Weak Progressiveness

Metrics

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

Abstract

Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with only finite traces. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a (weak) progress condition, and prove that this weak progressive forward simulation is equivalent to strong observational refinement.

Cite As Get BibTex

Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.31

Author Details

Brijesh Dongol
  • University of Surrey, UK
Gerhard Schellhorn
  • Universität Augsburg, Germany
Heike Wehrheim
  • Universität Oldenburg, Germany

Funding

  • Dongol, Brijesh: EPSRC grants EP/V038915/1 and EP/R032556/1, VeTSS and ARC Discovery Grant DP190102142.
  • Wehrheim, Heike: DFG Grant WE2290/12-1.

Acknowledgements

We thank John Derrick, Simon Doherty, Constantin Enea and our anonymous CONCUR reviewers for their comments on earlier versions of this paper.

References

  1. J. Aspnes. Randomized protocols for asynchronous consensus. Distributed Comput., 16(2-3):165-175, 2003. URL: https://doi.org/10.1007/s00446-002-0081-5.
  2. H. Attiya and C. Enea. Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In J. Suomela, editor, DISC, volume 146 of LIPIcs, pages 2:1-2:17. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.DISC.2019.2.
  3. A. Bouajjani, M. Emmi, C. Enea, and S. O. Mutluergil. Proving linearizability using forward simulations. In R. Majumdar and V. Kuncak, editors, CAV, 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.
  4. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560-599, 1984. URL: https://doi.org/10.1145/828.833.
  5. M. R. Clarkson and F. B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  6. R. Colvin and B. Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74(3):143-165, 2009. URL: https://doi.org/10.1016/j.scico.2008.09.013.
  7. J. Derrick and E. A. Boiten. Refinement in Z and Object-Z - Foundations and Advanced Applications (2. ed.). Springer, 2014. URL: https://doi.org/10.1007/978-1-4471-5355-9.
  8. J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. Brief Announcement: On Strong Observational Refinement and Forward Simulation. In S. Gilbert, editor, DISC, volume 209 of LIPIcs, pages 55:1-55:4, Dagstuhl, Germany, 2021. URL: https://doi.org/10.4230/LIPIcs.DISC.2021.55.
  9. J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. On strong observational refinement and forward simulation. CoRR, 2021. URL: http://arxiv.org/abs/2107.14509.
  10. J. Derrick, G. Schellhorn, and H. Wehrheim. Proving linearizability via non-atomic refinement. In J. Davies and J. Gibbons, editors, iFM, volume 4591 of Lecture Notes in Computer Science, pages 195-214. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73210-5_11.
  11. B. Dongol and L. Groves. Contextual trace refinement for concurrent objects: Safety and progress. In K. Ogata, M. Lawford, and S. Liu, editors, ICFEM, volume 10009 of Lecture Notes in Computer Science, pages 261-278, 2016. URL: https://doi.org/10.1007/978-3-319-47846-3_17.
  12. J. A. Goguen and J. Meseguer. Security policies and security models. In S&P, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  13. W. M. Golab, L. Higham, and P. Woelfel. Linearizable implementations do not suffice for randomized distributed computation. In L. Fortnow and S. P. Vadhan, editors, STOC, pages 373-382. ACM, 2011. URL: https://doi.org/10.1145/1993636.1993687.
  14. A. Gotsman and H. Yang. Liveness-preserving atomicity abstraction. In L. Aceto, M. Henzinger, and J. Sgall, editors, ICALP, volume 6756 of Lecture Notes in Computer Science, pages 453-465. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_36.
  15. W. O. D. Griffioen and F. W. Vaandrager. Normed simulations. In A. J. Hu and M. Y. Vardi, editors, CAV, volume 1427 of LNCS, pages 332-344, Vancouver, BC, Canada, 1998. Google Scholar
  16. W. O. D. Griffioen and F. W. Vaandrager. A theory of normed simulations. ACM Trans. Comput. Log., 5(4):577-610, 2004. URL: https://doi.org/10.1145/1024922.1024923.
  17. M. Helmi, L. Higham, and P. Woelfel. Strongly linearizable implementations: possibilities and impossibilities. In D. Kowalski and A. Panconesi, editors, PODC, pages 385-394. ACM, 2012. URL: https://doi.org/10.1145/2332432.2332508.
  18. M. Herlihy and N. Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2008. Google Scholar
  19. M. Herlihy and J. 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.
  20. V. Luchangco, M. Moir, and N. Shavit. Nonblocking k-compare-single-swap. In A. L. Rosenberg and F. M. auf der Heide, editors, SPAA, pages 314-323. ACM, 2003. URL: https://doi.org/10.1145/777412.777468.
  21. N. A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996. Google Scholar
  22. N. A. Lynch and F. 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.
  23. J. McLean. A general theory of composition for a class of "possibilistic" properties. IEEE Trans. Software Eng., 22(1):53-67, 1996. URL: https://doi.org/10.1109/32.481534.
  24. R. Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  25. G. Schellhorn. Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS), 7(11):952-979, 2001. Google Scholar
  26. G. Schellhorn. Completeness of Fair ASM Refinement. Science of Computer Programming, Elsevier, 76, issue 9:756-773, 2009. Google Scholar
  27. G. Schellhorn, J. Derrick, and H. Wehrheim. A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log., 15(4):31:1-31:37, 2014. URL: https://doi.org/10.1145/2629496.
  28. G. Schellhorn, H. Wehrheim, and J. Derrick. How to prove algorithms linearisable. In P. Madhusudan and S. A. Seshia, editors, CAV, 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.
  29. P. Stevens. Abstract games for infinite state processes. In D. Sangiorgi and R. de Simone, editors, CONCUR, volume 1466 of Lecture Notes in Computer Science, pages 147-162. Springer, 1998. URL: https://doi.org/10.1007/BFb0055621.
  30. R. J. van Glabbeek. The linear time - branching time spectrum II. In E. Best, editor, CONCUR, volume 715 of Lecture Notes in Computer Science, pages 66-81. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
  31. R. J. van Glabbeek, B. Luttik, and N. Trcka. Branching bisimilarity with explicit divergence. Fundam. Informaticae, 93(4):371-392, 2009. URL: https://doi.org/10.3233/FI-2009-109.
  32. D. Walker. Bisimulation and divergence. Information and Computation, 85:202-241, 1990. Google Scholar
  33. S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In CSFW-16, page 29. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212703.
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