Parametric and Sliced Causality

From FSL

[edit] CAV'07

Parametric and Sliced Causality

Feng Chen and Grigore Rosu

CAV'07, LNCS 4590, pp 240 - 253, 2007

Abstract. Happen-before causal partial order relations have been widely used in concurrent program verification and testing. In this paper, we present a parametric approach to happen-before causal partial orders. All existing variants of happen-before relations can be obtained as instances of the parametric framework for particular properties on the partial orders. A novel causal partial order, called sliced causality, is defined also as an instance of the parametric framework, which loosens the obvious but strict happens-before relation by considering static and dynamic dependence information about the program. Sliced causality has been implemented in a concurrent runtime verification tool for Java, named jPredictor, and the evaluation results show that sliced causality can significantly improve the capability of concurrent verification and testing on multi-threaded Java programs.

PDF, CAV'07 slides, CAV'07, TR@UIUC, BIB