AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
Separation algebras are a special case of the models in, corresponding to Boolean BI algebras

Local Action and Abstract Separation Logic

LICS, pp.366-378, (2007)

Cited by: 271|Views89
EI

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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • N. Benton. Abstracting allocation. In CSL 2006, pp182–196, 2006.
    Google ScholarLocate open access versionFindings
  • J. Berdine, C. Calcagno, and P.W. O’Hearn. Smallfoot: Automatic modular assertion checking with separation logic. In 4th FMCO, pp115-137, 2006.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • L. Birkedal and N. Torp-Smith. Higher-order separation logic and abstraction. submitted.
    Google ScholarFindings
  • L. Birkedal and H. Yang. Relational parametricity and separation logic. In 10th FOSSACS, LNCS 4423, pp93–107, 2007.
    Google ScholarLocate open access versionFindings
  • R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In 32nd POPL, pp59–70, 2005.
    Google ScholarLocate open access versionFindings
  • R. Bornat, C. Calcagno, and H. Yang. Variables as resource in separation logic. In 21st MFPS, pp247–276, 2005.
    Google ScholarLocate open access versionFindings
  • S. Brookes. A grainless semantics for parallel programs with shared mutable data. In 21st MFPS, pp277-307, 2005.
    Google ScholarFindings
  • S. Brookes. Variables as resource for shared-memory programs: Semantics and soundness. In 22nd MFPS, pp123–150, 2006.
    Google ScholarLocate open access versionFindings
  • S. D. Brookes. A semantics for concurrent separation logic. Proceedings of the 15th CONCUR, London. August, 2004.
    Google ScholarLocate open access versionFindings
  • 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.
    Findings
  • C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In 32nd POPL, pp271-282, 2005.
    Google ScholarLocate open access versionFindings
  • X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In 16th ESOP, to appear, 2007.
    Google ScholarLocate open access versionFindings
  • J. Hayman and G. Winskel. Independence and concurrent separation logic. In 21st LICS, pp147-156, 2006.
    Google ScholarLocate open access versionFindings
  • S. Isthiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. In 28th POPL, pages 36–49, 2001.
    Google ScholarLocate open access versionFindings
  • I. Mijajlovic, N. Torp-Smith, and P. O’Hearn. Refinement and separation contexts. Proceedings of FSTTCS, 2004.
    Google ScholarLocate open access versionFindings
  • E. Moggi. Notions of computation and monads. Information and Computation 93(1), pp55-92, 1991.
    Google ScholarLocate open access versionFindings
  • A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare type theory. In ICFP 2006, pages 62–73, 2006.
    Google ScholarLocate open access versionFindings
  • D. A. Naumann and M. Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. In 19th LICS, 2004.
    Google ScholarLocate open access versionFindings
  • 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.)
    Google ScholarLocate open access versionFindings
  • P. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In 15th CSL, pp1–19, 2001.
    Google ScholarLocate open access versionFindings
  • P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 99.
    Google ScholarLocate open access versionFindings
  • P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In 31st POPL, pages 268–280, 2004.
    Google ScholarLocate open access versionFindings
  • M. Parkinson and G. Bierman. Separation logic and abstraction. In 32nd POPL, pp59–70, 2005.
    Google ScholarLocate open access versionFindings
  • M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. In 21st LICS, 2006.
    Google ScholarLocate open access versionFindings
  • M. Parkinson, R. Bornat, and P. O’Hearn. Modular verification of a non-blocking stack. In 34th POPL, 2007.
    Google ScholarLocate open access versionFindings
  • A.J. Power and E.P. Robinson. Premonoidal categories and notions of computation. Math. Struct. Comp. Sci. 7(5), pp453-468, 1997.
    Google ScholarLocate open access versionFindings
  • D. Pym, P. O’Hearn, and H. Yang. Possible worlds and resources: the semantics of BI. Theoretical Computer Science, 315(1):257– 305, 2004.
    Google ScholarLocate open access versionFindings
  • D.J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Applied Logic Series, 2002.
    Google ScholarLocate open access versionFindings
  • W. Reisig. Petri nets. EATCS Monographs, vol. 4, 1995.
    Google ScholarLocate open access versionFindings
  • J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pp 303– 321, 2000. Palgrave.
    Google ScholarFindings
  • J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th LICS, pp 55-74, 2002.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • N. Torp-Smith, L. Birkedal, and J. Reynolds. Local reasoning about a copying garbage collector. In 31st POPL, pp220–231, 2004.
    Google ScholarLocate open access versionFindings
  • H. Yang and P. O’Hearn. A semantic basis for local reasoning. In 5th FOSSACS, LNCS 2303, 2002.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

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