Deterministic Replay for MCAPI Applications

Jan 2011 – June 2011

Similar to parallel programs in other domains, debugging MCAPI programs is a challenging task due to their high degree of concurrent execution and non-deterministic behavior. In this project we are developing a tool that is able to deterministically replay the executions of MCAPI programs, which provides valuable insight for MCAPI developers in case of failure.

Debugging Support for Message-Passing Software via SMT-Based Predictive Analysis

Sept 2008 – June 2011

The goal of this project is to support debugging message-passing software by predicting the possibility of reaching an error state during run-time. To achieve this goal we propose applying a novel predictive analysis technique in which a program model and a set of safety properties are encoded as a quantifier-free first-order logic formula. The satisfiability of this formula can be decided using any of the available off-the-shelf SMT solvers. If the formula is satisfiable, then we can infer that there exists an execution scenario (i.e. a specific interleaving) in which at least one safety property is violated. The solution produced by the SMT solver provides enough information to construct the execution scenario that violates the safety property.