Notes: Parallel Proofs for Parallel Programs
Languages and concurrent programs
Zac Kinkaid -- U. Toronto
Notes legibility estimate: LOW
Automatic analysis of algorithms
We'd like to know things like "What numeric types are used here? Are these array accesses in-bounds?"
Today: Proving the absence of faults in multi-threaded programs.
Multi-threaded programs are a great target for automated analysis, since they're so notoriously difficult for humans to reason about.
- Floyd -- program invariants
- Ashcroft, Manna -- extended Floyd to multithreaded programs by treating a multiprogram as a nondeterministic single-threaded program -- difficulty: doesn't scale in #threads
- ??, Reese -- (for data-independent threads) Prove each thread correct individually; then check that the reasoning doesn't interfere across threads -- difficulty extending to data-dependent threads, which requires some cleverness, which is difficult to automate
in common: attempts to reason about multi-threaded code using (extensions of) sequential reasoning
The big problem
Given (program, property), does property(program) hold?
Turing: Halting indeterminacy
Rice's Theorem: Every nontrivial property is undecideable
Allow either one-sided error or indeterminacy/divergence
x = 2; y