Permission accounting in separation logic.

Article


Bornat, R., Calcagno, C., Parkinson, M. and O'Hearn, P. 2005. Permission accounting in separation logic. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), Long Beach, California, USA. Proceedings. https://doi.org/10.1145/1047659.1040327
TypeArticle
TitlePermission accounting in separation logic.
AuthorsBornat, R., Calcagno, C., Parkinson, M. and O'Hearn, P.
Abstract

Concurrent separation logic includes the notion of ‘ownership' of a heap data structure that can be transferred between processes. This paper refined that idea with permission – partial ownership – so that we could deal with shared read-only data. It applies that idea to two significant examples – readers-and-writers, in particular, had never before had a simple formal proof – and shows why at least two forms of permission are required.
Separation logic has become a major influence on work in concurrency and in program analysis. Permissions are now routinely used in that work.

Research GroupFoundations of Computing group
PublisherAssociation for Computing Machinery (ACM)
Journal32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), Long Beach, California, USA. Proceedings
ISSN0362-1340
Publication dates
Print01 Jan 2005
Publication process dates
Deposited13 Oct 2008
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1145/1047659.1040327
LanguageEnglish
Page range259-270
Permalink -

https://repository.mdx.ac.uk/item/80qz3

  • 39
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as

Related outputs

Describing and simulating concurrent quantum systems
Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16
New lace and arsenic: adventures in weak memory with a program logic (v2)
Bornat, R., Alglave, J. and Parkinson, M. 2016. New lace and arsenic: adventures in weak memory with a program logic (v2). arXiv.org arXiv. https://doi.org/10.48550/arXiv.1512.01416
Towards automatic stability analysis for rely-guarantee proofs
Amjad, H. and Bornat, R. 2009. Towards automatic stability analysis for rely-guarantee proofs. in: Jones, N. and Müller-Olm, M. (ed.) Verification, model checking, and abstract interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings Springer.
Separation logic and concurrency
Bornat, R. 2010. Separation logic and concurrency. in: Boca, P., Bowen, J. and Siddiqi, J. (ed.) Formal Methods: State of the Art and New Directions London Springer Verlag. pp. 217-248
Inter-process buffers in separation logic with rely-guarantee
Bornat, R. and Amjad, H. 2010. Inter-process buffers in separation logic with rely-guarantee. Formal Aspects of Computing. 22 (6), pp. 735-772. https://doi.org/10.1007/s00165-009-0141-8
Explanation of two non-blocking shared-variable communication algorithms
Bornat, R. and Amjad, H. 2011. Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects of Computing. https://doi.org/10.1007/s00165-011-0213-4
Cyclic proofs of program termination in separation logic
Brotherston, J., Bornat, R. and Calcagno, C. 2008. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices - POPL '08. 43 (1), pp. 101-112. https://doi.org/10.1145/1328897.1328453
Variables as resource in Hoare logic.
Bornat, R., Calcagno, C. and Parkinson, M. 2006. Variables as resource in Hoare logic. in: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings. IEEE Computer Society. pp. 137-146
Variables as resources in separation logic.
Bornat, R., Calcagno, C. and Yang, H. 2006. Variables as resources in separation logic. 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.. 155, pp. 247-276. https://doi.org/10.1016/j.entcs.2005.11.059
Modular verification of a non-blocking stack.
Bornat, R., Parkinson, M. and O'Hearn, P. 2007. Modular verification of a non-blocking stack. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.. https://doi.org/10.1145/1190216.1190261