Fractional permissions without the fractions
Stefan Heule, K. Rustan M. Leino, Péter Müller, Alexander J. Summers · 2011
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.