Syntactic Control of Interference for Separation Logic

Research output: Contribution to conference (unpublished)Paper

Authors

Colleges, School and Institutes

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.

Details

Original languageEnglish
Pages323-336
Number of pages14
Publication statusPublished - 1 Jan 2012
EventPOPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Philadelphia, United States
Duration: 25 Jan 201227 Jan 2012

Conference

ConferencePOPL '12 -The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryUnited States
CityPhiladelphia
Period25/01/1227/01/12

Keywords

  • Separation Logic, Syntactic Control of Interference, Program Logic, Static Analysis, Conditional Critical Regions, Denotational Semantics, Concurrency, Fractional Permissions, Type Systems