Abstract Read Permissions: Fractional Permissions without the Fractions

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

Abstract Read Permissions: Fractional Permissions without the Fractions

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

14th International Conference on Verification, Model Checking, and Abstract Interpretation
January 20-22, 2013, Rome, Italy

Materials

Paper (.pdf, 383.37 KiB)
BibTeX (.bib, 652 Bytes)
DOI
Slides (.pdf, 721.00 KiB)

Abstract

Fractional Permissions are a popular approach to reasoning about programs that use shared-memory concurrency, because they provide a way of proving data race freedom while permitting concurrent read access. However, specification using fractional permissions typically requires the user to pick concrete mathematical values for partial permissions, making specifications overly low-level, tedious to write, and harder to adapt and re-use. This paper introduces abstract read permissions: a flexible and expressive specification methodology that supports fractional permissions while allowing the user to work at the abstract level of read and write permissions. The methodology is flexible, modular, and sound. It has been implemented in the verification tool Chalice.