Semantics of Fractional Permissions with Nesting

by John Boyland

Abstract

Fractional permissions use fractions to distinguish write access (1) from read access (any smaller fraction). Nesting (an extension of adoption) can be used to model object invariants and ownership. Indeed nesting extends both in a form of ``monotonically increasing invariants.'' Fractional permissions thus provides a foundation for defining the meaning of a large variety of access-based annotations: uniqueness, read-only, immutability, method effects, lock protected state etc. In this paper we give a semantics of fractional permissions with nesting (adoption), in terms of ``fractional heaps'' indicating the mutable state that can be accessed using each permission. We show that fractions are sound and that the system satisfies separation properties.

BibTeX Style Reference

@techreport(boyland:07frac-nesting,
  author =      {John Boyland}
  title =       {Semantics of Fractional Permissions with Nesting},
  institution = {University of Wisconsin-Milwaukee, Dept.\ of EE \& CS},
  number = {CS-07-01},
  month = dec,
  year = 2007)

How to Get a Copy

The technical report is available in PDF. The electronic appendix (machine-checked proofs) is also available.

Last Modified: December 5, 2007