Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts

We describe an algorithm to perform symbolic execution of a multithreaded program starting from an arbitrary program context. We argue that this can enable more efficient symbolic exploration of deep code paths in multithreaded programs by allowing the symbolic engine to jump directly to program contexts of interest. The key challenge is modeling the initial context with reason-able precision—an overly approximate model leads to exploration of many infeasible paths during symbolic execution, while a very precise model would be so expensive to compute that computing it would defeat the purpose of jumping directly to the initial context in the first place. We propose a context-specific dataflow analysis that approximates the initial context cheaply, but precisely enough to avoid some common causes of infeasible-path explosion. This model is necessarily approximate—it may leave portions of the memory state unconstrained, leaving our symbolic execution un-able to answer simple questions such as “which thread holds lock A? ” or “which object does pointer X refer to? ” in all cases. For these cases, we describe novel algorithms for evaluating symbolic pointers and symbolic synchronization during symbolic execution. Our symbolic execution semantics are sound and complete up to the limits of the underlying SMT solver. We describe initial exper-iments on an implementation in Cloud9. 1