RV Inc. to Give Tutorial at Runtime Verification ’16 Conference

Runtime Verification Inc. is going to be presenting an exciting tutorial at the RV’16 conference, featuring all of our current tools and technologies and their practical and creative uses and applications.

If you are new (or a veteran) to runtime verification technology, we invite you to join and learn about what RV Inc.’s tools can do for your codebase, today. We look forward to seeing you in sunny, beautiful Madrid!

2016-05-25--1464206820_1518x728_scrot

Testing K Framework using RV-Predict

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.
Continue reading

Detecting popular data races in Java using RV-Predict

Data races are a common kind of concurrency bug in multithreaded applications. A data race can be defined as two threads accessing a shared memory location concurrently and at least one of the accesses is a write. Data races are notoriously difficult to find and reproduce because they often happen under very specific circumstances. Therefore, you could have a successful pass of the tests most of the time but some test fails once in a while with some mysterious error message far from the root cause of the data race.

Despite all the effort on solving this problem, it remains a challenge in practice to detect data races effectively and efficiently. RV-Predict aims to change this undesired situation. In this blog post, we will summarize some of the most popular kinds of data races in Java and show you how to catch them using RV-Predict. The examples in this post are included in the RV-Predict distribution under the examples/ directory.

Continue reading

Using RV-Predict to track down race conditions

We’ve all had it happen: you write some multithreaded code, but when you run it, it crashes with some kind of error every second or third or hundredth run. The traditional way of trying to debug this problem is very tedious and involves attempting to reproduce the error (difficult) and then tracing the inconsistent state backwards to find the source of the race condition (even more difficult).

Enter RV-Predict. Today I was developing code for RV-Match when I ran into an intermittently occurring NullPointerException in its parser. Instead of trying to reproduce the bug and tracking its behavior backwards, I assumed going in that it was caused by a race condition, and ran RV-Predict on the program. After it crashed, it spat out the following error report: Continue reading

“restrict” keyword in header files

It would appear that Mac OS X’s copy of string.h is invalid.

It declares strcpy as

char *strcpy(char *, const char *);

But the C standard declares it as

char *strcpy(char * restrict, const char * restrict);

These two types are actually incompatible with each other according to the C standard, and a function that is declared  more than once in different translation units with different declarations is considered undefined behavior. Thus, any correctly conforming C library will cause any code that includes string.h to be undefined.

Oops!

Undefined C: Common mistakes

This blog post is the beginning of an intended series of blog posts detailing undefined and unspecified behavior in the ISO C standard, and its impact on development. To start with, we will summarize the domain and provide information about some of the undefined behaviors which we have found to be most widespread in production-deployed C code of the open source projects we have tested.

Continue reading