Operating C. Editor
Monitors: An Operating System StructuringConcept
C.A.R. Hoare
The Queen’s University of Belfast
Copyright By PowCoder代写 加微信 powcoder
This paper develops Brinch-Hansen’s concept of a monitor as a method of structuring an operating system. It introduces a form of synchronization, describes a possible method of implementation in terms of sema- phores and gives a suitable proof rule. Illustrative examples include a single resource scheduler, a bounded buffer, an alarm clock, a buffer pool, a disk head optimizer, and a version of the problem of readers and writers.
Key Words and Phrases: monitors, operating systems, scheduling, mutual exclusion, synchronization, system implementation languages, structured multiprogramming
CR Categories: 4.31, 4.22
I. Introduction
A primary aim of an operating system is to share a computer installation among many programs making unpredictable demands upon its resources• A primary task of its designer is therefore to construct resource allocation (or scheduling) algorithms for resources of various kinds (main store, drum store, magnetic tape handlers, consoles, etc.). In order to simplify his task, he should try to construct separate schedulers for each class of resource. Each scheduler will consist of a certain amount of local administrative data, together with some procedures and functions which are called by programs wishing to acquire and release resources. Such a collec- tion of associated data and procedures is known as a monitor; and a suitable notation can be based on the class notation of sIrvtULA67[6].
monitorname:monitor
begin.., declarations of data local to the monitor;
procedureprocname (… formal parameters…) ; begin.., procedurebody.., end;
•.. declarationsofotherprocedureslocaltothemonitor;
•.. initialization of local data of the monitor… end;
Note that the procedure bodies may have local data, in the normal way.
In order to call a procedure of a monitor, it is neces- sary to give the name of the monitor as well as the name of the desired procedure, separating them by a dot:
monitorname.procname(.., actual parameters…) ;
In an operating system it is sometimes desirable to declare several monitors with identical structure and behavior, for example to schedule two similar resources• In such cases, the declaration shown above will be preceded by the word class, and the separate momtors will be declared to belong to this class:
monitor I, monitor 2: classname;
Thus the structure of a class of monitors is identical to that described for a data representation in [13], except for addition of the basic word monitor. Brinch-Hansen uses the word shared for the same purpose [3].
The procedures of a monitor are common to all running programs, in the sense that any program may at any time attempt to call such a procedure• However, it is essential that only one program at a time actually succeed in entering a monitor procedure, and any sub- sequent call must be held up until the previous call has been completed. Otherwise, if two procedure bodies were in simultaneous execution, the effects on the local
variables of the monitor could be chaotic• The proce-
Copyright@ 1974,Associationfor ComputingMachinery,Inc. General permission to republish, but not for profit, all or part of this material is granted, provided that ACM’s copyright notice is given and that reference is made to the publication, to its date of issue, and to the fact that reprinting privileges were granted by permissionofthe Associationfor ComputingMachinery.
This paper is based on an address delivered to IRIA, France, May 11, 1973.Author’s address: Department of Computer Science, The Queen’s University of Belfast, Belfast BT7 INN, Northern Ireland•
Communications of
October 1974 Volume 17 Number 10
dures local to a monitor should not access any nonlocal variables other than those local to the same monitor, and these variables of the monitor should be inaccessible from outside the monitor. If these restrictions are im- posed, it is possible to guarantee against certain of the more obscure forms of time-dependent coding error; and this guarantee could be underwritten by a visual scan of the text of the program, which could readily be automated in a compiler.
Any dynamic resource allocator will sometimes need to delay a program wishing to acquire a resource which is not currently available, and to resume that program after some other program has released the resource required. We therefore need: a “wait” operation, issued from inside a procedure of the monitor, which causes the calling program to be delayed; and a “signal” opera- tion, also issued from inside a procedure of the same monitor, which causes exactly one of the waiting pro- grams to be resumed immediately. If there are no wait- ing programs, the signal has no effect. In order to enable other programs to release resources during a wait, a wait operation must relinquish the exclusion which would otherwise prevent entry to the releasing procedure. However, we decree that a signal operation be followed immediately by resumption of a waiting program, with- out possibility of an intervening procedure call from yet a third program. It is only in this way that a waiting program has an absolute guarantee that it can acquire the resource just released by the signalling program without any danger that a third program will interpose a monitor entry and seize the resource instead.
In many cases, there may be more than one reason for waiting, and these need to be distinguished by both the waiting and the signalling operation. We therefore introduce a new type of “variable” known as a “condi- tion”; and the writer of a {nonitor should declare a variable of type condition for each reason why a pro- gram might have to wait. Then the wait and signal operations should be preceded by the name of the relevant condition variable, separated from it by a dot:
condvariable, wait; eondvariable, signal;
Note that a condition “variable” is neither true nor false; indeed, it does not have any stored value accessible to the program. In practice, a condition variable will be represented by an (initially empty) queue of processes which are currently waiting on the condition; but this queue is invisible both to waiters and signallers. This design of the condition variable has been deliberately kept as primitive and rudimentary as possible, so that it may’ be implemented efficiently and used flexibly to achieve a wide variety of effects. There is a great temp- tation to introduce a more complex synchronization primitive, which may be easier to use for many purposes. We shall resist this temptation for a while.
As the simplest example of a monitor, we will design a scheduling algorithm for a single resource, which is
dynamically acquired and released by an unknown number of customer processes by calls on procedures
procedureacquire; procedure release;
A variable1
busy: Boolean
determines whether or not the resource is in use. If an attempt is made to acquire the resource when it is busy, the attempting program must be delayed by waiting on a variable
nonbusy :condition
which is signalled by the next subsequent release. The initial value of busy is false. These design decisions lead to the following code for the monitor:
single resource:monitor begin busy: Boolean;
nonbusy :condition; procedure acquire;
begin if busy then nonbusy, wa#; busy := true
end; procedurerelease;
begin busy := false; nonbusy, signal
busy := false; comment initial value;
end single resource
1. In designing a monitor, it seems natural to design the procedure headings, the data, the conditions, and the procedure bodies, in that order. All subsequent examples will be designed in this way.
2. The acquire procedure does not have to retest that busy has gone false when it resumes after its wait, since the release procedure has guaranteed that this is so; and as mentioned before, no other program can intervene between the signal and the continuation of exactly one waiting program.
3. If more than one program is waiting on a condition, we postulate that the signal operation will reactivate the longest waiting program. This gives a simple neutral queuing discipline which ensures that every waiting program will eventually get its turn.
4. The single resource monitor simulates a Boolean semaphore [7] with acquire and release used for P and V respectively. This is a simple proof that the monitor/ condition concepts are not in principle less powerful than semaphores, and that they can be used for all the same purposes.
1As in PASCAL [15],a variable declaration is of the form:
(variable identifier) :(type);
Communications of
October 1974 Volume 17 Number 10
2. Interpretation
Having proved that semaphores can be implemented by a monitor, the next task is to prove that monitors can be implemented by semaphores.
Obviously, we shall require for each monitor a Boolean semaphore “rnutex” to ensure that the bodies of the local procedures exclude each other. The sema- phore is initialized to 1; a P(mutex) must be executed on entry to each local procedure, and a V(mutex) must usually be executed on exit from it.
When a process signals a condition on which another process is waiting, the signalling process must wait until the resumed process permits it to proceed. We therefore introduce for each monitor a second semaphore “urgent” (initialized to 0), on which signalling processes suspend themselves by the operation P(urgent). Before releasing exclusion, each process must test whether any other process is waiting on urgent, and if so, must release it instead by a V(urgent) instruction. We therefore need to count the number of processes waiting on urgent, in an integer “urgentcount” (initially zero). Thus each exit from a procedure of a monitor should be coded:
if urgentcount > 0 then V(urgent)else V(mutex)
Finally, for each condition local to the monitor, we introduce a semaphore “condsem” (initialized to 0), on which a process desiring to wait suspends itself by a P(condsem) operation. Since a process signalling this condition needs to know whether anybody is waiting, we also need a count of the number of waiting processes held in an integer variable “condcount” (initially 0). The operation “cond. wait” may now be implemented as follows (recall that a waiting program must release ex- clusion before suspending itself):
condcount := condcount -Jr-1;
if urgentcount > 0 then V(urgent) else V(mutex) ; P(condsem) ;
comment This will always wait;
condcount := condcount – 1
The signal operation may be coded:
urgentcount := urgentcount -}- 1;
if condcount > 0 then {V(condsem) ; P(urgent) }; urgentcount := urgentcount — 1
In this implementation, possession of the monitor is regarded as a privilege which is explicitly passed from one process to another. Only when no one further wants the privilege is mutex finally released.
This solution is not intended to correspond to rec- ommended “style” in the use of semaphores. The con- cept of a condition-variable is intended as a substitute for semaphores, and has its own style of usage, in the same way that while-loops or coroutines are intended as a substitute for jumps.
In many cases, the generality of this solution is un- necessary, and a significant improvement in efficiency is possible.
1. When a procedure body in a monitor contains no
wait or signal, exit from the body can be coded by a simple V(mutex), since urgentcount cannot have changed during the execution of the body.
2. If a cond.signal is the last operation of a procedure body, it can be combined with monitor exit as follows:
if condcount > 0 then V(condsem) else if urgentcount > 0 then V(urgent)
rise V(mutex)
3. If there is no other wait or signal in the procedure body, the second line shown above can also be omitted. 4. If every signal occurs as the last operation of its procedure body, the variables urgentcount and urgent can be omitted, together with all operations upon them. This is such a simplification that O-J. Dahl suggests that signals should always be the last operation of a monitor procedure; in fact, this restriction is a very natural one, which has been unwittingly observed in all examples of this paper.
Significant improvements in effÉciency may also be obtained by avoiding the use of semaphores, and by implementing conditions directly in hardware, or at the lowest and most uninterruptible level of software (e.g. supervisor mode). In this case, the following optimiza- tions are possible.
1. urgentcount and condcount can be abolished, since the fact that someone is waiting can be established by examining the representation of the semaphore, which cannot change surreptitiously within noninterruptible mode.
2. Many monitors are very short and contain no calls to other monitors. Such monitors can be executed wholly in noninterruptible mode, using, as it were, the common exclusion mechanism provided by hardware. This will often involve less time in noninterruptible mode than the establishment of separate exclusion for each monitor.
I am grateful to J. Bezivin, J. Horning, and R.M. McKeag for assisting in the discovery of this algorithm.
3. Proof Rules
The analogy between a monitor and a data repre- sentation has been noted in the introduction. The mu- tual exclusion on the code of a monitor ensures that procedure calls follow each other in time, just as they do in sequential programming; and the same restrictions are placed on access to nonlocal data. These are the reasons why the same proof rules can be applied to monitors as to data representations.
As with a data representation, the programmer may associate an invariant ~ with the local data of a monitor, to describe some condition which will be true of this data before and after every procedure call. ~ must also be made true after initialization of the data, and before every wait instruction; otherwise the next following procedure call will not find the local data in a state which it expects.
Communications of
October 1974 Volume 17 Number 10
With each condition variable b the programmer may associate an assertion B which describes the condition under which a program waiting on b wishes to be re- sumed. Since other programs may invoke a monitor procedure during a wait, a waiting program must ensure that the invariant ~ for the monitor is true beforehand. This gives the proof rule for waits:
{b.wait} ~&B
Since a signal can cause immediate resumption of a wait- ing program, the conditions ~&B which are expected by that program must be made true before the signal; and since B may be made false again by the resumed pro- gram, only ~ may be assumed true afterwards. Thus the proof rule for a signal is:
~&B{b.signal}~
This exhibits a pleasing symmetry with the rule for waiting.
The introduction of condition variables makes it possible to write monitors subject to the risk of deadly embrace [7]. It is the responsibility of the programmer to avoid this risk, together with other scheduling disasters (thrashing, indefinitely repeated overtaking, etc. [11]). Assertion-oriented proof methods cannot prove absence of such risks; perhaps it is better to use less formal methods for such proofs.
Finally, in many cases an operating system monitor constructs some “virtual” resource which is used in place of actual resources by its “customer” pro- grams. This virtual resource is an abstraction from the set of local variables of the monitor. The program prover should therefore define this abstraction in terms of its concrete representation, and then express the in- tended effect of each of the procedure bodies in terms of the abstraction. This proof method is described in detail in [13].
4. Example: Bounded Buffer
A bounded buffer is a concrete representation of the abstract idea of a sequence of portions. The sequence is accessible to two programs running in parallel: the first of these (the producer) updates the sequence by append- ing a new portion x at the end; and the second (the consumer) updates it by removing the first portion. The initial value of the sequence is empty. We thus require two operations:
(1) append(x:portion) ;
which should be equivalent to the abstract operation
sequence := sequence n (x);
where (x) is the sequence whose only item is x and n de- notes concatenation of two sequences.
which should be equivalent to the abstract operations x := first(sequence); sequence := rest(sequence);
where first selects the first item of a sequence and rest denotes the sequence with its first item removed. Ob- viously, if the sequence is empty, first is undefined; and in this case we want to ensure that the consumer waits until the producer has made the sequence nonempty.
We shall assume that the amount of time taken to produce a portion or consume it is large in comparison with the time taken to append or remove it from the sequence. We may therefore be justified in making a design in which producer and consumer can both update the sequence, but not simultaneously•
The sequence is represented by an array: buffer :array 0..N — 1 of portion;
and two variables:
(1) lastpointer:O..N- 1;
which points to the buffer position into which the next append operation will put a new item, and
(2) count:O..N;
which always holds the length of the sequence (initially 0).
We define the function
seq (b,l,c) =dSifC= 0thenempty
else seq(b,lOl,c- 1) n(b[lG1]) where the circled operations are taken modulo N. Note
that ifc ~ O,
remove(result x: portion) ;
The definition of the abstract sequence in terms of its concrete representation may now be given:
sequence =as seq(buffer, lastpointer, count) Less formally, this may be written
sequence =as (buffer[lastpointerOcount ], buffer[lastpointerOcountQ1 ],
buffe r[lastpointerO 1])
Another way of conveying this information would be by an example and a picture, which would be even less formal.
The invariant for the monitor is:
0 <_count < N &0 <_lastpointer < N -- 1
There are two reasons for waiting, which must be represented by condition variables:
nonempty :condition;
means that the count is greater than 0, and
nonfull: condition;
means that the count is less than N.
first(seq(b,l,c) ) = b[l~c] rest(seq(b,l,c)) = seq(b,l,c- 1)
Communications of
October 1974 Volume 17 Number 10
With this constructive approach to the design [8], it is relatively easy to code the monitor without error.
bounded buffer:monitor
beginbuffer:array 0..N -- 1ofportion;
lastpointer:O. .N -- 1; count'.O. .N;
nonempty ,nonfull :condition;
procedure append(x :portion) ;
begin if count = N then nonfull, wait;
note 0 < count < N; buffer[lastpointer] := x; lastpointer := lastpointer @ 1; count := count--}-1;
nonempty, signal
end append;
procedure remove(resultx :portion) ;
begin if count = 0 then nonempty, wait; note 0 < count < N;
x := buffer[lastpointerOeount];
nonfull. signal end remove;
count := 0; lastpointer := 0; end bounded buffer;
A formal proof of the correctness of this monitor with respect to the stated abstraction and invariant can be given if desired by techniques described in [13]. How- ever, these techniques seem not capable of dealing with subsequent examples of this paper.
Single-buffered input and output may be regarded as a special case of the bounded buffer with N = I. In this ease, the array can be replaced by a single variable, the lastpointer is redundant, and we get:
iostream :monitor begin buffer:portion;
count: O.. l ;
nonempty,nonfull: condition; procedure append(x :portion) ;
begin if count = 1 then nonfull. wait; buffer := x;
count := 1;
nonempty, signal
end append;
procedure remove(result x :portion) ;
begin if count = 0 then nonempty.wait; x := buffer;
count := 0;
nonfull. signal
end remove; count := 0;
end iostream;
If physical output is carried out by a separate special purpose channel, then the interrupt from the channel should simulate a call of iostream.remove(x); and similarly for physical in
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com