Topic: proving concurrent programs

topics > computer science > programming > Group: program proving

parallel processing
requirement specification

automated tests of specifications and designs
formal methods and languages
hard real time systems
Petri net transitions and events
calculus of communicating processes
critical regions
interprocess communication
just-in-time compilation
model checker
real time systems
reliability of distributed systems
requirement specification by behaviors
safety, liveness, and system properties
specification and design of distributed systems
state machine


When proving concurrent systems, you need to prove that each component meets its specification and that the system meets safety assertions and progress assertions and avoids deadlocks and starvation. Concurrent systems are harder to prove and specify than sequential systems. One needs assertions that hold over all possible event and action sequences.

Birrel et al use a formal specification for Modula-3's thread interface. They found that informal specifications were incomplete, especially on multiprocessor systems. While difficult to write, the specifications have proved useful to users and implementers of the thread interface.

Occam includes a formal semantics. Simple constructs, autonomous processes, and data driven programs simplify concurrency arguments. (cbb 4/98)

Subtopic: safety, progress, liveness up

Quote: reason about concurrent systems using safety (nothing bad can happen) and progress (something good will happen) assertions [»shanAU9_1993]
Quote: prove that each component behaves correctly in isolation when its environment is correct; then proof rule for composition under safety and liveness conditions [»abadM1_1993]
Quote: for concurrent programming, prove that bad things can't happen and good things do; i.e., an expression of the program's variables; avoids process interleavings [»schnFB4_1998]
Quote: type systems say nothing about concurrency or dynamics; e.g., that initialize happens first, or x() must be invoked every 10 ms [»leeEA9_2000]
Quote: desired properties for state machines--absence of deadlock, completeness, and liveness; catch basic flaws and unwarranted assumptions [»holzGJ5_1999]
Quote: liveness is much harder to prove than safety, yet it is just as important; must prove that g() terminates to prove that h() occurs in f;g;h [»cookB1_2007]

Subtopic: parallelism up

Quote: algorithm for mutual exclusion of readers and writers; minimize delay of readers or writers; based on P, V, and active counts [»courPJ10_1971]

Subtopic: invariants up

Quote: for reasoning about concurrent programs, replace weakest precondition and strongest postcondition with weakest and strongest invariants [»lampL7_1990]
Quote: use invariants for safety properties, and leads-to and invariants for progress properties; includes every property for state-event sequences [»shanAU9_1993]
Quote: extend Hoare's assertions to concurrent programs by pre-conditions holding until termination of unit; equivalent for atomic actions [»lampL_1980]
Quote: model a concurrent system by state transitions and fairness requirements; use invariant and leads-to assertions and Hoare logic [»shanAU9_1993]

Subtopic: interruptible up

Quote: when does a property hold whether or not a statement is interruptible? [»liptRJ12_1975]
Quote: a right mover is a "release" [V] that can move later in an interleaving; a left mover is a "seize" [P] that can move earlier [»liptRJ12_1975]
Quote: for proofs, can treat a sequence as atomic if it consists of right movers (V) followed by left movers (P) [»liptRJ12_1975]

Subtopic: schedule-time validation up

Quote: validate Eventrons at run-time before scheduling; no allocation or pointer modification; creates a data-specific call graph [»spooD6_2006]

Subtopic: formal specification up

Quote: occam has a formal semantics; used an interactive transformation system to prove that an occam program satisfied the IEEE floating point standard [»mayD_1987]
Quote: use a formal specification for synchronization primitives on a multiprocessor; otherwise difficult questions about their precise semantics [»birrAD_1991a]
Quote: formal specification of Modula-3 threads for safety properties and termination; ignores liveness [»birrAD_1991a]
Quote: programmers and implementers use the formal specification of Modula-3 threads [»birrAD_1991a]
Quote: an untrained user found an error in the formal specification of Modula-3 threads; another error was missed for a year
Quote: Sing# has formal message passing semantics; all processes run in one virtual address space without overwriting data; avoids kernel traps and context switches [»taneAS5_2006]
Quote: Sing# sends strongly typed messages over bidirectional channels; a state machine defines the channel's protocol [»taneAS5_2006]

Subtopic: proving concurrent programs up

Quote: the dining philosophers problem demonstrates the constructive approach to multiprogramming correctness [»dijkEW2_1971]
Quote: introduce the intermediate state, 'hungry', to solve the dining philosophers problem
Quote: used detailed, hierarchical proofs since theorems about concurrent system specifications are difficult to get right [»abadM1_1993]
Quote: a concurrent language needs simple constructs that guarantee determinism; usually not true of message communication systems [»chanKM7_1980]
Quote: verify atomicity using Lipton's right and left movers; lock acquisition moves to the right while lock release moves left; atomic if acquisition and release move to start and end respectively [»flanC6_2003]
Quote: a specification is realizable iff the system has a winning strategy; i.e., the system wins under all legal environment behaviors [»abadM1_1993]
Quote: process autonomy--each component of a distributed program should be designed and proved separately; can not name other processes [»chanKM7_1980]

Subtopic: search for deadlocks and assertion violations up

Quote: efficient search technique for detecting deadlocks and assertion violations in concurrent programs [»godeP1_1997]

Subtopic: temporal logic up

Quote: transition-axiom method for proving concurrent systems combines abstract programs and temporal logic; rules for implementation and composition [»abadM1_1993]

Subtopic: atomic operations up

Quote: specify atomic operations for concurrent programs by angle brackets, e.g., ' := ' [»lampL_1980]

Subtopic: intermediate results up

Quote: in proofs of concurrent programs need to introduce value variables for intermediate results [»lampL_1980]

Subtopic: path expression up

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

Subtopic: data flow up

Quote: data-driven programs simplify correctness proofs, use data streams instead of elements; queuing-network analysis, and microcomputer networks [»dennPJ_1980]

Subtopic: problems with proving up

Quote: threaded programs are extremely difficult to prove equivalent; due to the enormous number of possible interleavings [»leeEA5_2006]
Quote: sequential execution is function composition; a neat, simple model with deterministic results

Related Topics up

Group: parallel processing   (41 topics, 1125 quotes)
Group: requirement specification   (11 topics, 307 quotes)

Topic: automated tests of specifications and designs (12 items)
Topic: concurrency (33 items)
Topic: deadlocks (21 items)
Topic: formal methods and languages (53 items)
Topic: hard real time systems (64 items)
Topic: Petri net transitions and events (21 items)
Topic: calculus of communicating processes (13 items)
Topic: critical regions (58 items)
Topic: interprocess communication (29 items)
Topic: just-in-time compilation (20 items)
Topic: model checker (49 items)
Topic: real time systems (14 items)
Topic: reliability of distributed systems (35 items)
Topic: requirement specification by behaviors (16 items)
Topic: safety, liveness, and system properties (22 items)
Topic: specification and design of distributed systems (14 items)
Topic: state machine
(67 items)

Updated barberCB 12/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.