Fractional permissions is trick used in separation logic and its generalization permission logic to for permission accounting. That is, to track the notion of sharing a resource. The idea is to distinguish between
- owning 100% of a resource that allows you to do anything with it: read/write/delete.
- having several owners of a resource that might each own 50%, 25% and 25% (say) of the resource and can only read the resource.
Adapted for separation logic by bornat:popl:2005. Later, heule:ftfjp:2011 developed a variation that avoids the sometimes ad hoc choice of what fractions to use.
Notes related to Fractional permissions
Permission accounting, VeriFast verifier
Papers related to Fractional permissions
- Permission accounting in separation logic [bornat:popl:2005]
- Fractional permissions without the fractions [heule:ftfjp:2011]
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- Verification of concurrent programs with Chalice [leino:fosad:2007]