## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Local Action and Abstract Separation Logic

LICS, pp.366-378, (2007)

EI

Keywords

Abstract

Separation logic is an extension of Hoare's logic which supports a local way of reasoning about programs that mutate memory. We present a study of the semantic structures lying behind the logic. The core idea is of a local action, a state transformer that mutates the state in a local way. We formulate local actions for a class of models c...More

Code:

Data:

Introduction

- Separation logic is an extension of Hoare’s logic which has been used to attack the old problem of reasoning about the mutation of data structures in memory [33, 17, 23, 34].
- Separation logic derives its power from an interplay between the separating conjunction connective ∗ and proof rules for commands that use ∗.
- Chief among these are the frame rule [17, 23] and the concurrency rule [22].
- The concurrency rule states that processes that operate on separate resources can be reasoned about independently

Highlights

- Separation logic is an extension of Hoare’s logic which has been used to attack the old problem of reasoning about the mutation of data structures in memory [33, 17, 23, 34]
- Our purpose in this paper is to describe these semantic assumptions in a general way, for a collection of models that abstract away from the RAM and other concrete models used in work on separation logic
- Separation algebras are a special case of the models in [30], corresponding to Boolean BI algebras
- The second precursor is [37], which identified Safety Monotonicity and the Frame Property, conditions on an operational semantics corresponding to the frame rule
- The formulation of the best state transformers (Definition 10) is much simpler and easier to understand than its relational cousin in [25]

Conclusion

**Conclusion and Related**

Work

There are three main precursors to this work. The first is the model theory of BI [24, 31], which Pym emphasized can be understood as providing a general model of resource.- In comparison to [37] the main step forward – apart from concurrency and consideration of a class of models rather than a single one – is the use of functions into the poset P (Σ) instead of relations satisfying Safety Monotonicity and the Frame Property.
- This shift has led to dramatic simplifications.
- The formulation of the best state transformers (Definition 10) is much simpler and easier to understand than its relational cousin in [25]

Funding

- We are grateful to Philippa Gardner and Martin Hyland for trenchant criticisms at decisive points in this work. We acknowledge the financial support of the EPSRC

Reference

- A. Ahmed, L. Jia, and D. Walker. Reasoning about hierarchical storage. In 18th LICS, pp33-44, 2003.
- M. Barnett, R. DeLine, M. Fahndrich, K.R.M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27–56, 2004.
- N. Benton. Abstracting allocation. In CSL 2006, pp182–196, 2006.
- J. Berdine, C. Calcagno, and P.W. O’Hearn. Smallfoot: Automatic modular assertion checking with separation logic. In 4th FMCO, pp115-137, 2006.
- J. Berdine, B. Cook, D. Distefano, and P. O’Hearn. Automatic termination proofs for programs with shape-shifting heaps. In 18th CAV, pp386-400, 2006.
- L. Birkedal and N. Torp-Smith. Higher-order separation logic and abstraction. submitted.
- L. Birkedal and H. Yang. Relational parametricity and separation logic. In 10th FOSSACS, LNCS 4423, pp93–107, 2007.
- R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In 32nd POPL, pp59–70, 2005.
- R. Bornat, C. Calcagno, and H. Yang. Variables as resource in separation logic. In 21st MFPS, pp247–276, 2005.
- S. Brookes. A grainless semantics for parallel programs with shared mutable data. In 21st MFPS, pp277-307, 2005.
- S. Brookes. Variables as resource for shared-memory programs: Semantics and soundness. In 22nd MFPS, pp123–150, 2006.
- S. D. Brookes. A semantics for concurrent separation logic. Proceedings of the 15th CONCUR, London. August, 2004.
- C. Calcagno, P. O’Hearn, and H. Yang. Local Action and Abstract Separation Logic (Longer version). www.dcs.qmul.ac.uk/∼ohearn/papers/asl-long.pdf, 2007.
- C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In 32nd POPL, pp271-282, 2005.
- X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In 16th ESOP, to appear, 2007.
- J. Hayman and G. Winskel. Independence and concurrent separation logic. In 21st LICS, pp147-156, 2006.
- S. Isthiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. In 28th POPL, pages 36–49, 2001.
- I. Mijajlovic, N. Torp-Smith, and P. O’Hearn. Refinement and separation contexts. Proceedings of FSTTCS, 2004.
- E. Moggi. Notions of computation and monads. Information and Computation 93(1), pp55-92, 1991.
- A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare type theory. In ICFP 2006, pages 62–73, 2006.
- D. A. Naumann and M. Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. In 19th LICS, 2004.
- P. O’Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), pp271-307, May 2007. (Preliminary version appeared in CONCUR’04, LNCS 3170, 49–67.)
- P. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In 15th CSL, pp1–19, 2001.
- P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 99.
- P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In 31st POPL, pages 268–280, 2004.
- M. Parkinson and G. Bierman. Separation logic and abstraction. In 32nd POPL, pp59–70, 2005.
- M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. In 21st LICS, 2006.
- M. Parkinson, R. Bornat, and P. O’Hearn. Modular verification of a non-blocking stack. In 34th POPL, 2007.
- A.J. Power and E.P. Robinson. Premonoidal categories and notions of computation. Math. Struct. Comp. Sci. 7(5), pp453-468, 1997.
- D. Pym, P. O’Hearn, and H. Yang. Possible worlds and resources: the semantics of BI. Theoretical Computer Science, 315(1):257– 305, 2004.
- D.J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Applied Logic Series, 2002.
- W. Reisig. Petri nets. EATCS Monographs, vol. 4, 1995.
- J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pp 303– 321, 2000. Palgrave.
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th LICS, pp 55-74, 2002.
- N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its abstractions. 32nd POPL, pp296–309, 2005.
- N. Torp-Smith, L. Birkedal, and J. Reynolds. Local reasoning about a copying garbage collector. In 31st POPL, pp220–231, 2004.
- H. Yang and P. O’Hearn. A semantic basis for local reasoning. In 5th FOSSACS, LNCS 2303, 2002.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn