research-article

Open access

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic

Authors:

Lennard Gäher,

Daniel Gratzer,

Joseph Tassarotti,

Robbert Krebbers,

Lars BirkedalAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 80 - 95

https://doi.org/10.1145/3453483.3454031

Published: 18 June 2021 Publication History

Abstract

Step-indexed separation logic has proven to be a powerful tool for modular reasoning about higher-order stateful programs. However, it has only been used to reason about safety properties, never liveness properties. In this paper, we observe that the inability of step-indexed separation logic to support liveness properties stems fundamentally from its failure to validate the existential property, connecting the meaning of existential quantification inside and outside the logic. We show how to validate the existential property—and thus enable liveness reasoning—by moving from finite step-indices (natural numbers) to transfinite step-indices (ordinals). Concretely, we transform the Coq-based step-indexed logic Iris to Transfinite Iris, and demonstrate its effectiveness in proving termination and termination-preserving refinement for higher-order stateful programs.

References

[1]

Amal Ahmed. 2004. Semantics of types for mutable state. Ph.D. Dissertation. Princeton University.

Digital Library

[2]

Amal Ahmed, Andrew W. Appel, and Roberto Virga. 2002. A stratified semantics of general references. In LICS. 75–86. https://doi.org/10.1109/LICS.2002.1029818

[3]

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence. In POPL. 340–353. https://doi.org/10.1145/1480881.1480925

Digital Library

[4]

Pierre America and Jan Rutten. 1989. Solving reflexive domain equations in a category of complete metric spaces. JCSS, 39, 3 (1989), 343–375. https://doi.org/10.1016/0022-0000(89)90027-5

[5]

Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press. isbn:110704801X

Digital Library

[6]

Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23, 5 (2001), 657–683. https://doi.org/10.1145/504709.504712

Digital Library

[7]

Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. 2007. A very modal model of a modern, major, general type system. In POPL. 109–122. https://doi.org/10.1145/1190216.1190235

Digital Library

[8]

Robert Atkey. 2010. Amortised resource analysis with separation logic. In ESOP (LNCS, Vol. 6012). 85–103. https://doi.org/10.1007/978-3-642-11957-6_6

Digital Library

[9]

Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. 2021. Diamonds are not forever: liveness in reactive programming with guarded recursion. PACMPL, 5, POPL (2021), 1–28. https://doi.org/10.1145/3434283

Digital Library

[10]

Lars Birkedal, Ales Bizjak, and Jan Schwinghammer. 2013. Step-indexed relational reasoning for countable nondeterminism. LMCS, 9, 4 (2013), https://doi.org/10.2168/LMCS-9(4:4)2013

[11]

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2011. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. In LICS. 55–64. https://doi.org/10.1109/LICS.2011.16

Digital Library

[12]

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. 2011. Step-indexed Kripke models over recursive worlds. In POPL. 119–132. https://doi.org/10.1145/1926385.1926401

Digital Library

[13]

Ales Bizjak, Lars Birkedal, and Marino Miculan. 2014. A model of countable nondeterminism in guarded type theory. In RTA-TLCA (LNCS, Vol. 8560). 108–123. https://doi.org/10.1007/978-3-319-08918-8_8

[14]

Michael C. Browne, Edmund M. Clarke, and Orna Grumberg. 1988. Characterizing finite Kripke structures in propositional temporal logic. TCS, 59 (1988), 115–131. https://doi.org/10.1016/0304-3975(88)90098-9

Digital Library

[15]

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A separation logic tool to verify correctness of C programs. JAR, 61, 1-4 (2018), 367–422. https://doi.org/10.1007/s10817-018-9457-5

Digital Library

[16]

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2019. Verifying concurrent, crash-safe systems with Perennial. In SOSP. 243–258. https://doi.org/10.1145/3341301.3359632

Digital Library

[17]

Arthur Charguéraud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. 418–430. https://doi.org/10.1145/2034773.2034828

Digital Library

[18]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In ECOOP (LNCS, Vol. 8586). 207–231. https://doi.org/10.1007/978-3-662-44202-9_9

Digital Library

[19]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular termination verification for non-blocking concurrency. In ESOP (LNCS, Vol. 9632). 176–201. https://doi.org/10.1007/978-3-662-49498-1_8

[20]

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2020. RustBelt meets relaxed memory. PACMPL, 4, POPL (2020), 34:1–34:29. https://doi.org/10.1145/3371102

Digital Library

[21]

