Download

Open access
Date
2014Type
- Report
Altmetrics
Download
Abstract
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. Show more
Permanent link
https://doi.org/10.3929/ethz-a-010152828Publication status
publishedExternal links
Search via SFX
Publisher
ETH-ZürichSubject
ACCESS CONTROL (OPERATING SYSTEMS); SPECIAL PROGRAMMING METHODS; SPEZIELLE PROGRAMMIERMETHODEN; ZUGRIFFSKONTROLLE (BETRIEBSSYSTEME)Organisational unit
03653 - Müller, Peter02150 - Departement Informatik / Department of Computer Science
More
Show all metadata
Altmetrics