Checking interference with fractional permissions

by John Boyland.

Abstract

We describe a type system for checking interference using the concept of linear capabilities (which we call ``permissions''). Our innovations include the concept of ``fractional'' permissions: reads can be permitted with fractional permissions whereas writes require complete permissions. This distinction expresses the fact that reads on the same state do not conflict with each other. One may give shared read access at one point while still retaining write permission afterwards. We give an operational semantics of a simple imperative language with structured parallelism and prove that the permission system enables parallelism to proceed with deterministic results.

BibTeX Style Reference

@inproceedings(boyland:03fractions,
  author =      {John Boyland},
  title =       {Checking Interference with Fractional Permissions},
  booktitle =   "Static Analysis: 10th International Symposium",
  editor =      "R. Cousot",
  year =        2003,
  series =      "Lecture Notes in Computer Science",
  publisher =   "Springer",
  address =     "Berlin, Heidelberg, New York",
  volume =      "" # "2694",
  pages =       {55-72})

How to Get a Copy

The paper is published in the SAS 2003 proceedings. The appendix to the paper (which includes technical matter) is available. The paper proper is copyright by Springer Verlag, but is available (with appendix attached) by kind permission of Springer. This copy is available only for academic or personal use.

The talk given at SAS 2003 is available.

Last Modified: March 7, 2005