research-article

Syntactic control of interference for separation logic

Authors:

John C. ReynoldsAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 323 - 336

https://doi.org/10.1145/2103621.2103695

Published: 25 January 2012 Publication History

Abstract

Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.

Supplementary Material

JPG File (popl_5a_3.jpg)

Download
16.36 KB

ZIP File (popl233.zip)

The file popl233-reddy-supplemental.pdf contains the technical appendix for the paper "Syntactic Control of Interference for Separation Logic" by Uday S. Reddy and John C. Reynolds.

Download
149.34 KB

MP4 File (popl_5a_3.mp4)

Download
218.59 MB

References

[1]

S. Abramsky and G. McCusker. Linearity, sharing and state. In Algol-like Languages tOT, chapter 20.

[2]

S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In LICS 1998, pages 334--344, 1998.

Digital Library

[3]

K. R. Apt. Ten years of Hoare's logic: A survey. ACM Trans. Program. Lang. Syst., 3 (4): 431--483, Oct. 1981.

Digital Library

[4]

J. Berdine and I. Wehrman. Variable conditions and CSL. Private communication, 4th April, 2011.

[5]

K. Bierhoff. API protocol compliance in object-oriented software. Technical Report Carnegie Mellon University-ISR-09--108, Carnegie-Mellon University, Apr 2009.

[6]

R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in Separation Logic. In ACM Symp. on Princ. of Program. Lang., pages 59--70. ACM Press, 2005.

Digital Library

[7]

R. Bornat, C. Calcagno, and H. Yang. Variables as resource in Separation Logic. In Proc. 22nd Ann. Conf. on Math. Found. of Program. Semantics (MFPS XXII) MFPS 06, pages 247--276.

Digital Library

[8]

J. Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis: 10th Intern. Symp., volume 2694 of LNCS, pages 55--72. Springer, 2003.

Digital Library

[9]

973)}Brinch-Hansen-monitorsP. Brinch Hansen. Operating System Principles. Prentice-Hall, Englewood Cliffs, 1973.

Digital Library

[10]

P. Brinch Hansen. Structured multiprogramming. Comm. ACM, 15: 574--577, July 1972.

Digital Library

[11]

S. D. Brookes. A semantics for Concurrent Separation Logic. Theoretical Comput. Sci., 375 (1--3): 227--270, Apr 2007.

Digital Library

[12]

S. D. Brookes. A revisionist history of Concurrent Separation Logic. In MFPS 2011, pages 5--28.

Digital Library

[13]

S. D. Brookes. Variables as resource for shared-memory programs: Semantics and soundness. In Proc. 22nd Ann. Conf. on Math. Found. of Program. Semantics (MFPS XXII) MFPS 06, pages 123--150.

Digital Library

[14]

L. Damas and R. Milner. Principal type-schemes for functional programs. In ACM Symp. on Princ. of Program. Lang., pages 207--212, 1982.

Digital Library

[15]

J.-Y. Girard. Linear logic. Theoretical Comput. Sci., 50: 1--102, 1987.

Digital Library

[16]

A. Gotsman, J. Berdine, and B. Cook. Precision and the conjunction rule in Concurrent Separation Logic. In MFPS 2011.

Digital Library

[17]

C. A. R. Hoare. Towards a theory of parallel programming. In C. A. R. Hoare and R. H. Perrott, editors, Operating Systems Techniques, pages 61--71. Academic Press, 1972.

[18]

C. A. R. Hoare. Monitors: An operating system structuring concept. Comm. ACM, 17 (10): 549--558, Oct. 1974.

Digital Library

[19]

B. J., C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with Separation Logic. In F. S. de Boer, editor, Formal Methods for Components and Objects, 4th Intern. Symp., volume 4111 of LNCS, pages 115--137. Springer-Verlag, 2005.

Digital Library

[20]

K. Kapoor, K. Lodaya, and U. S. Reddy. Fine grained concurrency with Separation Logic. J. Philosophical Logic, 40 (5): 583--632, Oct 2011. 10.1007/s10992-011--9195--1.

[21]

M. Main, A. Melton, and M. Mislove. Proc. 22nd Ann. Conf. on Math. Found. of Program. Semantics (MFPS XXII), volume 158 of Elect. Notes in Theor. Comput. Sci. Elsevier, 2006.

[22]

G. McCusker. A graph model for imperative computation. Logical Methods in Comp. Sci., 6 (1--2), Jan 2010.

[23]

R. Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17: 348--375, 1978.

[24]

M. Mislove and J. Ouaknine, editors. Proc. 27nd Ann. Conf. on Math. Found. of Program. Semantics (MFPS XXVII), volume 276 of Elect. Notes in Theor. Comput. Sci. Elsevier, 2011.

[25]

P. W. O'Hearn. Resources, concurrency and local reasoning. Theoretical Comput. Sci., 375 (1--3): 271--307, May 2007.

Digital Library

[26]

P. W. O'Hearn. Linear logic and interference control. In Category Theory and Computer Science, volume 350 of LNCS, pages 74--93. Springer-Verlag, 1991.

Digital Library

[27]

P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin Symbolic Logic, 5 (2): 215--244, June 1999.

[28]

P. W. O'Hearn and R. D. Tennent. Algol-like Languages (Two volumes). Birkhauser, Boston, 1997.

Digital Library

[29]

