John Boyland
University of Wisconsin - Milwaukee
Checking interference with fractional permissions
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.
Principles
of Programming Seminars
Friday, September 19, 2003
3:30 p.m.
Wean Hall 8220