Runtime predictive analysis

In computer science, runtime predictive analysis (or predictive analysis) is a runtime verification technique for detecting property violations in program executions that can be inferred from an observed execution. An important class of predictive analysis methods has been developed for detecting concurrency errors (such as data races) in concurrent programs, where a runtime monitor is used to predict errors which did not happen in the observed run, but can happen in an alternative execution of the same program. The predictive capability comes from the fact that the analysis is performed on an abstract model extracted online from the observed execution, which admits a class of executions including the observed one.^[1]

Overview

Predictive analysis has been applied to detect a wide class of concurrency errors, including:

data races
deadlocks
atomicity violations
order violations, e.g., use-after-free errors

Implementation

Predictive analysis is typically implemented by first instrumenting the source program. At runtime, the analysis can be performed online and detects errors on the fly. Alternatively, the online monitor can dump the execution trace for offline analysis.

Techniques

Partial order based techniques

Partial order based techniques are most often employed for race detection. At runtime, a partial order over the events in the trace is constructed, and any unordered pairs of events are reported as races. Many predictive techniques for race detection are based on the happens-before relation or a weakened version of it. Such techniques can typically be implemented efficiently with vector clock algorithms, allowing only one pass of the whole input trace, and is thus suitable for online deployment.^{[citation needed]}

SMT-based techniques

SMT encodings allow the analysis to extract a refined causal model from an execution trace. Furthermore, control-flow information can be incorporated into the model. SMT-based techniques can achieve soundness and completeness (also called maximality), but has exponential-time complexity with respect to the trace size. In practice, the analysis is typically deployed to bounded segments of an execution trace, thus trading completeness for scalability.^{[citation needed]}

Other techniques

In the context of data race detection, sound and highly complete polynomial-time predictive analysis has been developed.^{[citation needed]}

Tools

RV-predict: SMT-based predictive race detection.
Rapid: a lightweight framework for implementing dynamic race detection engines.
RoadRunner.
UFO: SMT-based predictive use-after-free detection.

References

^ "Runtime Predictive Analysis". November, 2008. {{cite web}}: Check date values in: |date= (help)

[1] "Runtime Predictive Analysis". November, 2008. {{cite web}}: Check date values in: |date= (help)

[1]