QuoteRef: birrAD_1991a

topics > all references > ThesaHelp: references a-b

references a-b
critical regions
requirement specification
proving concurrent programs
managing shared memory
program proving
path expression
specification and design of distributed systems


Birrell, A.D., Guttag, J.V., Horning, J.J., Levin, R., "Thread synchronization: a formal specification", pp. 119-129, in Nelson, G. (ed.), Systems Programming in Modula-3, Englewood Cliffs, New Jersey, Prentice Hall, 1991. Google


boldface used for literals.

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

Related Topics up

ThesaHelp: references a-b (396 items)
Topic: critical regions (58 items)
Group: requirement specification   (11 topics, 306 quotes)
Topic: proving concurrent programs (37 items)
Topic: managing shared memory (74 items)
Group: program proving   (10 topics, 310 quotes)
Topic: path expression (14 items)
Topic: specification and design of distributed systems (14 items)

Collected barberCB 3/98
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.