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:
-
Using fractional permissions where ownership can be split into several parts and can be recombined later. (This seems to be best for recursive functions?)
-
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.
Notes related to Permission accounting in separation logic
Fractional permissions, Permission accounting
Papers related to Permission accounting in separation logic
- 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]