Robert Dockins and Aquinas Hobor. 2010. A theory of termination via indirection. In Modelling, Controlling and Reasoning About State (Dagstuhl Seminar Proceedings, Vol. 10351). http://drops.dagstuhl.de/opus/volltexte/2010/2805/

[22]

Robert Dockins and Aquinas Hobor. 2012. Time bounds for general function pointers. 286 (2012), 139–155. https://doi.org/10.1016/j.entcs.2012.08.010

Digital Library

[23]

Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner, and Julian Sutherland. 2019. TaDA Live: Compositional reasoning for termination of fine-grained concurrent programs. arxiv:1901.05750

[24]

Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS, 7, 2:16 (2011), June, 1–37. https://doi.org/10.2168/LMCS-7(2:16)2011

[25]

Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In POPL. 185–198. https://doi.org/10.1145/1706299.1706323

Digital Library

[26]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A mechanised relational logic for fine-grained concurrency. In LICS. 442–451. https://doi.org/10.1145/3209108.3209174

Digital Library

[27]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021. Compositional non-interference for fine-grained concurrent programs. To appear in S&P’21.

[28]

Pietro Di Gianantonio and Marino Miculan. 2004. Unifying recursive and co-recursive definitions in sheaf categories. In FOSSACS (LNCS, Vol. 2987). 136–150. https://doi.org/10.1007/978-3-540-24727-2_11

[29]

Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020. Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris. PACMPL, 4, ICFP (2020), 114:1–114:29. https://doi.org/10.1145/3408996

Digital Library

[30]

Gerhard Hessenberg. 1906. Grundbegriffe der Mengenlehre. 1, Vandenhoeck & Ruprecht.

[31]

Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP (LNCS, Vol. 4960). 353–367. https://doi.org/10.1007/978-3-540-78739-6_27

[32]

Iris project. 2021. A higher-order concurrent separation logic framework implemented and verified in the proof assistant Coq. https://iris-project.org/

[33]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: Securing the foundations of the Rust programming language. PACMPL, 2, POPL (2018), 66:1–66:34. https://doi.org/10.1145/3158154

Digital Library

[34]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2021. Safe systems programming in Rust. CACM, 64, 4 (2021), 144–152. https://doi.org/10.1145/3418295

Digital Library

[35]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256–269. https://doi.org/10.1145/2951913.2951943

Digital Library

[36]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP, 28 (2018), e20. https://doi.org/10.1017/S0956796818000151

[37]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. 637–650. https://doi.org/10.1145/2676726.2676980

Digital Library

[38]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In POPL. 175–189. isbn:9781450346603 https://doi.org/10.1145/3009837.3009850

Digital Library

[39]

Dominik Kirst and Gert Smolka. 2018. Large Model Constructions for Second-Order ZF in Dependent Type Theory. In CPP. 228–239. isbn:9781450355865 https://doi.org/10.1145/3167095

Digital Library

[40]

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. PACMPL, 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772

Digital Library

[41]

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The essence of higher-order concurrent separation logic. In ESOP (LNCS, Vol. 10201). 696–723. https://doi.org/10.1007/978-3-662-54434-1_26

Digital Library

[42]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205–217. https://doi.org/10.1145/3093333.3009855

Digital Library

[43]

Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. 2017. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL. 218–231. https://doi.org/10.1145/3093333.3009877

Digital Library

[44]

Vladimir Iosifovich Levenshtein. 1965. Binary codes capable of correcting deletions, insertions, and reversals. Soviet Physics Doklady, 10 (1965), 707–710.

[45]

Hongjin Liang and Xinyu Feng. 2016. A program logic for concurrent objects under fair scheduling. In POPL. 385–399. https://doi.org/10.1145/2837614.2837635

Digital Library

[46]

Hongjin Liang and Xinyu Feng. 2018. Progress of concurrent objects with partial methods. PACMPL, 2, POPL (2018), 20:1–20:31. https://doi.org/10.1145/3158108

Digital Library

[47]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019. Time credits and time receipts in Iris. In ESOP (LNCS, Vol. 11423). 3–29. https://doi.org/10.1007/978-3-030-17184-1_1

[48]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2020. Cosmo: A concurrent separation logic for Multicore OCaml. PACMPL, 4, ICFP (2020), 96:1–96:29. https://doi.org/10.1145/3408978

Digital Library

[49]

Hiroshi Nakano. 2000. A modality for recursion. In LICS. 255–266. https://doi.org/10.1109/LICS.2000.855774

[50]

Peter W. O’Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic, 5, 2 (1999), 215–244. https://doi.org/10.2307/421090

[51]

Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In CSL (LNCS, Vol. 2142). 1–19. https://doi.org/10.1007/3-540-44802-0_1

