Document Open Access Logo

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris

Authors Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.17.pdf
  • Filesize: 0.75 MB
  • 29 pages

Document Identifiers

Author Details

Jan-Oliver Kaiser
Hoang-Hai Dang
Derek Dreyer
Ori Lahav
Viktor Vafeiadis

Cite As Get BibTex

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ECOOP.2017.17

Abstract

The field of concurrent separation logics (CSLs) has recently
undergone two exciting developments: (1) the Iris framework for
encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency.
Unfortunately, these developments are seemingly incompatible, since
Iris only applies to languages with an operational interleaving
semantics, while C11 is defined by a declarative (axiomatic)
semantics.  In this paper, we show that, on the contrary, it is not
only feasible but useful to marry these developments together.  Our
first step is to provide a novel operational characterization of
RA+NA, the fragment of C11 containing RA accesses and "non-atomic"
(normal data) accesses.  Instantiating Iris with this semantics, we
then derive higher-order variants of two prominent RA+NA logics, GPS
and RSL. Finally, we deploy these derived logics in order to perform
the first mechanical verifications (in Coq) of several interesting
case studies of RA+NA programming.  In a nutshell, we provide the
first foundationally verified framework for proving programs correct
under C11's weak-memory semantics.

Subject Classification

Keywords
  • Weak memory models
  • release-acquire
  • concurrency
  • separation logic

Metrics

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

Supplementary Materials

References

  1. Technical appendix and Coq development accompanying this paper, available at the following URL: URL: http://plv.mpi-sws.org/igps/.
  2. Tatsuya Abe and Toshiyuki Maeda. Observation-based concurrent program logic for relaxed memory consistency models. In APLAS, pages 63-84, 2016. Google Scholar
  3. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. The problem of programming language concurrency semantics. In ESOP, 2015. Google Scholar
  4. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In POPL, pages 55-66, 2011. Google Scholar
  5. Richard Bornat, Jade Alglave, and Matthew J. Parkinson. New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs/1512.01416, 2015. Google Scholar
  6. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. TaDA: A logic for time and data abstraction. In ECOOP, 2014. Google Scholar
  7. T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP 2010, volume 6183 of LNCS, pages 504-528. Springer, 2010. Google Scholar
  8. Marko Doko and Viktor Vafeiadis. A program logic for C11 memory fences. In VMCAI, volume 9583 of Lecture Notes in Computer Science, pages 413-430. Springer, 2016. Google Scholar
  9. Marko Doko and Viktor Vafeiadis. Tackling real-life relaxed concurrency with FSL++. In ESOP, 2017. Google Scholar
  10. Derek Dreyer. The RustBelt project. URL: http://plv.mpi-sws.org/rustbelt/.
  11. Xinyu Feng. Local rely-guarantee reasoning. In POPL, pages 315-327, 2009. Google Scholar
  12. C. B. Jones. Tentative steps toward a development method for interfering programs. TOPLAS, 5(4):596-619, 1983. Google Scholar
  13. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In ICFP, pages 256-269, 2016. Google Scholar
  14. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL, pages 637-650, 2015. Google Scholar
  15. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising semantics for relaxed-memory concurrency. In POPL, pages 175-189, 2017. Google Scholar
  16. Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher-order concurrent separation logic. In ESOP, 2017. Google Scholar
  17. Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In POPL, pages 205-217, 2017. Google Scholar
  18. Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL, pages 218-231, 2017. Google Scholar
  19. Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming release-acquire consistency. In POPL, POPL 2016, pages 649-662. ACM, 2016. Google Scholar
  20. Ori Lahav and Viktor Vafeiadis. Owicki-Gries reasoning for weak memory models. In Automata, Languages, and Programming, ICALP 2015, volume 9135 of LNCS, pages 311-323. Springer, 2015. Google Scholar
  21. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. Google Scholar
  22. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In VMCAI, pages 41-62, 2016. Google Scholar
  23. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, 2014. Google Scholar
  24. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. Google Scholar
  25. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002. Google Scholar
  26. Tom Ridge. A rely-guarantee proof system for x86-TSO. In VSTTE 2010, volume 6217 of LNCS, pages 55-70. Springer, 2010. Google Scholar
  27. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, pages 77-87, 2015. Google Scholar
  28. Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. A separation logic for fictional sequential consistency. In ESOP 2015, volume 9032 of LNCS, pages 736-761. Springer, 2015. Google Scholar
  29. Alexander Summers. Personal communication, 2017. Google Scholar
  30. Kasper Svendsen and Lars Birkedal. Impredicative concurrent abstract predicates. In ESOP, 2014. Google Scholar
  31. Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis. Verifying read-copy-update in a logic for weak memory. In 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pages 110-120. ACM, 2015. Google Scholar
  32. Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. ACM, 2013. Google Scholar
  33. Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA, OOPSLA 2014, pages 691-707. ACM, 2014. Google Scholar
  34. Viktor Vafeiadis and Chinmay Narayan. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA 2013, pages 867-884. ACM, 2013. Google Scholar
  35. Viktor Vafeiadis and Matthew Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR 2007, volume 4703 of LNCS, pages 256-271. Springer, 2007. 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 About DROPS Imprint Privacy Contact