Fractional Permissions without the Fractions

Stefan Heule; K. Rustan M. Leino; Peter Müller; Alexander J. Summers

Fractional Permissions without the Fractions

by Stefan Heule, K. Rustan M. Leino, Peter Müller and Alexander J. Summers

13th Workshop on Formal Techniques for Java-like Programs
July 26-26, 2011, Lancaster, UK

Superseded by the VMCAI'13 publication.

Materials

Paper (.pdf, 226.60 KiB)
BibTeX (.bib, 628 Bytes)
DOI
Slides (.pdf, 515.70 KiB)

Abstract

Fractional Permissions are a popular approach to reasoning about programs that use shared-memory concurrency. Abstractly, they provide a way of managing that either multiple readers or one writer thread can access a resource concurrently. Concretely, specification using fractional permissions typically requires the user to pick concrete mathematical values for partial permissions, making specifications overly verbose, tedious to write, and harder to adapt and re-use.
This paper contributes a flexible and expressive specification methodology for supporting fractional permissions while allowing the user to work at the abstract level of read and write permissions. The methodology is flexible and modular, and has been implemented in the verification tool Chalice.