Richard Bornat
Abstract
A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The roots of the approach are in Boyland's [3] demonstration of the utility of fractional permissions in specifying non-interference between concurrent threads. We add the notion of counting permission, which mirrors the programming technique called permission counting. Both fractional and counting permissions permit passivity, the specification that a program can be permitted to access a heap cell yet prevented from altering it. Models of both mechanisms are described. The use of two different mechanisms is defended. Some interesting problems are acknowledged and some intriguing possibilities for future development, including the notion of resourcing as a step beyond typing, are paraded.
- R. Bornat. Proving pointer programs in Hoare logic. In R. C. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction, 5th International Conference, LNCS, pages 102--126. Springer, 2000.]] Google Scholar
Digital Library
- R. Bornat, C. Calcagno, and P. O'Hearn. Local reasoning, separation and aliasing. SPACE Workshop, Venice, 2004.]]Google Scholar
- J. Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis: 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 55--72, Berlin, Heidelberg, New York, 2003. Springer.]] Google ScholarDigital Library
- P. Brinch Hansen. Operating System Principles. Prentice Hall, 1973.]] Google ScholarDigital Library
- P. Brinch Hansen, editor. The Origin of Concurrent Programming. Springer-Verlag, 2002.]] Google ScholarDigital Library
- S. D. Brookes. A semantics for concurrent separation logic. In CONCUR'04: 15th International Conference on Concurrency Theory, volume 3170 of Lecture Notes in Computer Science, pages 16--34, London, August 2004. Springer. Extended version to appear in Theoretical Computer Science.]]Google ScholarCross Ref
- R. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7:23--50, 1972.]]Google Scholar
- P. J. Courtois, F. Heymans, and D. L. Parnas. Concurrent control with "readers" and "writers". Commun. ACM, 14(10):667--668, 1971.]] Google ScholarDigital Library
- E. W. Dijkstra. Cooperating sequential processes. In F. Genuys, editor, Programming Languages, pages 43--112. Academic Press, 1968. Reprinted in {5}.]]Google Scholar
- R. Ennals, R. Sharp, and A. Mycroft. Linear types for packet processing. In To appear. Proceedings of the 2004 European Symposium on Programming (ESOP), LNCS. Springer-Verlag, 2004.]]Google Scholar
- C. A. R. Hoare. Towards a theory of parallel programming. In Hoare and Perrott, editors, in, ed. Operating System Techniques, 1972., pages 61--71. Academic Press, 1972.]]Google Scholar
- E. J. Johnson and A. Kunze. IXP2400/2800 Programming: The Complete Microengine Coding Guide. Intel Press, 2003.]] Google ScholarDigital Library
- P. O'Hearn. Notes on separation logic for shared-variable concurrency. unpublished, Jan. 2002.]]Google Scholar
- P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In L. Fribourg, editor, CSL 2001, pages 1--19. Springer-Verlag, 2001. LNCS 2142.]] Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency and local reasoning. to appear in Theoretical Computer Science; preliminary version published as {16}.]] Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR'04: 15th International Conference on Concurrency Theory, volume 3170 of Lecture Notes in Computer Science, pages 49--67, London, August 2004. Springer. Extended version is {15}.]]Google Scholar
- P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215--244, June 1999.]]Google ScholarCross Ref
- D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.]]Google Scholar
- J. Reynolds. Separation logic: a logic for shared mutable data structures. Invited Paper, LICS'02, 2002.]] Google ScholarDigital Library
- 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. Palgrave, 2000.]]Google Scholar
- H. Yang and P. O'Hearn. A semantic basis for local reasoning. In 5th FOSSACS, pages 402--416. Springer-Verlag, 2002.]] Google ScholarDigital Library
Index Terms
- Permission accounting in separation logic
Recommendations
Permission accounting in separation logic
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesA lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The ...
Permission based granular access control pattern
PLoP '14: Proceedings of the 21st Conference on Pattern Languages of ProgramsEnterprise applications are designed to address specific business needs and are generally run within the internal corporate networks. Access to enterprise applications is controlled by various corporate policies, based on numerous widely accepted ...
Syntactic Control of Interference and Concurrent Separation Logic
At last year@?s MFPS conference we introduced a revised version of Concurrent Separation Logic in which assertions are tagged with a ''rely set'' of variables assumed to be unmodified by other processes. We showed that this logic is compositional and ...
Comments