MECHANISMS FOR SPECIFYING SCHEDULING POLICIES
Original Publication Date: 1899-Dec-30
Included in the Prior Art Database: 2007-Apr-12
Software Patent Institute
Schneider, F.B.: AUTHOR [+3]
F. 8. Schneider A. J. Bernstefn rG1 C1 G2 C2 . Gn Cnl sals contained in papers titled "Cbmmunicating Sequential his specifies the execution of exactly one of its consti- Processesw flt0ar781 and *Dlstrlbuted Processes" fBrin78al. tuent guarded commands. Note that tf more than one guard fs which are based on a message passfnq synchronization scheme. true then one sf the corresponding cmmand list8 IS selected arbitrarily. The elternatlve sumnnd !A undcflnrtd if none Crmmon to mnny recent ptogcamml nq languages Is the in- oE the quards ef the casstttt~ent qoardrvl carnmsndr; (GI, G?, &'I rr,; k01t 0 1 aYlbt.ncr lc trnLlil u:r 8 trnl hnko 4s~pllei t , all11 otLen . . ., Gn) is truo. Cunrded corsmandn may also be comblnsd l G l Ci GZ C2 . .. Cn Cnl which specifies as many executions of the alternative com- mand as possible. Consequently, when a l l constituent guards are false, the repetitive command terminates. Notice that in a guarded command program the logical assertions that would be part of a formal proof of that program are actually em- bedded in the program code a s the guards. Typically, a guarded command program is developed along with its proof of correctness.
MECHANISMS FOR SPECIFYING
F. B. Schneider and
A. J. Bernstein
F. B. Schneider?
A. J. Bernstein
Jan. 8, 1979
Ex tensions t o concur rent prog rarnrn f ng languages are presented which allow control of scheduling policies previously defined by the run-time support system. It is shown that the use of these mechanisms simplifies t h e solutions of concurrent programming problems. In addition, the p r o p s e d extensions allow easy identification of those aspects of a program concerned with perfor- mance, thereby making programs easier t o read and understand.
Keywords: ,.Concurrent Paszal, Monitors, Cc .ilnunicat-
ing Sequential Processes, Operating Systems, Scheduling Algorithms.
* T h i s work is partially supported b y NSF grant NCS
76-fl4828 and MCS 76-223Gfl.
1. Computer Science Department, Upson .Hall, Cornell Univer- sity, Ithaca, New York 14853.
2. Department of Computer Science, S.U.N.Y. a t Stony Brook, Stony Brook, New York 11?94.
help t a enforce, various correctness criteria. For example, fn Concurrent Pascal access to variables declared wlthin a monitor is guaranteed to be eutually exclusive. It follows from this and certain syntactic constraints of the language that a l l shared data in a Concurrent Pascal program i s pro- tected from simultaneous access fBecn781 fBr in751.
The guarded command language proposal of Dijkstra fDijk761 provides another illustration of the trend to make explicit various correctness crlterla. Central to this
It is wsfl known that the construction of software is language proposal is the enumeration of the logical precvn- made considerably easier by the use of high level languages. ditions necessary before the execution of a cornman+ can Prograins written in htgh level languages are easier to proceed. A guarded command has the form:
understand, modify (hence malntainl and formally verify than
their assrz~tly Ianquage Counterparts. Consequently, a 4006
d e ~ l OF research has been devoted to the definition of high where GI the guard, is a boolean expression, and C Is a com- level languages suitable for various environments and appli- mand list. C is only executed provided G is true. GuardeC cations. Of particular interest hare are those languages commands may be combined into an alternative command having and language proposals intended for writing asynchronous the form (the notation in [Hoar781 is used)
systems. Notable examples of such languages are Concurrent
Pascal rBrin751 and ~odulo [Wirt771, which are based on the
mcnitor construct IBrin77l IHoar741, and the language p...