Constraint Semantics for Abstract Read Permissions

The concept of controlling access to mutable shared data via permissions is at the heart of permission logics such as sep- aration logic and implicit dynamic frames, and is also used in type systems, for instance, to give a semantics to \read- only" annotations. Existing permission models have dier- ent strengths in terms of expressiveness. Fractional permis- sions, for example, enable unbounded (recursive) splitting, whereas counting permissions enable unbounded subtraction of the same permission amount. Combining these strengths in a single permission model appeared to increase the com- plexity for the user and tools. In this paper we extend our previous work on abstract read permissions by providing them with a novel constraint semantics, which retains the use of the domain of rational numbers but enables unboun- ded subtraction of identical amounts. Thus we can keep an intuitive model conducive to SMT solvers while enabling \counting.