English for Research: Grammar, Usage and Style

Abstract

A specification of the monitor primitives that have been proposed for mutual exclusion and interprocess communication in operating systems is verified to be correct. The specification is given in the PASCAL programming language and the proofs of correctness use the axiomatic definition of this language. Two aspects of correctness are considered: the correctness of the program implementation of the primitives and the correctness as viewed by the processes that execute the monitor primitives.