Predictive trace analysis (PTA) detects concurrency faults not recorded in the observed execution order of a nondeterminate concurrent program by producing and analyzing other feasible execution orders of events of the same program from the recorded trace using causal relationships. Existing PTA techniques mostly predict low-level conventional concurrency faults like memory anomalies, data races, and so on using global execution traces. This paper proposes GPredict, which implements PTA in multithreaded Java programs, for predicting various high-level generic concurrency property violations like unsafe iterator traversal along with conventional concurrency faults. GPredict uses only thread-local traces, leading to significant performance improvement over existing techniques.

GPredict provides a property specification language, extended from monitoring-oriented programming (MOP) [1], to declare property parameters, property event sets (using AspectJ pointcuts), thread attributes, and so on, and to define a property (like “a collectioncannot be modified when being iterated over”) using regular expressions over the declared events and attributes. Property violations are modeled by defining first-order logical constraints over the events. For obtaining other feasible execution sequences of the same program from observed thread-local traces, the authors define a causal model (extending global traces [2]) by modeling first-order logical constraints on critical events (named model events) that determine the causal order like shared data read/writes, thread synchronizations, and so on. GPredict uses the Z3 satisfiable modulo theory (SMT) solver [3] to solve the conjunction of all the constraints and detect “property violations in all the feasible executions captured by the causal model.”

For implementation, “taking the target program (Java bytecode) and the property specification as input, GPredict first adds necessary instrumentation into the program for logging the model events during execution, and uses JavaMOP’s front-end parser to produce a corresponding AspectJ file for the property.” The AspectJ file is weaved into the instrumented bytecode during program execution to emit a trace, upon which GPredict uses an offline analyzer to build required constraints and a SMT solver to detect violations.

The paper is well presented. It will be helpful to developers of multithreaded programs in Java who have prior knowledge of SMT problems, AspectJ, and JavaMOP.