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
Notes related to Fractional permissions without the fractions
Papers related to Fractional permissions without the fractions
- Abstract read permissions: Fractional permissions without the fractions [heule:vmcai:2013]