P. W. O'Hearn, A. J. Power, M. Takeyama, and R. D. Tennent. Syntactic control of interference revisited. In S. D. Brookes, M. Main, A. Melton, and M. Mislove, editors, Math. Found. of Program. Semantics: Eleventh Ann. Conference, volume 1 of Elect. Notes in Theor. Comput. Sci. Elsevier, 1995. (Reprinted as Chapter 18 of OT).

[30]

P. W. O'Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In L. Fribourg, editor, CSL 2001, volume 2142 of LNCS, pages 1--19, Berlin, 2001. Springer-Verlag.

Digital Library

[31]

S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Comm. ACM, 19 (5): 279--285, May 1976.

Digital Library

[32]

M. Parkinson, R. Bornat, and Calcagno. Variables as resource in Hoare Logics. In Symp. on Logic in Comput. Sci., pages 137--146. IEEE, 2006.

Digital Library

[33]

U. S. Reddy. Global state considered unnecessary: An introduction to object-based semantics. J. Lisp and Symbolic Computation, 9: 7--76, 1996. (Reprinted as Chapter 19 of OT).

[34]

J. Reynolds. Separation Logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002.

Digital Library

[35]

J. C. Reynolds. A problematic program (joint work with Josh Berdine). Presentation at the Dagstuhl workshop on Types, Logics and Semantics for State, 2008.

[36]

J. C. Reynolds. Syntactic control of interference. In ACM Symp. on Princ. of Program. Lang., pages 39--46. ACM, 1978. (Reprinted as Chapter 10 of OT).

Digital Library

[37]

J. C. Reynolds. Idealized Algol and its specification logic. In D. Neel, editor, Tools and Notions for Program Construction, pages 121--161. Cambridge Univ. Press, 1982. (Reprinted as Chapter 6 of OT).

[38]

V. Vafeiadis. Concurrent Separation Logic and operational semantics. In MFPS 2011.

[39]

H. Yang and P. W. O'Hearn. A semantics basis for local reasoning. In FOSSACS, pages 402--416, Berlin, 2002. Springer-Verlag.

Digital Library

[40]

H. Yasuoka and T. Terauchi. Polymorphic fractional capabilities. In Static Analysis Symposium/Workshop on Static Analysis, pages 36--51, 2009. 10.1007/978--3--642-03237-0_5.

Digital Library

Cited By

El-Zawawy M(2015)Boosting the Software Quality of Parallel Programming Using Logical MeansComputational Science and Its Applications -- ICCSA 201510.1007/978-3-319-21413-9_8(101-116)Online publication date: 19-Jun-2015
https://doi.org/10.1007/978-3-319-21413-9_8
Ştefănescu ACiobâcă ŞMereuta RMoore BŞerbănută TRoşu G(2014)All-Path Reachability LogicRewriting and Typed Lambda Calculi10.1007/978-3-319-08918-8_29(425-440)Online publication date: 2014
https://doi.org/10.1007/978-3-319-08918-8_29
Lei JQiu Z(2014)Modular Reasoning for Message-Passing ProgramsTheoretical Aspects of Computing – ICTAC 201410.1007/978-3-319-10882-7_17(277-294)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10882-7_17
Show More Cited By

Index Terms

Syntactic control of interference for separation logic
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics
      1. Denotational semantics

Recommendations

Syntactic control of interference for separation logic
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
436
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)3

Reflects downloads up to 08 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

El-Zawawy M(2015)Boosting the Software Quality of Parallel Programming Using Logical MeansComputational Science and Its Applications -- ICCSA 201510.1007/978-3-319-21413-9_8(101-116)Online publication date: 19-Jun-2015
https://doi.org/10.1007/978-3-319-21413-9_8
Ştefănescu ACiobâcă ŞMereuta RMoore BŞerbănută TRoşu G(2014)All-Path Reachability LogicRewriting and Typed Lambda Calculi10.1007/978-3-319-08918-8_29(425-440)Online publication date: 2014
https://doi.org/10.1007/978-3-319-08918-8_29
Lei JQiu Z(2014)Modular Reasoning for Message-Passing ProgramsTheoretical Aspects of Computing – ICTAC 201410.1007/978-3-319-10882-7_17(277-294)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10882-7_17
Ley-Wild RNanevski A(2013)Subjective auxiliary state for coarse-grained concurrencyACM SIGPLAN Notices10.1145/2480359.242913448:1(561-574)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429134
Ley-Wild RNanevski AGiacobazzi RCousot R(2013)Subjective auxiliary state for coarse-grained concurrencyProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429134(561-574)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429134
Gordon CParkinson MParsons JBromfield ADuffy J(2012)Uniqueness and reference immutability for safe parallelismACM SIGPLAN Notices10.1145/2398857.238461947:10(21-40)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384619
Gordon CParkinson MParsons JBromfield ADuffy JLeavens GDwyer M(2012)Uniqueness and reference immutability for safe parallelismProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384619(21-40)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384619
Brookes S(2012)Syntactic Control of Interference and Concurrent Separation LogicElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2012.08.007286(87-102)Online publication date: 1-Sep-2012
https://dl.acm.org/doi/10.1016/j.entcs.2012.08.007
Le DChin WTeo Y(2012)Variable permissions for concurrency verificationProceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering10.1007/978-3-642-34281-3_4(5-21)Online publication date: 12-Nov-2012
https://dl.acm.org/doi/10.1007/978-3-642-34281-3_4

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents