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:
The present author has given the following example: ØÖÙ Ü ÓÒ× ́¿ μ where the final assertion describes a disconnected piece of structure, and would be falsified if the disconnected piece were reclaimed by a garbage collector

Separation Logic: A Logic for Shared Mutable Data Structures

LICS, pp.55-74, (2002)

Cited by: 2417|Views131
EI WOS

Abstract

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperativeprograms that use shared mutable data structure.The simple imperative programming language is extended with commands (not expressions) for accessing and modifying sha...More

Code:

Data:

Introduction
  • The use of shared mutable data structures, i.e., of structures where an updatable field can be referenced from more than one point, is widespread in areas as diverse as systems programming and artificial intelligence.
  • £ logical operation È É, called separating conjunction, that asserts that È and É hold for disjoint portions of the addressable storage.
Highlights
  • The use of shared mutable data structures, i.e., of structures where an updatable field can be referenced from more than one point, is widespread in areas as diverse as systems programming and artificial intelligence
  • Approaches to reasoning about this technique have been studied for three decades, but the result has been methods that suffer from either limited applicability or extreme complexity, and scale poorly to programs of even moderate size. (A partial bibliography is given in Reference [28].)
  • The problem faced by these approaches is that the correctness of a program that mutates data structures usually
  • The following program performs an in-place reversal of a list: ÒÐ Û Ð ÒÐ Ó · 1⁄2℄ · 1⁄2℄
  • £ logical operation È É, called separating conjunction, that asserts that È and É hold for disjoint portions of the addressable storage
  • The present author [28] has given the following example: ØÖÙ Ü ÓÒ× ́¿ μ where the final assertion describes a disconnected piece of structure, and would be falsified if the disconnected piece were reclaimed by a garbage collector
Results
  • Suppose that an assertion Ô holds for a store that maps the variable Ü into an address « and a heap that maps « into 1⁄2 .
  • The following is a detailed proof outline of a local specification of a command that uses allocation and mutation to construct a two-element cyclic structure containing relative addresses: ÑÔ Ü ÓÒ× ́ μ
  • The authors can use an assertion variable Ô to specify that every property of the heap that is active before executing
  • To capture the sharing structure, the authors use iterated separating conjunction to define ʬμ to assert that the last element of ¬ is the empty list, while every previous element consists of a single integer cons’ed onto some later element of ¬: ʬμ
  • The existence of weakest preconditions for each of the new commands assures them that a central property of Hoare logic is preserved by the extension: that a program specification annotated with loop invariants and recursion hypotheses can be reduced to a collection of assertions, called verification conditions, whose validity will insure the original specification.
  • The present author [28] has given the following example: ØÖÙ Ü ÓÒ× ́¿ μ where the final assertion describes a disconnected piece of structure, and would be falsified if the disconnected piece were reclaimed by a garbage collector.
  • New Forms of Inference In Yang’s proof of the Schorr-Waite algorithm, there are thirteen assertions that have been semantically validated but do not seem to be consequences of known inference rules, and are far too specific to be considered axioms.
Conclusion
  • Consider the definition of given in Section 6: The assertion1⁄2 ¡ 3⁄4μ ¡ ́3⁄4 ¡ ¿μμμ holds in states where two distinct records overlap, e.g. iff one were to try to recast the Schorr-Waite proof in the logic with address arithmetic, it would be difficult to assert that distinct records do not overlap, and that all address values in the program denote the first fields of records.
  • Types and assertions may be semantically similar, the actual development of type systems for programming languages has been quite separate from the development of approaches to specification such as Hoare logic, refinement calculi, or model checking.
Reference
  • R. Bornat. Explicit description in BI pointer logic. Unpublished, June 2001.
    Google ScholarLocate open access versionFindings
  • R. M. Burstall. Some techniques for proving correctness of programs which alter data structures. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 23–50. Edinburgh University Press, Edinburgh, Scotland, 1972.
    Google ScholarLocate open access versionFindings
  • L. Caires and L. Monteiro. Verifiable and executable specifications of concurrent objects in Ä. In C. Hankin, editor, Programming Languages and Systems — ESOP ’98, volume 1381 of Lecture Notes in Computer Science, pages 42–56, Berlin, 1998. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • C. Calcagno. Program logics in the presence of garbage collection (abstract). In F. Henglein, J. Hughes, H. Makholm, and H. Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, page 11. IT University of Copenhagen, 2001.
    Google ScholarLocate open access versionFindings
  • C. Calcagno. Semantic and Logical Properties of Stateful Programmming. Ph. D. dissertation, Universitadi Genova, Genova, Italy, 2002.
    Google ScholarFindings
  • C. Calcagno and P. W. O’Hearn. On garbage and program logic. In Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in Computer Science, pages 137–151, Berlin, 2001. Springer-Verlag.
    Google ScholarFindings
  • C. Calcagno, P. W. O’Hearn, and R. Bornat. Program logic and equivalence in the presence of garbage collection. Submitted July 2001, 2001.
    Google ScholarLocate open access versionFindings
  • C. Calcagno, H. Yang, and P. W. O’Hearn. Computability and complexity results for a spatial assertion language for data structures. In R. Hariharan, M. Mukund, and V. Vinay, editors, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 108–119, Berlin, 2001. Springer-Verlag.
    Google ScholarFindings
  • L. Cardelli, P. Gardner, and G. Ghelli. A spatial logic for querying graphs. In M. Hennessy and P. Widmayer, editors, Automata, Languages and Programming, Lecture Notes in Computer Science, Berlin, 2002. Springer-Verlag.
    Google ScholarFindings
  • L. Cardelli and G. Ghelli. A query language based on the ambient logic. In D. Sands, editor, Programming Languages and Systems — ESOP 2001, volume 2028 of Lecture Notes in Computer Science, pages 1–22, Berlin, 2001. SpringerVerlag.
    Google ScholarFindings
  • L. Cardelli and A. D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Conference Record of POPL ’00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 365–377, New York, 2000. ACM.
    Google ScholarFindings
  • G. Conforti, G. Ghelli, A. Albano, D. Colazzo, P. Manghi, and C. Sartiani. The query language TQL. In Proceedings of the 5th International Workshop on the Web and Databases (WebDB), Madison, Wisconsin, 2002.
    Google ScholarLocate open access versionFindings
  • D. Galmiche and D. Mery. Proof-search and countermodel generation in propositional BI logic. In N. Kobayashi and B. C. Pierce, editors, Theoretical Aspects of Computer Software, volume 2215 of Lecture Notes in Computer Science, pages 263–282, Berlin, 2001. Springer-Verlag.
    Google ScholarFindings
  • D. Galmiche, D. Mery, and D. J. Pym. Resource tableaux. Submitted, 2002.
    Google ScholarLocate open access versionFindings
  • D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, Cambridge, Massachusetts, 2000.
    Google ScholarFindings
  • C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580 and 583, October 1969.
    Google ScholarLocate open access versionFindings
  • C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971.
    Google ScholarLocate open access versionFindings
  • C. A. R. Hoare. Towards a theory of parallel programming. In C. A. R. Hoare and R. H. Perrott, editors, Operating Systems Techniques, volume 9 of A.P.I.C. Studies in Data Processing, pages 61–71, London, 1972. Academic Press.
    Google ScholarLocate open access versionFindings
  • S. Ishtiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 14–26, New York, 2001. ACM.
    Google ScholarFindings
  • G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In X. Leroy and A. Ohori, editors, Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28–52, Berlin, 1998. SpringerVerlag.
    Google ScholarLocate open access versionFindings
  • P. W. O’Hearn. Notes on conditional critical regions in spatial pointer logic. Unpublished, August 31, 2001.
    Google ScholarLocate open access versionFindings
  • P. W. O’Hearn. Notes on separation logic for shared-variable concurrency. Unpublished, January 3, 2002.
    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 1999.
    Google ScholarLocate open access versionFindings
  • P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In L. Fribourg, editor, Computer Science Logic, volume 2142 of Lecture Notes in Computer Science, pages 1–19, Berlin, 2001. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • S. S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 19(5):279–285, May 1976.
    Google ScholarLocate open access versionFindings
  • D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers, Boston, Massachusetts, 2002. (to appear).
    Google ScholarFindings
  • J. C. Reynolds. The Craft of Programming. Prentice-Hall International, London, 1981.
    Google ScholarFindings
  • J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In J. Davies, B. Roscoe, and J. Woodcock, editors, Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
    Google ScholarFindings
  • J. C. Reynolds. Lectures on reasoning about shared mutable data structure. IFIP Working Group 2.3 School/Seminar on State-of-the-Art Program Design Using Logic, Tandil, Argentina, September 6-13, 2000.
    Google ScholarFindings
  • J. C. Reynolds and P. W. O’Hearn. Reasoning about shared mutable data structure (abstract of invited lecture). In F. Henglein, J. Hughes, H. Makholm, and H. Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, page 7. IT University of Copenhagen, 2001. The slides for this lecture are available at ftp://ftp.cs.cmu.edu/user/jcr/spacetalk.ps.gz.
    Google ScholarLocate open access versionFindings
  • M. Tofte and J.-P. Talpin. Implementation of the typed callby-value -calculus using a stack of regions. In Conference Record of POPL ’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188– 201, New York, 1994. ACM Press.
    Google ScholarLocate open access versionFindings
  • D. Walker and G. Morrisett. Alias types for recursive data structures. In R. W. Harper, editor, Types in Compilation, volume 2071 of Lecture Notes in Computer Science, pages 177–206, Berlin, 2001. Springer-Verlag.
    Google ScholarFindings
  • H. Yang. An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm. In F. Henglein, J. Hughes, H. Makholm, and H. Niss, editors, SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, pages 41–68. IT University of Copenhagen, 2001.
    Google ScholarLocate open access versionFindings
  • H. Yang. Local Reasoning for Stateful Programs. Ph. D. dissertation, University of Illinois, Urbana-Champaign, Illinois, July 2001.
    Google ScholarFindings
  • H. Yang and P. W. O’Hearn. A semantic basis for local reasoning. In M. Nielsen and U. Engberg, editors, Foundations of Software Science and Computation Structures, volume 2303 of Lecture Notes in Computer Science, pages 402–416, Berlin, 2002. Springer-Verlag.
    Google ScholarFindings
Your rating :
0

 

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