Parametric and Sliced Causality

From FSL
Jump to: navigation, search


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

Personal tools