A Framework for Runtime Verification of Concurrent Programs

This talk is about the VYRD project, a verification framework for concurrent programs that combines ideas from model checking and testing. In Norse mythology, the three Vyrd sisters weave together the threads of fate.

In the first part of the talk, we present our work on runtime refinement checking. We describe two novel correctness criteria for concurrent software, a tool we built for detecting violations of these criteria at run-time, and the successful results we obtained using our tool on industrial-scale programs, including the Boxwood project from MSR SVC. Our tool has low overhead, provides significant improvement over testing, and was able to detect previously uncaught errors on industrial-scale programs.

We then present an improvement to this technique, in which a constrained, inexpensive application of an execution-based model checker drives runtime refinement verification. This hybrid technique is able to get extensive checking from very small test cases by combining the improved coverage provided by a model checker with the improved observability of checking refinement.

Last, we present a novel test coverage metric for concurrent software. This metric corresponds well with concurrency errors we encountered ourselves and found in the literature. The metric is meant as an aid to the programmer in identifying unexercised, error-prone scenarios. We propose techniques for making the metric easy-to-use and computationally practical.