PhD Final Oral Defense: Katherine Coons, November 16, 2012, 1 p.m. CST, ACES 5.336

Contact Name: 
Lydia Griffith
Nov 16, 2012 1:00pm - 3:00pm

PhD Final Oral Defense: Katherine Elizabeth Coons

Date: November 16, 2012
Time: 1 p.m. CST
Place: ACES 5.336
Research Supervisor: Kathryn S. McKinley

Title: Fast Error Detection with Coverage Guarantees for Concurrent Software

Concurrency errors are notoriously difficult to debug because they often occur only under unexpected thread interleavings that are difficult to identify and reproduce. These errors are increasingly important as recent hardware trends compel developers to write more concurrent software. To alleviate this problem, dynamic testing tools should find bugs quickly and reproducibly, and should guarantee coverage. Prior approaches find bugs quickly, or guarantee coverage, but not both.

To find bugs quickly and guarantee coverage, we modify a dynamic, stateless model checker for concurrent software to combine two approaches previously thought to be impractical to combine. We combine bounded search, which explores only thread interleavings that do not exceed a bound, with dynamic partial-order reduction, which explores only one interleaving of independent transitions. First, we prioritize the state space with best-first search and show that heuristics that combine intuitions from these approaches find bugs quickly. Second, we restrict partial-order reduction to combine these approaches while maintaining bounded coverage.

Several properties of bound functions emerge that permit or inhibit partial-order reduction. By bounding the partial order on a program’s transitions, rather than the total order on those transitions, we combine these approaches without sacrificing partial-order reduction. We apply this technique to preemption-bounded search. This bounded, dynamic partial-order reduction algorithm finds bugs quickly and reproducibly with small bounded values, and incrementally guarantees coverage as the bound increases. This thesis extensively analyzes the space of dynamic, bounded partial-order reduction strategies and makes bounded, stateless model checking for concurrent programs significantly more efficient and more practical.