Lecture Notes in Computer Science, 2003, Volume 2694/2003, 1075, DOI: 10.1007/3-540-44898-5_4

Checking Interference with Fractional Permissions

John Boyland

View Related Documents

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.
This material is based upon work supported by the National Science Foundation under Grant No. 9984681
The author wishes to acknowledge support through the High Dependability Computing Program from NASA Ames cooperative agreement NCC-2-1298.

Fulltext Preview

Image of the first page of the fulltext document