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

Quotation Skeleton

our specification [for Modula-3 threads] deals only with safety properties … [p. 121] an atomic action in a concurrent program … [on its call and return state]. Our method is based on the observation that any behavior … A key property of atomic actions is serializability … [p. 121] We specify a non-atomic procedure by giving … [p. 122] we present the formal specification without much … [Thread] interface itself.   Google-1   Google-2

Copyright clearance needed for quotation.

Additional Titles

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

Related Topics

Topic: proving concurrent programs (37 items)
Topic: path expression (14 items)