Fractional permissions without the fractions

Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 14 March 2020

Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs
FTfJP '11
Lancaster, United Kingdom
Association for Computing Machinery
New York, NY, USA
2011
Topic(s): tools verification
Note(s): permission logic, Chalice verifier, fractional permissions, permission accounting
Papers: bornat:popl:2005

The standard way of distinguishing read and write permissions in separation logic is with fractional permissions in which you can write a resource if you have 100% of the resource read a resource if you have some fraction of the resource and you have no access if you have 0% of the resource. When you replicate references to a resource, you split the fraction into some smaller parts and when you are done with those references, you recombine (sum) all their fractions.

Whilst this is intuitively appealing, in practice you find yourself making arbitrary choices about the size of each fraction and, if you add another use of a resource, you might need to update the existing choice of fractions from “p/2” (say) to “p/3”.

This paper describes an experimental version of the Chalice verifier which directly encodes the notion of “read permission” as a read instead of having to encode it as a fraction of an access. They end up with six different forms of permission:

  • 1 - a full permission (allowing both reads and writes)
  • rd - read permission
  • rd(tok) - a token read permission (used for asynchronous method calls)
  • rd(o) - monitor read permission (used for monitor calls)
  • P1 + P2 - combining permissions
  • P1 - P2 - removing permissions

Chalice verifier, Fractional permissions, Permission accounting

  • Abstract read permissions: Fractional permissions without the fractions [heule:vmcai:2013]