verification of fairness in an implementation of monitors
An implementation in Pascal by Saxena and Bredt of the Monitor construct is studied. Techniques are given for using a program verifer to analyse the conditions under which the implementation is fair (i.e. once a process is delayed it eventually will be continued). By use of a virtual data structure, fairness is represented in terms of simple properties which can be verified automatically. Examples are given illustrating how the verification can force unstated assumptions upon which the implementation depends to be made explicit, and how it can be used to study whether the implementation makes adequate use of resources. The development of techniques for analysis of such implementations is required before the correctness of high-level language operating systems such as Brinch Hansen's SOLO can be completely established.
verification fairness implementation monitors use process virtualization data structures resource developer analysis correctness language operating system condition variables program proofs program correctness process queues