More Web Proxy on the site http://driver.im/

research-article

Open access

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs

Authors:

Benjamin Lucien Kaminski,

Joost-Pieter Katoen,

Christoph Matheja,

Thomas NollAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 34, Pages 1 - 29

https://doi.org/10.1145/3290347

Published: 02 January 2019 Publication History

Abstract

We present quantitative separation logic (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, separating conjunction and separating implication, are lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness, etc.

Furthermore, we develop a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in QSL. This calculus is a conservative extension of both Ishtiaq’s, O’Hearn’s and Reynolds’ separation logic for heap-manipulating programs and Kozen’s / McIver and Morgan’s weakest preexpectations for probabilistic programs. Soundness is proven with respect to an operational semantics based on Markov decision processes. Our calculus preserves O’Hearn’s frame rule, which enables local reasoning. We demonstrate that our calculus enables reasoning about quantities such as the probability of terminating with an empty heap, the probability of reaching a certain array permutation, or the expected length of a list.

Supplementary Material

WEBM File (a34-matheja.webm)

Download
76.59 MB

References

[1]

Susanne Albers and Marek Karpinski. 2002. Randomized splay trees: Theoretical and experimental results. Inf. Process. Lett. 81, 4 (2002), 213–221.

Digital Library

[2]

Krzysztof R Apt and Gordon D Plotkin. 1986. Countable nondeterminism and random assignment. Journal of the ACM (JACM) 33, 4 (1986), 724–767.

Digital Library

[3]

Cecilia R. Aragon and Raimund Seidel. 1989. Randomized Search Trees. In FOCS. 540–545.

Digital Library

[4]

Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science 7, 2 (2011).

[5]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.

Digital Library

[6]

Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An AssertionBased Program Logic for Probabilistic Programs. In ESOP 2018. 117–144.

[7]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2012. Probabilistic Relational Hoare Logics for ComputerAided Security Proofs. In MPC. 1–6.

Digital Library

[8]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018. Quantitative Separation Logic. CoRR abs/1802.10467 (2018). arXiv: 1802.10467 http://arxiv.org/abs/1802.10467

[9]

Guy E. Blelloch and Margaret Reid-Miller. 1998. Fast Set Operations Using Treaps. In SPAA. 16–26.

Digital Library

[10]

Marius Bozga, Radu Iosif, and Swann Perarnau. 2010. Quantitative Separation Logic and Programs with Lists. J. Autom. Reasoning 45, 2 (2010), 131–156.

Digital Library

[11]

James Brotherston. 2007. Formalised Inductive Reasoning in the Logic of Bunched Implications. In SAS. 87–103.

Digital Library

[12]

Michael Carbin, Sasa Misailovic, and Martin C. Rinard. 2016. Verifying quantitative reliability for programs that execute on unreliable hardware. Commun. ACM 59, 8 (2016), 83–91.

Digital Library

[13]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV (LNCS), Vol. 8044. Springer, 511–526.

[14]

Bor-Yuh Evan Chang and Xavier Rival. 2008. Relational inductive shape analysis. In POPL. 247–260.

Digital Library

[15]

Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In POPL. ACM, 327–342.

Digital Library

[16]

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. 2012. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77, 9 (2012), 1006–1036.

Digital Library

[17]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press. http://mitpress.mit.edu/books/introduction- algorithms

Digital Library

[18]

Patrick Cousot and Radhia Cousot. 1979. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math. 82, 1 (1979), 43–57.

[19]

Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice–Hall.

[20]

Rusins Freivalds. 1977. Probabilistic Machines Can Use Less Running Time. In IFIP Congress, Vol. 839. 842.

[21]

Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2014. Operational versus Weakest Pre-Expectation Semantics for the Probabilistic Guarded Command Language. Performance Evaluation 73 (2014), 110–132.

Digital Library

[22]

Thomas A. Henzinger. 2013. Quantitative reactive modeling and verification. Computer Science - R&D 28, 4 (2013), 331–344.

Digital Library

[23]

Wim H. Hesselink. 1993. Proof Rules for Recursive Procedures. Formal Asp. Comput. 5, 6 (1993), 554–570.

Digital Library

[24]

Charles Antony Richard Hoare. 1962. Quicksort. Comput. J. 5, 1 (1962), 10–15.

[25]

Charles Antony Richard Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580.

Digital Library

[26]

Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In POPL. 14–26.

Digital Library

[27]

Claire Jones. 1990. Probabilistic Non–Determinism. Ph.D. Dissertation. University of Edinburgh, UK.

[28]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs. In ESOP (LNCS), Vol. 9632. Springer, 364–389.

[29]

Donald Ervin Knuth. 1992. Two Notes on Notation. The American Mathematical Monthly 99, 5 (1992), 403–422.

Digital Library

[30]

Dexter Kozen. 1979. Semantics of Probabilistic Programs. In FOCS. 101–114.

Digital Library

[31]

Dexter Kozen. 1983. A Probabilistic PDL. In STOC. 291–297.

Digital Library

[32]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205–217.

Digital Library

[33]

Stephen Magill, Aleksandar Nanevski, Edmund Clarke, and Peter Lee. 2006. Inferring invariants in separation logic for imperative list-processing programs. SPACE 1, 1 (2006), 5–7.

[34]

Conrado Martínez and Salvador Roura. 1998. Randomized Binary Search Trees. J. ACM 45, 2 (1998), 288–323.

Digital Library

[35]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer.

Digital Library

[36]

Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. PACMPL 2, POPL (2018), 33:1–33:28.

Digital Library

[37]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. Trans. on Programming Languages and Systems 18, 3 (1996), 325–353.

Digital Library

[38]

Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI. 496–512.

Digital Library

[39]

Peter W. O’Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification. 286–318.

[40]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In LICS. 672–681.

Digital Library

[41]

William Pugh. 1990. Skip Lists: A Probabilistic Alternative to Balanced Trees. Commun. ACM 33, 6 (1990), 668–676.

Digital Library

[42]

Martin Lee Puterman. 2005. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons.

[43]

John Charles Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55–74.

Digital Library

[44]

Dana Scott. 2008. The Algebraic Intepretation of Quantifiers. Intuitionistic and Classical. Andrzej Mostowski and Foundational Studies (2008), 289–312.

[45]

Joseph Tassarotti and Robert Harper. 2018. A Separation Logic for Concurrent Randomized Programs. CoRR abs/1802.02951 (2018). arXiv: 1802.02951 http://arxiv.org/abs/1802.02951

Digital Library

[46]

Hongseok Yang and Peter W. O’Hearn. 2002. A Semantic Basis for Local Reasoning. In FOSSACS. 402–416.

Digital Library

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Zilberstein NSaliling ASilva A(2024)Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational EffectsProceedings of the ACM on Programming Languages10.1145/36498218:OOPSLA1(276-304)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649821
Show More Cited By

Index Terms

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
1. Theory of computation

Recommendations

Pointer analysis and separation logic
Quantitative Separation Logic and Programs with Lists

This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine et al. (2004). Our main extension consists in introducing atomic formulae of the form ls ^k( x , y ) describing a list ...
Semantics for disjunctive logic programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
949
Total Downloads

Downloads (Last 12 months)180
Downloads (Last 6 weeks)11

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Zilberstein NSaliling ASilva A(2024)Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational EffectsProceedings of the ACM on Programming Languages10.1145/36498218:OOPSLA1(276-304)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649821
Batz KBiskup TKatoen JWinkler T(2024)Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36329358:POPL(2792-2820)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632935
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Schröer PRandone FPardo RWa̧sowski A(2024)Symbolic Quantitative Information Flow for Probabilistic ProgramsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_6(128-154)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_6
Batz KKaminski BMatheja CWinkler T(2024)J-P: MDP. FP. PPPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_11(255-302)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_11
Schröer PBatz KKaminski BKatoen JMatheja C(2023)A Deductive Verification Infrastructure for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36228707:OOPSLA2(2052-2082)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622870
Avanzini MMoser GSchaper M(2023)Automated Expected Value Analysis of Recursive ProgramsProceedings of the ACM on Programming Languages10.1145/35912637:PLDI(1050-1072)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591263
Li JAhmed AHoltzen S(2023)Lilac: A Modal Separation Logic for Conditional ProbabilityProceedings of the ACM on Programming Languages10.1145/35912267:PLDI(148-171)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591226
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents