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

research-article

Open access

A separation logic for concurrent randomized programs

Authors:

Joseph Tassarotti,

Robert HarperAuthors Info & Claims

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

Article No.: 64, Pages 1 - 30

https://doi.org/10.1145/3290377

Published: 02 January 2019 Publication History

Abstract

We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

Supplementary Material

WEBM File (a64-tassarotti.webm)

Download
94.66 MB

References

[1]

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In ESOP. 214–241.

[2]

Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press.

Digital Library

[3]

Philippe Audebaud and Christine Paulin-Mohring. 2009. Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74, 8 (2009), 568–589.

Digital Library

[4]

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. 2015. Relational Reasoning via Probabilistic Coupling. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings. 387–401.

Digital Library

[5]

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017a. Proving uniformity and independence by self-composition and coupling. In LPAR.

[6]

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. 2017b. *-Liftings for Differential Privacy. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland. 102:1–102:12.

[7]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In ICALP. 107:1–107:15.

[8]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2012. Probabilistic Relational Hoare Logics for ComputerAided Security Proofs. In Mathematics of Program Construction - 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012. Proceedings. 1–6.

Digital Library

[9]

Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017c. Coupling proofs are probabilistic product programs. In POPL. 161–174.

Digital Library

[10]

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

[11]

Jon Beck. 1969. Distributive laws. In Seminar on Triples and Categorical Homology Theory, B. Eckmann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 119–140.

[12]

Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In POPL.

Digital Library

[13]

Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 279–294.

[14]

Silas Boyd-Wickizer, Austin T. Clements, Yandong Mao, Aleksey Pesterev, M. Frans Kaashoek, Robert Tappan Morris, and Nickolai Zeldovich. 2010. An Analysis of Linux Scalability to Many Cores. In 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings. 1–16.

Digital Library

[15]

John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. 55–72.

Digital Library

[16]

Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. http://mitpress.mit.edu/books/certified- programming- dependent- types

Digital Library

[17]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP. 207–231.

Digital Library

[18]

Dave Dice, Yossi Lev, and Mark Moir. 2013. Scalable statistics counters. In SPAA. 43–52.

Digital Library

[19]

Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18, 8 (1975), 453–457.

Digital Library

[20]

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: Compositional reasoning for concurrent programs. In POPL.

Digital Library

[21]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP. 504–528.

Digital Library

[22]

Xinyu Feng. 2009. Local rely-guarantee reasoning. In POPL. 315–327.

Digital Library

[23]

Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP. 173–188.

Digital Library

[24]

Philippe Flajolet. 1985. Approximate Counting: A Detailed Analysis. BIT 25, 1 (1985), 113–134.

Digital Library

[25]

Keir Fraser. 2004. Practical lock-freedom. Ph.D. Dissertation. University of Cambridge.

[26]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. 442–451.

Digital Library

[27]

Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In CONCUR. 388–402.

Digital Library

[28]

Jeremy Gibbons and Ralf Hinze. 2011. Just do it: simple monadic equational reasoning. In ICFP. 2–14.

Digital Library

[29]

Wojciech M. Golab, Lisa Higham, and Philipp Woelfel. 2011. Linearizable implementations do not suffice for randomized distributed computation. In Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011. 373–382.

Digital Library

[30]

Jean Goubault-Larrecq. 2007. Continuous Previsions. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 542–557.

Digital Library

[31]

Jean Goubault-Larrecq. 2015. Full abstraction for non-deterministic and probabilistic extensions of PCF I: The angelic cases. J. Log. Algebr. Meth. Program. 84, 1 (2015), 155–184.

[32]

Maurice Herlihy, Yossi Lev, Victor Luchangco, and Nir Shavit. 2006. A Provably Correct Scalable Concurrent Skip List (Brief Announcement). In OPODIS.

[33]

Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. TOPLAS 12, 3 (1990), 463–492.

Digital Library

[34]

J. Hsu. 2017. Probabilistic Couplings for Probabilistic Reasoning. ArXiv e-prints (Oct. 2017). arXiv: cs.LO/1710.09951

[35]

Claire Jones. 1990. Probabilistic non-determinism. Ph.D. Dissertation. University of Edinburgh, UK. http://hdl.handle.net/ 1842/413

