Permission accounting in separation logic

Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew Parkinson
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 07 February 2020

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
POPL '05
Long Beach, California, USA
Association for Computing Machinery
New York, NY, USA
Pages 259-270
Topic(s): verification
Note(s): permission logic, separation logic, permission accounting, fractional permissions

Separation logic is about tracking ownership of objects and, usually, this means full ownership: you either own an object and can do anything you want with it or you have no access at all. This paper is about sharing ownership as in the reader-writer pattern where an object can be shared between several readers or ownership can be given to a single writer.

The paper explores two ways of doing this:

  1. Using fractional permissions where ownership can be split into several parts and can be recombined later. (This seems to be best for recursive functions?)

  2. Using counting permissions where the number of readers is tracked.

The main technical trick used in adding this to the logic is to change from modelling the heap as a map from addresses to values but, instead, as a map from addresses to pairs of values and permissions and permissions are either a fraction or a count.

Besides the technical content, the writing style of the author stands out. Beyond the innocent sounding fact that it is written in the first person, the style is very hard to describe – you need to read it for yourself.

Fractional permissions, Permission accounting

  • Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
  • Fractional permissions without the fractions [heule:ftfjp:2011]
  • VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
  • Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]