Key points are not available for this paper at this time.
Monitors are a convenient and powerful tool for writing schedulers in concurrent programs. There are at least four conventions for handling their wait and signal operations: the signaling process may yield to the waiting one, continue and thus leave the signal pending, or return immediately from the monitor; or signals may be performed automatically.Formal proof schemas are presented for each of the signaling conventions. Such schemas not only support proof of monitors, they also display the conventions' properties precisely and allow them to be compared. It is shown that all of the conventions are equivalent except for immediate return, which is strictly weaker than the others. A modification of immediate return which corrects its weakness and retains its desirable features is proposed.
John H. Howard (Wed,) studied this question.