120 ;;Quote: semaphores are the same as a mutex, but a thread does not "hold" a semaphore, there is no precondition for release, and P and V may be textual separated

120+;;Quote: if possible, use mutexes and condition variables instead of semaphores. They provide additional structure

120+;;Quote: use semaphores to synchronize with an interrupt routine; use P(sem) to block on the interrupt and V(sem) to signal an event

119 ;;Quote: use a formal specification for synchronization primitives on a multiprocessor; otherwise difficult questions about their precise semantics

120 ;;Quote: Larch divides a specification into mathematical abstractions and program interfaces

120 ;;Quote: formal specification of Modula-3 threads for safety properties and termination; ignores liveness

120+;;Quote: specify a non-atomic, concurrent procedure with a predicate that defines the allowable sequences of atomic actions

127 ;;Quote: programmers and implementers use the formal specification of Modula-3 threads

127+;;Quote: an untrained user found an error in the formal specification of Modula-3 threads; another error was missed for a year

129 ;;Quote: writing a good formal specification is difficult and time consuming; the hardest parts are understanding the object to be specified and developing the mathematical abstractions

129+;;Quote: systems programmers find formal specifications of concurrent programs helpful

129 ;;Quote: difficult to disentangle a concurrent program's behavior from the desired behavior for all implementations; requirement writers need the original designers