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 access- right 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. Categories and Subject Descriptors: D.3.3 (Programm|ng Languages): Language Constructs-- abstract data types; concurrent programming structures; D.4.5 (Operating Systems): Reliability-- verification; D.4.6 (Operating Systems): Security and Protection--access controls

This publication has 11 references indexed in Scilit: