Verification

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 differ-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.