Alexander J. Summers (ETH Zurich): Fractional Permissions without the Fractions
(Joint work with Stefan Heule, Rustan Leino and Peter Müller)
Abstract: Fractional Permissions are a popular approach to the problem of reasoning modularly about shared memory concurrency. When combined with appropriate synchronisation primitives, fractional permissions allow the specification and verification of a disciplined usage of shared locations: one writer thread, or many reader threads at a time (but not both!). Permission amounts are specified using rational values between 0 (no permission) and 1 (full permission); anything in between denotes a read permission.
However, the specification of permission amounts as concrete rational numbers leads to several drawbacks. The user of the methodology must pick appropriate values that are consistent with all other method specifications in the program. This can be tedious, and the user is generally concerned with permissions only at the abstract level of when reading and writing to a location is permitted; the values associated with these permissions are largely irrelevant to the programmer. Furthermore, rational numbers typically have relatively poor support from automatic theorem provers.
We present a specification methodology for permissions which provides most of the flexibility and expressiveness of fractional permissions, while allowing the user to write specifications at the abstract level of read and write permissions. The methodology is modular and sound, and has been designed to support reasoning using locks/monitors, fork/join of threads and sequential features such as loops and method calls. A prototype has been implemented in a modified version of the verification tool Chalice. The underlying encoding is designed to use under-specified integer values (no rationals), which makes it possible to leverage good support from automatic theorem provers.