Access-Right Expressions

Abstract

data types, and in particular those that are designed to provide resources for use by concurrently executable programs, are often designed to be used only in certain ways.The intended constraints on use of an instance of such a type can be expressed in two principal ways: as assertions on the domain of values input to each operator, and as constraints on the sequences in which the operators of the type can be called by a customer process.These constraints must be enforced in the environment in which an instance of the type is used.Nevertheless, they are very much a part of the type specification, for its definition is not complete, nor can the consistency of its representation be proved, without them.A notation is provided in which to express sequential constraints, which are here called accessright expressions.It is suggested that these expressions should be declared in a programming language that supports the definition of monitors or resource managers.Implications for the proof rules of monitors are discussed, and suggestions are made for a programming language implementation.