This blog post is the beginning of a series of blog posts recording our experience of hunting data races in complex real-world applications using RV-Predict. To start with, we will choose the K framework as our first test subject.
Why the K framework? Well, there are a number of reasons. First of all, it’s a very cool project! Check out its website for a quick introduction. It is also the foundation of our RV-Match product, which aims to provide strong correctness guarantees through formal verification. Therefore, it’s very important that the underlying K Framework is free from bugs including data races. Finally, the K framework is complex. It is written in a combination of Java and Scala and makes use of the Java 8 features extensively. It also takes advantage of many 3rd-party libraries such as Guice, Guava, Nailgun, etc. As a practical race detector, RV-Predict must be able to handle all these aspects gracefully.