Abstract Read Permissions: Fractional Permissions without the Fractions

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

Proceedings 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013 |

Published by Springer Berlin Heidelberg

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.