SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Thu 23 Oct 2014 14:37 - 15:00 at Salon F - Concurrency Chair(s): David Grove

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 reasonable 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 \emph{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 unable to answer simple questions such as ``which thread holds lock A?''. For such cases, we describe a novel algorithm for evaluating \emph{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 experiments on an implementation in Cloud9.

Thu 23 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
ConcurrencyOOPSLA at Salon F
Chair(s): David Grove IBM Research
13:30
22m
Talk
Atlas: Leveraging Locks for Non-volatile Memory Consistency
OOPSLA
Dhruva Chakrabarti HP Labs, Hans-J. Boehm Google, Kumud Bhandari Rice University
Link to publication
13:52
22m
Talk
Fast Splittable Pseudorandom Number Generators
OOPSLA
Guy L. Steele Jr. Oracle Labs, Doug Lea State University of New York (SUNY) Oswego, Christine H. Flood Red Hat
Link to publication
14:15
22m
Talk
Multithreaded Test Synthesis for Deadlock Detection
OOPSLA
Malavika Samak Indian Institute of Science, Bangalore, Murali Krishna Ramanathan Indian Institute of Science, Bangalore
Link to publication
14:37
22m
Talk
Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts
OOPSLA
Tom Bergan University of Washington, Dan Grossman University of Washington, Luis Ceze University of Washington
Link to publication