[52]

Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2021. Transfinite Iris appendix and Coq development. https://iris-project.org/transfinite-iris/

[53]

Simon Spies, Neel Krishnaswami, and Derek Dreyer. 2021. Transfinite step-indexing for termination. PACMPL, 5, POPL (2021), 1–29. https://doi.org/10.1145/3434294

Digital Library

[54]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP (LNCS, Vol. 8410). 149–168. https://doi.org/10.1007/978-3-642-54833-8_9

Digital Library

[55]

Kasper Svendsen, Lars Birkedal, and Matthew J. Parkinson. 2013. Modular reasoning about separation of concurrent data structures. In ESOP (LNCS, Vol. 7792). 169–188. https://doi.org/10.1007/978-3-642-37036-6_11

Digital Library

[56]

Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. 2018. A separation logic for a promising semantics. In ESOP (LNCS, Vol. 10801). 357–384. https://doi.org/10.1007/978-3-319-89884-1_13

[57]

Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. 2016. Transfinite step-indexing: Decoupling concrete and logical steps. In ESOP (LNCS, Vol. 9632). 727–751. https://doi.org/10.1007/978-3-662-49498-1_28

[58]

Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A higher-order logic for concurrent termination-preserving refinement. In ESOP (LNCS, Vol. 10201). 909–936. https://doi.org/10.1007/978-3-662-54434-1_34

Digital Library

[59]

Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. PACMPL, 2, POPL (2018), 64:1–64:28. https://doi.org/10.1145/3158152

Digital Library

[60]

Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. 377–390. https://doi.org/10.1145/2500365.2500600

Digital Library

[61]

Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL. 343–356. https://doi.org/10.1145/2429069.2429111

Digital Library

[62]

Benjamin Werner. 1997. Sets in types, types in sets. In TACS (LNCS, Vol. 1281). 530–346. https://doi.org/10.1007/BFb0014566

[63]

Nobuko Yoshida, Kohei Honda, and Martin Berger. 2007. Logical reasoning for higher-order functions with local state. In FOSSACS (LNCS, Vol. 4423). 361–377. https://doi.org/10.1007/978-3-540-71389-0_26

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Show More Cited By

Index Terms

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic
1. Theory of computation
  1. Logic
    1. Hoare logic
    2. Separation logic

Recommendations

Step-Indexed Kripke Model of Separation Logic for Storable Locks

We present a version of separation logic for modular reasoning about concurrent programs with dynamically allocated storable locks and dynamic thread creation. The assertions of the program logic are modelled by a Kripke model over a recursively de. ned ...
Later credits: resourceful reasoning for the later modality

In the past two decades, step-indexed logical relations and separation logics have both come to play a major role in semantics and verification research. More recently, they have been married together in the form of step-indexed separation logics like ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
506
Total Downloads

Downloads (Last 12 months)156
Downloads (Last 6 weeks)34

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Mansky WDu K(2024)An Iris Instance for Verifying CompCert C ProgramsProceedings of the ACM on Programming Languages10.1145/36328488:POPL(148-174)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632848
Lammich P(2024)Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel SortingJournal of Automated Reasoning10.1007/s10817-024-09701-w68:3Online publication date: 19-Jun-2024
https://doi.org/10.1007/s10817-024-09701-w
Guéneau AHostert JSpies SSammler MBirkedal LDreyer D(2023)Melocoton: A Program Logic for Verified Interoperability Between OCaml and CProceedings of the ACM on Programming Languages10.1145/36228237:OOPSLA2(716-744)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622823
Charguéraud AChlipala AErbsen AGruetter S(2023)Omnisemantics: Smooth Handling of NondeterminismACM Transactions on Programming Languages and Systems10.1145/357983445:1(1-43)Online publication date: 8-Mar-2023
https://dl.acm.org/doi/10.1145/3579834
Spies SGäher LTassarotti JJung RKrebbers RBirkedal LDreyer D(2022)Later credits: resourceful reasoning for the later modalityProceedings of the ACM on Programming Languages10.1145/35476316:ICFP(283-311)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547631
Gäher LSammler MSpies SJung RDang HKrebbers RKang JDreyer D(2022)Simuliris: a separation logic framework for verifying concurrent program optimizationsProceedings of the ACM on Programming Languages10.1145/34986896:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498689
Timany AKrebbers RDreyer DBirkedal L(undefined)A Logical Approach to Type SoundnessJournal of the ACM10.1145/3676954
https://dl.acm.org/doi/10.1145/3676954

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents