Multithreaded programs are difficult to get right.  The interaction of concurrently executing threads leads to a huge number of program behaviors.  Programmers, unable to account for all possible interactions among threads, often make errors which are difficult to find by traditional testing methods.  In this lecture, I will present CHESS, a software model checker for systematically enumerating such behaviors.

CHESS implements iterative context-bounding, a new approach for effectively searching the state space of a multithreaded program.  In an execution of a multithreaded program, a context switch occurs when a thread temporarily stops execution and a different thread starts.  Iterative context-bounding gives priority to executions with fewer context switches, exploring all executions with no context switches followed by all executions with one context switch and so on.

For a fixed number of context switches, the total number of executions in a program is polynomial in the number of steps taken by each thread.  This theoretical upper bound makes it practically feasible to scale systematic exploration to large programs without sacrificing the ability to go deep in the state space.  Our experience applying CHESS to large real-world programs shows that systematic search with a small number of context switches has the ability to expose nontrivial concurrency bugs.  CHESS has uncovered 9 previously unknown bugs in our benchmarks, each exposed by an execution with at most 2 context switches.

Monday, July 30, 2007

10:00 am - 11:00 am

3330 Walnut Street,

Room 315 Levine Hall