xref: /plan9/sys/doc/sleep.ms (revision 426d2b71458df9b491ba6c167f699b3f1f7b0428)
1*426d2b71SDavid du Colombier.HTML "Process Sleep and Wakeup on a Shared-memory Multiprocessor
2219b2ee8SDavid du Colombier.TL
3219b2ee8SDavid du ColombierProcess Sleep and Wakeup on a Shared-memory Multiprocessor
4219b2ee8SDavid du Colombier.AU
5219b2ee8SDavid du ColombierRob Pike
6219b2ee8SDavid du ColombierDave Presotto
7219b2ee8SDavid du ColombierKen Thompson
8219b2ee8SDavid du ColombierGerard Holzmann
9219b2ee8SDavid du Colombier.sp
107dd7cddfSDavid du Colombierrob,presotto,ken,gerard@plan9.bell-labs.com
11219b2ee8SDavid du Colombier.AB
127dd7cddfSDavid du Colombier.FS
137dd7cddfSDavid du ColombierAppeared in a slightly different form in
147dd7cddfSDavid du Colombier.I
157dd7cddfSDavid du ColombierProceedings of the Spring 1991 EurOpen Conference,
167dd7cddfSDavid du Colombier.R
177dd7cddfSDavid du ColombierTromsø, Norway, 1991, pp. 161-166.
187dd7cddfSDavid du Colombier.FE
19219b2ee8SDavid du ColombierThe problem of enabling a `sleeping' process on a shared-memory multiprocessor
20219b2ee8SDavid du Colombieris a difficult one, especially if the process is to be awakened by an interrupt-time
21219b2ee8SDavid du Colombierevent.  We present here the code
22219b2ee8SDavid du Colombierfor sleep and wakeup primitives that we use in our multiprocessor system.
23219b2ee8SDavid du ColombierThe code has been exercised by years of active use and by a verification
24219b2ee8SDavid du Colombiersystem.
25219b2ee8SDavid du Colombier.AE
26219b2ee8SDavid du Colombier.LP
27219b2ee8SDavid du ColombierOur problem is to synchronise processes on a symmetric shared-memory multiprocessor.
28219b2ee8SDavid du ColombierProcesses suspend execution, or
29219b2ee8SDavid du Colombier.I sleep,
30219b2ee8SDavid du Colombierwhile awaiting an enabling event such as an I/O interrupt.
31219b2ee8SDavid du ColombierWhen the event occurs, the process is issued a
32219b2ee8SDavid du Colombier.I wakeup
33219b2ee8SDavid du Colombierto resume its execution.
34219b2ee8SDavid du ColombierDuring these events, other processes may be running and other interrupts
35219b2ee8SDavid du Colombieroccurring on other processors.
36219b2ee8SDavid du Colombier.LP
37219b2ee8SDavid du ColombierMore specifically, we wish to implement subroutines called
38219b2ee8SDavid du Colombier.CW sleep ,
39219b2ee8SDavid du Colombiercallable by a process to relinquish control of its current processor,
40219b2ee8SDavid du Colombierand
41219b2ee8SDavid du Colombier.CW wakeup ,
42219b2ee8SDavid du Colombiercallable by another process or an interrupt to resume the execution
43219b2ee8SDavid du Colombierof a suspended process.
44219b2ee8SDavid du ColombierThe calling conventions of these subroutines will remain unspecified
45219b2ee8SDavid du Colombierfor the moment.
46219b2ee8SDavid du Colombier.LP
47219b2ee8SDavid du ColombierWe assume the processors have an atomic test-and-set or equivalent
48219b2ee8SDavid du Colombieroperation but no other synchronisation method.  Also, we assume interrupts
49219b2ee8SDavid du Colombiercan occur on any processor at any time, except on a processor that has
50219b2ee8SDavid du Colombierlocally inhibited them.
51219b2ee8SDavid du Colombier.LP
52219b2ee8SDavid du ColombierThe problem is the generalisation to a multiprocessor of a familiar
53219b2ee8SDavid du Colombierand well-understood uniprocessor problem.  It may be reduced to a
54219b2ee8SDavid du Colombieruniprocessor problem by using a global test-and-set to serialise the
55219b2ee8SDavid du Colombiersleeps and wakeups,
56219b2ee8SDavid du Colombierwhich is equivalent to synchronising through a monitor.
57219b2ee8SDavid du ColombierFor performance and cleanliness, however,
58219b2ee8SDavid du Colombierwe prefer to allow the interrupt handling and process control to be multiprocessed.
59219b2ee8SDavid du Colombier.LP
60219b2ee8SDavid du ColombierOur attempts to solve the sleep/wakeup problem in Plan 9
61219b2ee8SDavid du Colombier[Pik90]
62219b2ee8SDavid du Colombierprompted this paper.
63219b2ee8SDavid du ColombierWe implemented solutions several times over several months and each
64219b2ee8SDavid du Colombiertime convinced ourselves \(em wrongly \(em they were correct.
65219b2ee8SDavid du ColombierMultiprocessor algorithms can be
66219b2ee8SDavid du Colombierdifficult to prove correct by inspection and formal reasoning about them
67219b2ee8SDavid du Colombieris impractical.  We finally developed an algorithm we trust by
68219b2ee8SDavid du Colombierverifying our code using an
69219b2ee8SDavid du Colombierempirical testing tool.
70219b2ee8SDavid du ColombierWe present that code here, along with some comments about the process by
71219b2ee8SDavid du Colombierwhich it was designed.
72219b2ee8SDavid du Colombier.SH
73219b2ee8SDavid du ColombierHistory
74219b2ee8SDavid du Colombier.LP
75219b2ee8SDavid du ColombierSince processes in Plan 9 and the UNIX
76219b2ee8SDavid du Colombiersystem have similar structure and properties, one might ask if
77219b2ee8SDavid du ColombierUNIX
78219b2ee8SDavid du Colombier.CW sleep
79219b2ee8SDavid du Colombierand
80219b2ee8SDavid du Colombier.CW wakeup
81219b2ee8SDavid du Colombier[Bac86]
82219b2ee8SDavid du Colombiercould not easily be adapted from their standard uniprocessor implementation
83219b2ee8SDavid du Colombierto our multiprocessor needs.
84219b2ee8SDavid du ColombierThe short answer is, no.
85219b2ee8SDavid du Colombier.LP
86219b2ee8SDavid du ColombierThe
87219b2ee8SDavid du ColombierUNIX
88219b2ee8SDavid du Colombierroutines
89219b2ee8SDavid du Colombiertake as argument a single global address
90219b2ee8SDavid du Colombierthat serves as a unique
91219b2ee8SDavid du Colombieridentifier to connect the wakeup with the appropriate process or processes.
92219b2ee8SDavid du ColombierThis has several inherent disadvantages.
93219b2ee8SDavid du ColombierFrom the point of view of
94219b2ee8SDavid du Colombier.CW sleep
95219b2ee8SDavid du Colombierand
96219b2ee8SDavid du Colombier.CW wakeup ,
97219b2ee8SDavid du Colombierit is difficult to associate a data structure with an arbitrary address;
98219b2ee8SDavid du Colombierthe routines are unable to maintain a state variable recording the
99219b2ee8SDavid du Colombierstatus of the event and processes.
100219b2ee8SDavid du Colombier(The reverse is of course easy \(em we could
101219b2ee8SDavid du Colombierrequire the address to point to a special data structure \(em
102219b2ee8SDavid du Colombierbut we are investigating
103219b2ee8SDavid du ColombierUNIX
104219b2ee8SDavid du Colombier.CW sleep
105219b2ee8SDavid du Colombierand
106219b2ee8SDavid du Colombier.CW wakeup ,
107219b2ee8SDavid du Colombiernot the code that calls them.)
108219b2ee8SDavid du ColombierAlso, multiple processes sleep `on' a given address, so
109219b2ee8SDavid du Colombier.CW wakeup
110219b2ee8SDavid du Colombiermust enable them all, and let process scheduling determine which process
111219b2ee8SDavid du Colombieractually benefits from the event.
112219b2ee8SDavid du ColombierThis is inefficient;
113219b2ee8SDavid du Colombiera queueing mechanism would be preferable
114219b2ee8SDavid du Colombierbut, again, it is difficult to associate a queue with a general address.
115219b2ee8SDavid du ColombierMoreover, the lack of state means that
116219b2ee8SDavid du Colombier.CW sleep
117219b2ee8SDavid du Colombierand
118219b2ee8SDavid du Colombier.CW wakeup
119219b2ee8SDavid du Colombiercannot know what the corresponding process (or interrupt) is doing;
120219b2ee8SDavid du Colombier.CW sleep
121219b2ee8SDavid du Colombierand
122219b2ee8SDavid du Colombier.CW wakeup
123219b2ee8SDavid du Colombiermust be executed atomically.
124219b2ee8SDavid du ColombierOn a uniprocessor it suffices to disable interrupts during their
125219b2ee8SDavid du Colombierexecution.
126219b2ee8SDavid du ColombierOn a multiprocessor, however,
127219b2ee8SDavid du Colombiermost processors
128219b2ee8SDavid du Colombiercan inhibit interrupts only on the current processor,
129219b2ee8SDavid du Colombierso while a process is executing
130219b2ee8SDavid du Colombier.CW sleep
131219b2ee8SDavid du Colombierthe desired interrupt can come and go on another processor.
132219b2ee8SDavid du ColombierIf the wakeup is to be issued by another process, the problem is even harder.
133219b2ee8SDavid du ColombierSome inter-process mutual exclusion mechanism must be used,
134219b2ee8SDavid du Colombierwhich, yet again, is difficult to do without a way to communicate state.
135219b2ee8SDavid du Colombier.LP
136219b2ee8SDavid du ColombierIn summary, to be useful on a multiprocessor,
137219b2ee8SDavid du ColombierUNIX
138219b2ee8SDavid du Colombier.CW sleep
139219b2ee8SDavid du Colombierand
140219b2ee8SDavid du Colombier.CW wakeup
141219b2ee8SDavid du Colombiermust either be made to run atomically on a single
142219b2ee8SDavid du Colombierprocessor (such as by using a monitor)
143219b2ee8SDavid du Colombieror they need a richer model for their communication.
144219b2ee8SDavid du Colombier.SH
145219b2ee8SDavid du ColombierThe design
146219b2ee8SDavid du Colombier.LP
147219b2ee8SDavid du ColombierConsider the case of an interrupt waking up a sleeping process.
148219b2ee8SDavid du Colombier(The other case, a process awakening a second process, is easier because
149219b2ee8SDavid du Colombieratomicity can be achieved using an interlock.)
150219b2ee8SDavid du ColombierThe sleeping process is waiting for some event to occur, which may be
151219b2ee8SDavid du Colombiermodeled by a condition coming true.
152219b2ee8SDavid du ColombierThe condition could be just that the event has happened, or something
153219b2ee8SDavid du Colombiermore subtle such as a queue draining below some low-water mark.
154219b2ee8SDavid du ColombierWe represent the condition by a function of one
155219b2ee8SDavid du Colombierargument of type
156219b2ee8SDavid du Colombier.CW void* ;
157219b2ee8SDavid du Colombierthe code supporting the device generating the interrupts
158219b2ee8SDavid du Colombierprovides such a function to be used by
159219b2ee8SDavid du Colombier.CW sleep
160219b2ee8SDavid du Colombierand
161219b2ee8SDavid du Colombier.CW wakeup
162219b2ee8SDavid du Colombierto synchronise.  The function returns
163219b2ee8SDavid du Colombier.CW false
164219b2ee8SDavid du Colombierif the event has not occurred, and
165219b2ee8SDavid du Colombier.CW true
166219b2ee8SDavid du Colombiersome time after the event has occurred.
167219b2ee8SDavid du ColombierThe
168219b2ee8SDavid du Colombier.CW sleep
169219b2ee8SDavid du Colombierand
170219b2ee8SDavid du Colombier.CW wakeup
171219b2ee8SDavid du Colombierroutines must, of course, work correctly if the
172219b2ee8SDavid du Colombierevent occurs while the process is executing
173219b2ee8SDavid du Colombier.CW sleep .
174219b2ee8SDavid du Colombier.LP
175219b2ee8SDavid du ColombierWe assume that a particular call to
176219b2ee8SDavid du Colombier.CW sleep
177219b2ee8SDavid du Colombiercorresponds to a particular call to
178219b2ee8SDavid du Colombier.CW wakeup ,
179219b2ee8SDavid du Colombierthat is,
180219b2ee8SDavid du Colombierat most one process is asleep waiting for a particular event.
181219b2ee8SDavid du ColombierThis can be guaranteed in the code that calls
182219b2ee8SDavid du Colombier.CW sleep
183219b2ee8SDavid du Colombierand
184219b2ee8SDavid du Colombier.CW wakeup
185219b2ee8SDavid du Colombierby appropriate interlocks.
186219b2ee8SDavid du ColombierWe also assume for the moment that there will be only one interrupt
187219b2ee8SDavid du Colombierand that it may occur at any time, even before
188219b2ee8SDavid du Colombier.CW sleep
189219b2ee8SDavid du Colombierhas been called.
190219b2ee8SDavid du Colombier.LP
191219b2ee8SDavid du ColombierFor performance,
192219b2ee8SDavid du Colombierwe desire that multiple instances of
193219b2ee8SDavid du Colombier.CW sleep
194219b2ee8SDavid du Colombierand
195219b2ee8SDavid du Colombier.CW wakeup
196219b2ee8SDavid du Colombiermay be running simultaneously on our multiprocessor.
197219b2ee8SDavid du ColombierFor example, a process calling
198219b2ee8SDavid du Colombier.CW sleep
199219b2ee8SDavid du Colombierto await a character from an input channel need not
200219b2ee8SDavid du Colombierwait for another process to finish executing
201219b2ee8SDavid du Colombier.CW sleep
202219b2ee8SDavid du Colombierto await a disk block.
203219b2ee8SDavid du ColombierAt a finer level, we would like a process reading from one input channel
204219b2ee8SDavid du Colombierto be able to execute
205219b2ee8SDavid du Colombier.CW sleep
206219b2ee8SDavid du Colombierin parallel with a process reading from another input channel.
207219b2ee8SDavid du ColombierA standard approach to synchronisation is to interlock the channel `driver'
208219b2ee8SDavid du Colombierso that only one process may be executing in the channel code at once.
209219b2ee8SDavid du ColombierThis method is clearly inadequate for our purposes; we need
210219b2ee8SDavid du Colombierfine-grained synchronisation, and in particular to apply
211219b2ee8SDavid du Colombierinterlocks at the level of individual channels rather than at the level
212219b2ee8SDavid du Colombierof the channel driver.
213219b2ee8SDavid du Colombier.LP
214219b2ee8SDavid du ColombierOur approach is to use an object called a
215219b2ee8SDavid du Colombier.I rendezvous ,
216219b2ee8SDavid du Colombierwhich is a data structure through which
217219b2ee8SDavid du Colombier.CW sleep
218219b2ee8SDavid du Colombierand
219219b2ee8SDavid du Colombier.CW wakeup
220219b2ee8SDavid du Colombiersynchronise.
221219b2ee8SDavid du Colombier(The similarly named construct in Ada is a control structure;
222219b2ee8SDavid du Colombierours is an unrelated data structure.)
223219b2ee8SDavid du ColombierA rendezvous
224219b2ee8SDavid du Colombieris allocated for each active source of events:
225219b2ee8SDavid du Colombierone for each I/O channel,
226219b2ee8SDavid du Colombierone for each end of a pipe, and so on.
227219b2ee8SDavid du ColombierThe rendezvous serves as an interlockable structure in which to record
228219b2ee8SDavid du Colombierthe state of the sleeping process, so that
229219b2ee8SDavid du Colombier.CW sleep
230219b2ee8SDavid du Colombierand
231219b2ee8SDavid du Colombier.CW wakeup
232219b2ee8SDavid du Colombiercan communicate if the event happens before or while
233219b2ee8SDavid du Colombier.CW sleep
234219b2ee8SDavid du Colombieris executing.
235219b2ee8SDavid du Colombier.LP
236219b2ee8SDavid du ColombierOur design for
237219b2ee8SDavid du Colombier.CW sleep
238219b2ee8SDavid du Colombieris therefore a function
239219b2ee8SDavid du Colombier.P1
240219b2ee8SDavid du Colombiervoid sleep(Rendezvous *r, int (*condition)(void*), void *arg)
241219b2ee8SDavid du Colombier.P2
242219b2ee8SDavid du Colombiercalled by the sleeping process.
243219b2ee8SDavid du ColombierThe argument
244219b2ee8SDavid du Colombier.CW r
245219b2ee8SDavid du Colombierconnects the call to
246219b2ee8SDavid du Colombier.CW sleep
247219b2ee8SDavid du Colombierwith the call to
248219b2ee8SDavid du Colombier.CW wakeup ,
249219b2ee8SDavid du Colombierand is part of the data structure for the (say) device.
250219b2ee8SDavid du ColombierThe function
251219b2ee8SDavid du Colombier.CW condition
252219b2ee8SDavid du Colombieris described above;
253219b2ee8SDavid du Colombiercalled with argument
254219b2ee8SDavid du Colombier.CW arg ,
255219b2ee8SDavid du Colombierit is used by
256219b2ee8SDavid du Colombier.CW sleep
257219b2ee8SDavid du Colombierto decide whether the event has occurred.
258219b2ee8SDavid du Colombier.CW Wakeup
259219b2ee8SDavid du Colombierhas a simpler specification:
260219b2ee8SDavid du Colombier.P1
261219b2ee8SDavid du Colombiervoid wakeup(Rendezvous *r).
262219b2ee8SDavid du Colombier.P2
263219b2ee8SDavid du Colombier.CW Wakeup
264219b2ee8SDavid du Colombiermust be called after the condition has become true.
265219b2ee8SDavid du Colombier.SH
266219b2ee8SDavid du ColombierAn implementation
267219b2ee8SDavid du Colombier.LP
268219b2ee8SDavid du ColombierThe
269219b2ee8SDavid du Colombier.CW Rendezvous
270219b2ee8SDavid du Colombierdata type is defined as
271219b2ee8SDavid du Colombier.P1
272219b2ee8SDavid du Colombiertypedef struct{
273219b2ee8SDavid du Colombier	Lock	l;
274219b2ee8SDavid du Colombier	Proc	*p;
275219b2ee8SDavid du Colombier}Rendezvous;
276219b2ee8SDavid du Colombier.P2
277219b2ee8SDavid du ColombierOur
278219b2ee8SDavid du Colombier.CW Locks
279219b2ee8SDavid du Colombierare test-and-set spin locks.
280219b2ee8SDavid du ColombierThe routine
281219b2ee8SDavid du Colombier.CW lock(Lock\ *l)
282219b2ee8SDavid du Colombierreturns when the current process holds that lock;
283219b2ee8SDavid du Colombier.CW unlock(Lock\ *l)
284219b2ee8SDavid du Colombierreleases the lock.
285219b2ee8SDavid du Colombier.LP
286219b2ee8SDavid du ColombierHere is our implementation of
287219b2ee8SDavid du Colombier.CW sleep .
288219b2ee8SDavid du ColombierIts details are discussed below.
289219b2ee8SDavid du Colombier.CW Thisp
290219b2ee8SDavid du Colombieris a pointer to the current process on the current processor.
291219b2ee8SDavid du Colombier(Its value differs on each processor.)
292219b2ee8SDavid du Colombier.P1
293219b2ee8SDavid du Colombiervoid
294219b2ee8SDavid du Colombiersleep(Rendezvous *r, int (*condition)(void*), void *arg)
295219b2ee8SDavid du Colombier{
296219b2ee8SDavid du Colombier	int s;
297219b2ee8SDavid du Colombier
298219b2ee8SDavid du Colombier	s = inhibit();		/* interrupts */
299219b2ee8SDavid du Colombier	lock(&r->l);
300219b2ee8SDavid du Colombier
301219b2ee8SDavid du Colombier	/*
302219b2ee8SDavid du Colombier	 * if condition happened, never mind
303219b2ee8SDavid du Colombier	 */
304219b2ee8SDavid du Colombier	if((*condition)(arg)){
305219b2ee8SDavid du Colombier		unlock(&r->l);
306219b2ee8SDavid du Colombier		allow();	/* interrupts */
307219b2ee8SDavid du Colombier		return;
308219b2ee8SDavid du Colombier	}
309219b2ee8SDavid du Colombier
310219b2ee8SDavid du Colombier	/*
311219b2ee8SDavid du Colombier	 * now we are committed to
312219b2ee8SDavid du Colombier	 * change state and call scheduler
313219b2ee8SDavid du Colombier	 */
314219b2ee8SDavid du Colombier	if(r->p)
315219b2ee8SDavid du Colombier		error("double sleep %d %d", r->p->pid, thisp->pid);
316219b2ee8SDavid du Colombier	thisp->state = Wakeme;
317219b2ee8SDavid du Colombier	r->p = thisp;
318219b2ee8SDavid du Colombier	unlock(&r->l);
319219b2ee8SDavid du Colombier	allow(s);	/* interrupts */
320219b2ee8SDavid du Colombier	sched();	/* relinquish CPU */
321219b2ee8SDavid du Colombier}
322219b2ee8SDavid du Colombier.P2
323219b2ee8SDavid du Colombier.ne 3i
324219b2ee8SDavid du ColombierHere is
325219b2ee8SDavid du Colombier.CW wakeup.
326219b2ee8SDavid du Colombier.P1
327219b2ee8SDavid du Colombiervoid
328219b2ee8SDavid du Colombierwakeup(Rendezvous *r)
329219b2ee8SDavid du Colombier{
330219b2ee8SDavid du Colombier	Proc *p;
331219b2ee8SDavid du Colombier	int s;
332219b2ee8SDavid du Colombier
333219b2ee8SDavid du Colombier	s = inhibit();	/* interrupts; return old state */
334219b2ee8SDavid du Colombier	lock(&r->l);
335219b2ee8SDavid du Colombier	p = r->p;
336219b2ee8SDavid du Colombier	if(p){
337219b2ee8SDavid du Colombier		r->p = 0;
338219b2ee8SDavid du Colombier		if(p->state != Wakeme)
339219b2ee8SDavid du Colombier			panic("wakeup: not Wakeme");
340219b2ee8SDavid du Colombier		ready(p);
341219b2ee8SDavid du Colombier	}
342219b2ee8SDavid du Colombier	unlock(&r->l);
343219b2ee8SDavid du Colombier	if(s)
344219b2ee8SDavid du Colombier		allow();
345219b2ee8SDavid du Colombier}
346219b2ee8SDavid du Colombier.P2
347219b2ee8SDavid du Colombier.CW Sleep
348219b2ee8SDavid du Colombierand
349219b2ee8SDavid du Colombier.CW wakeup
350219b2ee8SDavid du Colombierboth begin by disabling interrupts
351219b2ee8SDavid du Colombierand then locking the rendezvous structure.
352219b2ee8SDavid du ColombierBecause
353219b2ee8SDavid du Colombier.CW wakeup
354219b2ee8SDavid du Colombiermay be called in an interrupt routine, the lock must be set only
355219b2ee8SDavid du Colombierwith interrupts disabled on the current processor,
356219b2ee8SDavid du Colombierso that if the interrupt comes during
357219b2ee8SDavid du Colombier.CW sleep
358219b2ee8SDavid du Colombierit will occur only on a different processor;
359219b2ee8SDavid du Colombierif it occurred on the processor executing
360219b2ee8SDavid du Colombier.CW sleep ,
361219b2ee8SDavid du Colombierthe spin lock in
362219b2ee8SDavid du Colombier.CW wakeup
363219b2ee8SDavid du Colombierwould hang forever.
364219b2ee8SDavid du ColombierAt the end of each routine, the lock is released and processor priority
365219b2ee8SDavid du Colombierreturned to its previous value.
366219b2ee8SDavid du Colombier.CW Wakeup "" (
367219b2ee8SDavid du Colombierneeds to inhibit interrupts in case
368219b2ee8SDavid du Colombierit is being called by a process;
369219b2ee8SDavid du Colombierthis is a no-op if called by an interrupt.)
370219b2ee8SDavid du Colombier.LP
371219b2ee8SDavid du Colombier.CW Sleep
372219b2ee8SDavid du Colombierchecks to see if the condition has become true, and returns if so.
373219b2ee8SDavid du ColombierOtherwise the process posts its name in the rendezvous structure where
374219b2ee8SDavid du Colombier.CW wakeup
375219b2ee8SDavid du Colombiermay find it, marks its state as waiting to be awakened
376219b2ee8SDavid du Colombier(this is for error checking only) and goes to sleep by calling
377219b2ee8SDavid du Colombier.CW sched() .
378219b2ee8SDavid du ColombierThe manipulation of the rendezvous structure is all done under the lock,
379219b2ee8SDavid du Colombierand
380219b2ee8SDavid du Colombier.CW wakeup
381219b2ee8SDavid du Colombieronly examines it under lock, so atomicity and mutual exclusion
382219b2ee8SDavid du Colombierare guaranteed.
383219b2ee8SDavid du Colombier.LP
384219b2ee8SDavid du Colombier.CW Wakeup
385219b2ee8SDavid du Colombierhas a simpler job.  When it is called, the condition has implicitly become true,
386219b2ee8SDavid du Colombierso it locks the rendezvous, sees if a process is waiting, and readies it to run.
387219b2ee8SDavid du Colombier.SH
388219b2ee8SDavid du ColombierDiscussion
389219b2ee8SDavid du Colombier.LP
390219b2ee8SDavid du ColombierThe synchronisation technique used here
391219b2ee8SDavid du Colombieris similar to known methods, even as far back as Saltzer's thesis
392219b2ee8SDavid du Colombier[Sal66].
393219b2ee8SDavid du ColombierThe code looks trivially correct in retrospect: all access to data structures is done
394219b2ee8SDavid du Colombierunder lock, and there is no place that things may get out of order.
395219b2ee8SDavid du ColombierNonetheless, it took us several iterations to arrive at the above
396219b2ee8SDavid du Colombierimplementation, because the things that
397219b2ee8SDavid du Colombier.I can
398219b2ee8SDavid du Colombiergo wrong are often hard to see.  We had four earlier implementations
399219b2ee8SDavid du Colombierthat were examined at great length and only found faulty when a new,
400219b2ee8SDavid du Colombierdifferent style of device or activity was added to the system.
401219b2ee8SDavid du Colombier.LP
402219b2ee8SDavid du Colombier.ne 3i
403219b2ee8SDavid du ColombierHere, for example, is an incorrect implementation of wakeup,
404219b2ee8SDavid du Colombierclosely related to one of our versions.
405219b2ee8SDavid du Colombier.P1
406219b2ee8SDavid du Colombiervoid
407219b2ee8SDavid du Colombierwakeup(Rendezvous *r)
408219b2ee8SDavid du Colombier{
409219b2ee8SDavid du Colombier	Proc *p;
410219b2ee8SDavid du Colombier	int s;
411219b2ee8SDavid du Colombier
412219b2ee8SDavid du Colombier	p = r->p;
413219b2ee8SDavid du Colombier	if(p){
414219b2ee8SDavid du Colombier		s = inhibit();
415219b2ee8SDavid du Colombier		lock(&r->l);
416219b2ee8SDavid du Colombier		r->p = 0;
417219b2ee8SDavid du Colombier		if(p->state != Wakeme)
418219b2ee8SDavid du Colombier			panic("wakeup: not Wakeme");
419219b2ee8SDavid du Colombier		ready(p);
420219b2ee8SDavid du Colombier		unlock(&r->l);
421219b2ee8SDavid du Colombier		if(s)
422219b2ee8SDavid du Colombier			allow();
423219b2ee8SDavid du Colombier	}
424219b2ee8SDavid du Colombier}
425219b2ee8SDavid du Colombier.P2
426219b2ee8SDavid du ColombierThe mistake is that the reading of
427219b2ee8SDavid du Colombier.CW r->p
428219b2ee8SDavid du Colombiermay occur just as the other process calls
429219b2ee8SDavid du Colombier.CW sleep ,
430219b2ee8SDavid du Colombierso when the interrupt examines the structure it sees no one to wake up,
431219b2ee8SDavid du Colombierand the sleeping process misses its wakeup.
432219b2ee8SDavid du ColombierWe wrote the code this way because we reasoned that the fetch
433219b2ee8SDavid du Colombier.CW p
434219b2ee8SDavid du Colombier.CW =
435219b2ee8SDavid du Colombier.CW r->p
436219b2ee8SDavid du Colombierwas inherently atomic and need not be interlocked.
437219b2ee8SDavid du ColombierThe bug was found by examination when a new, very fast device
438219b2ee8SDavid du Colombierwas added to the system and sleeps and interrupts were closely overlapped.
439219b2ee8SDavid du ColombierHowever, it was in the system for a couple of months without causing an error.
440219b2ee8SDavid du Colombier.LP
441219b2ee8SDavid du ColombierHow many errors lurk in our supposedly correct implementation above?
442219b2ee8SDavid du ColombierWe would like a way to guarantee correctness; formal proofs are beyond
443219b2ee8SDavid du Colombierour abilities when the subtleties of interrupts and multiprocessors are
444219b2ee8SDavid du Colombierinvolved.
445219b2ee8SDavid du ColombierWith that in mind, the first three authors approached the last to see
446219b2ee8SDavid du Colombierif his automated tool for checking protocols
447219b2ee8SDavid du Colombier[Hol91]
448219b2ee8SDavid du Colombiercould be
449219b2ee8SDavid du Colombierused to verify our new
450219b2ee8SDavid du Colombier.CW sleep
451219b2ee8SDavid du Colombierand
452219b2ee8SDavid du Colombier.CW wakeup
453219b2ee8SDavid du Colombierfor correctness.
454219b2ee8SDavid du ColombierThe code was translated into the language for that system
455219b2ee8SDavid du Colombier(with, unfortunately, no way of proving that the translation is itself correct)
456219b2ee8SDavid du Colombierand validated by exhaustive simulation.
457219b2ee8SDavid du Colombier.LP
458219b2ee8SDavid du ColombierThe validator found a bug.
459219b2ee8SDavid du ColombierUnder our assumption that there is only one interrupt, the bug cannot
460219b2ee8SDavid du Colombieroccur, but in the more general case of multiple interrupts synchronising
461219b2ee8SDavid du Colombierthrough the same condition function and rendezvous,
462219b2ee8SDavid du Colombierthe process and interrupt can enter a peculiar state.
463219b2ee8SDavid du ColombierA process may return from
464219b2ee8SDavid du Colombier.CW sleep
465219b2ee8SDavid du Colombierwith the condition function false
466219b2ee8SDavid du Colombierif there is a delay between
467219b2ee8SDavid du Colombierthe condition coming true and
468219b2ee8SDavid du Colombier.CW wakeup
469219b2ee8SDavid du Colombierbeing called,
470219b2ee8SDavid du Colombierwith the delay occurring
471219b2ee8SDavid du Colombierjust as the receiving process calls
472219b2ee8SDavid du Colombier.CW sleep .
473219b2ee8SDavid du ColombierThe condition is now true, so that process returns immediately,
474219b2ee8SDavid du Colombierdoes whatever is appropriate, and then (say) decides to call
475219b2ee8SDavid du Colombier.CW sleep
476219b2ee8SDavid du Colombieragain.  This time the condition is false, so it goes to sleep.
477219b2ee8SDavid du ColombierThe wakeup process then finds a sleeping process,
478219b2ee8SDavid du Colombierand wakes it up, but the condition is now false.
479219b2ee8SDavid du Colombier.LP
480219b2ee8SDavid du ColombierThere is an easy (and verified) solution: at the end of
481219b2ee8SDavid du Colombier.CW sleep
482219b2ee8SDavid du Colombieror after
483219b2ee8SDavid du Colombier.CW sleep
484219b2ee8SDavid du Colombierreturns,
485219b2ee8SDavid du Colombierif the condition is false, execute
486219b2ee8SDavid du Colombier.CW sleep
487219b2ee8SDavid du Colombieragain.  This re-execution cannot repeat; the second synchronisation is guaranteed
488219b2ee8SDavid du Colombierto function under the external conditions we are supposing.
489219b2ee8SDavid du Colombier.LP
490219b2ee8SDavid du ColombierEven though the original code is completely
491219b2ee8SDavid du Colombierprotected by interlocks and had been examined carefully by all of us
492219b2ee8SDavid du Colombierand believed correct, it still had problems.
493219b2ee8SDavid du ColombierIt seems to us that some exhaustive automated analysis is
494219b2ee8SDavid du Colombierrequired of multiprocessor algorithms to guarantee their safety.
495219b2ee8SDavid du ColombierOur experience has confirmed that it is almost impossible to
496219b2ee8SDavid du Colombierguarantee by inspection or simple testing the correctness
497219b2ee8SDavid du Colombierof a multiprocessor algorithm.  Testing can demonstrate the presence
498219b2ee8SDavid du Colombierof bugs but not their absence
499219b2ee8SDavid du Colombier[Dij72].
500219b2ee8SDavid du Colombier.LP
501219b2ee8SDavid du ColombierWe close by claiming that the code above with
502219b2ee8SDavid du Colombierthe suggested modification passes all tests we have for correctness
503219b2ee8SDavid du Colombierunder the assumptions used in the validation.
504219b2ee8SDavid du ColombierWe would not, however, go so far as to claim that it is universally correct.
505219b2ee8SDavid du Colombier.SH
506219b2ee8SDavid du ColombierReferences
507219b2ee8SDavid du Colombier.LP
508219b2ee8SDavid du Colombier[Bac86] Maurice J. Bach,
509219b2ee8SDavid du Colombier.I "The Design of the UNIX Operating System,
510219b2ee8SDavid du ColombierPrentice-Hall,
511219b2ee8SDavid du ColombierEnglewood Cliffs,
512219b2ee8SDavid du Colombier1986.
513219b2ee8SDavid du Colombier.LP
514219b2ee8SDavid du Colombier[Dij72] Edsger W. Dijkstra,
515219b2ee8SDavid du Colombier``The Humble Programmer \- 1972 Turing Award Lecture'',
516219b2ee8SDavid du Colombier.I "Comm. ACM,
517219b2ee8SDavid du Colombier15(10), pp. 859-866,
518219b2ee8SDavid du ColombierOctober 1972.
519219b2ee8SDavid du Colombier.LP
520219b2ee8SDavid du Colombier[Hol91] Gerard J. Holzmann,
521219b2ee8SDavid du Colombier.I "Design and Validation of Computer Protocols,
522219b2ee8SDavid du ColombierPrentice-Hall,
523219b2ee8SDavid du ColombierEnglewood Cliffs,
524219b2ee8SDavid du Colombier1991.
525219b2ee8SDavid du Colombier.LP
526219b2ee8SDavid du Colombier[Pik90]
527219b2ee8SDavid du ColombierRob Pike,
528219b2ee8SDavid du ColombierDave Presotto,
529219b2ee8SDavid du ColombierKen Thompson,
530219b2ee8SDavid du ColombierHoward Trickey,
531219b2ee8SDavid du Colombier``Plan 9 from Bell Labs'',
532219b2ee8SDavid du Colombier.I "Proceedings of the Summer 1990 UKUUG Conference,
533219b2ee8SDavid du Colombierpp. 1-9,
534219b2ee8SDavid du ColombierLondon,
535219b2ee8SDavid du ColombierJuly, 1990.
536219b2ee8SDavid du Colombier.LP
537219b2ee8SDavid du Colombier[Sal66] Jerome H. Saltzer,
538219b2ee8SDavid du Colombier.I "Traffic Control in a Multiplexed Computer System
539219b2ee8SDavid du ColombierMIT,
540219b2ee8SDavid du ColombierCambridge, Mass.,
541219b2ee8SDavid du Colombier1966.
542