Digital Library

[36]

C. B. Jones. 1983. Tentative steps toward a development method for interfering programs. TOPLAS 5, 4 (1983), 596–619.

Digital Library

[37]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-Order Ghost State. In ICFP.

Digital Library

[38]

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.

Digital Library

[39]

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

Digital Library

[40]

Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22, 3 (1981), 328–350.

[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. 696–723.

Digital Library

[42]

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.

Digital Library

[43]

T. Lindvall. 2002. Lectures on the Coupling Method. Dover Publications, Incorporated.

[44]

Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. 2016. Probabilistic rely-guarantee calculus. Theor. Comput. Sci. 655 (2016), 120–134.

Digital Library

[45]

Michael W. Mislove. 2000. Nondeterminism and Probabilistic Choice: Obeying the Laws. In CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings. 350–364.

Digital Library

[46]

Michael W. Mislove. 2006. On Combining Probability and Nondeterminism. Electr. Notes Theor. Comput. Sci. 162 (2006), 261–265.

[47]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18, 3 (1996), 325–353.

Digital Library

[48]

Robert Morris. 1978. Counting Large Numbers of Events in Small Registers. Commun. ACM 21, 10 (1978), 840–842.

Digital Library

[49]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In ESOP. 290–310.

Digital Library

[50]

Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. 2008. Hoare type theory, polymorphism and separation. J. Funct. Program. 18, 5-6 (2008), 865–911.

Digital Library

[51]

P.W. O’Hearn. 2007. Resources, concurrency, and local reasoning. TCS 375, 1 (2007), 271–307.

Digital Library

[52]

Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In POST. 53–72.

Digital Library

[53]

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

Digital Library

[54]

Lyle Harold Ramshaw. 1979. Formalizing the Analysis of Algorithms. Ph.D. Dissertation. Stanford University.

[55]

John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS.

Digital Library

[56]

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. 2016. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In OOPSLA. 92–110.

Digital Library

[57]

Wouter Swierstra. 2009. A Hoare Logic for the State Monad. In TPHOLs. 440–451.

Digital Library

[58]

Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP. 909–936.

Digital Library

[59]

Iris Team. 2017. Iris 3.0 Documentation. http://plv.mpi- sws.org/iris/appendix- 3.0.pdf

[60]

Regina Tix, Klaus Keimel, and Gordon D. Plotkin. 2009. Semantic Domains for Combining Probability and Non-Determinism. Electr. Notes Theor. Comput. Sci. 222 (2009), 3–99.

Digital Library

[61]

Jean-Baptiste Tristan, Joseph Tassarotti, and Guy L. Steele Jr. 2015. Efficient Training of LDA on a GP U by Mean-for-Mode Estimation. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015. 59–68.

Digital Library

[62]

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.

Digital Library

[63]

Viktor Vafeiadis. 2007. Modular fine-grained concurrency verification. Ph.D. Dissertation. University of Cambridge.

[64]

V. Vafeiadis and M. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In CONCUR. 256–271.

Digital Library

[65]

Eelis van der Weegen and James McKinna. 2008. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In TYPES. 256–271.

[66]

Daniele Varacca. 2002. The Powerdomain of Indexed Valuations. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. 299.

Digital Library

[67]

Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism. Mathematical Structures in Computer Science 16, 1 (2006), 87–113.

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
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814
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
Show More Cited By

Index Terms

A separation logic for concurrent randomized programs
1. Theory of computation
  1. Logic
    1. Separation logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

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 ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

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 ...
Concurrent Separation Logic and Operational Semantics

This paper presents a new soundness proof for concurrent separation logic (CSL) in terms of a standard operational semantics. The proof gives a direct meaning to CSL judgments, which can easily be adapted to accommodate extensions of CSL, such as ...

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

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
916
Total Downloads

Downloads (Last 12 months)127
Downloads (Last 6 weeks)4

Reflects downloads up to 12 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
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814
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
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
Avanzini MBarthe GGrégoire BMoser GVanoni G(2024)Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security ProofsProceedings of the ACM on Programming Languages10.1145/36498398:OOPSLA1(784-809)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649839
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
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
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
Ileri AZeldovich NChlipala AKaashoek F(2024)Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00041(96-111)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00041
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