RV Predict Demo
What RV PREDICT does
RV Predict aids the programmer in dynamically detecting concurrency errors in multithreaded Java programs. RV Predict is entirely automatic and generates no false positives/alarms.
After using RV Predict, please take a moment fill out the following survey
Context
Current architecture trends have made concurrent programming a necessity. Concurrency errors are often very subtle and are hard to detect during testing because of their non-deterministic nature. Thus, many programs have concurrency errors even if they appear to execute correctly before deployment. Unfortunately, such errors may unexpectedly manifest in deployed systems and can be catastrophic.
How RV Predict works
1. Go to File/Open and select a Java binary file (.class file). The selected binary must be executable, that is, it must contain a Main method. RV predict will automatically calculate the root directory and the main class file and display them in its output window.
2. Go to Settings and set the execution parameters of your program. The classpath is initially copied from the system's CLASSPATH variable, but it can be changed. Also, give the program arguments and the desired heap size. To check whether the program executes, click on the "check" button in the main window. If everything goes well, the output of the original program should be displayed in the bottom text area. Making sure that the original program executes is a hard prerequisite for RV Predict: no prediction can be done unless the program can be executed using the "check" button. You may want to give the program a larger heap than needed, because the instrumentation (see next) will also take some heap space at runtime.
3. Click on "predict" (PLEASE, do this only after you are certain that the program runs when clicking "check"---see above). A series of operations will be performed automatically: first, a copy of the program (to avoid changing the original) will be instrumented in a temporary directory (this may take awhile); second, the instrumented program will be executed and its execution trace will be collected (this step is expected to be, on average, up to 3 times slower than running the original program); third the collected execution trace will be analyzed for concurrency errors. The RV Predict output will be listed in the top text area, while the program output will be listed in the bottom text area.
The underlying technology
RV Predict is based on technologies invented at the University of Illinois at Urbana-Chamapaign and first implemented in the academic runtime verification system jPredictor in 2008 (see the jPredictor paper in ICSE'08).
RV Predict significantly improves (by orders of magnitude) both the error-detection capabilities and the performance of jPredictor. The idea underlying RV Predict is to execute the program under test and observe how certain events (e.g., reads and writes of shared objects, acquires and releases of synchronization objects, etc.) causally depend upon each other during the execution of the program. An error is reported whenever RV Predict cannot find enough combined evidence in the program code (extracted statically) and in the causal dependence (extracted dynamically) to justify the observed behavior. The observed execution may directly encounter no errors, yet the reported errors can happen in other executions of the same program. This gives the user the feel that the tool "predicts" errors from correct program executions.
Limitations
To obtain the maximum benefit from using RV Predict, one should understand its limitations: both the limitations of its underlying technology and the limitations of our current beta implementation. Like any dynamic tool, RV predict cannot detect errors in code that has not been executed during the observed run. Therefore, one should not assume that a program has no concurrency errors when RV Predict reports no errors. One may use RV Predict in combination with test-case generation techniques and tools to increase coverage. The only guarantee that RV Predict gives is that any reported error is a real concurrency error.
This version of RV Predict only provides support for datarace prediction and only reports the line numbers where the racing events were generated. The instrumentation phase can be slow. Several static analyses of the program to test are performed during instrumentation in order to minimize the number of observed events and the information they need to carry, so that the runtime overhead of the instrumented program is low and the predictive capability of the prediction phase is high. For small programs, the instrumentation phase can be the slowest phase.
NB1: RV Predict instruments Java binaries (.class files), so the source code (.java) of the program under test is not needed. Moreover, RV Predict will create its own temporary copy of the instrumented binary, so one should not fear that one's binaries are destroyed.
NB2: The instrumented program should not be much slower than the original. In general, it should be less than two or three times slower. However, there are pathological examples where a large number of shared objects are created and where almost every operation in the program under test is a read or write of a shared object. In such cases, the instrumented program can be significantly slower than the original. The prediction phase can also be slow, especially when there are many shared objects.
NB3: Each shared object is checked for races independently from the others, and a message is output to the user each time a new shared object is checked (so the user can monitor its progress). To observe means to interact. Thus, it can be possible that one sees a different behavior of the same program after instrumentation; nevertheless, any observed behavior is feasible, so any reported errors are valid. Sometimes it may even be the case that an error manifests by just running the instrumented program; prediction does not do much in that case, but an error has been detected, nevertheless. Other times the program under test deadlocks; that deadlock is not an artifact of RV Predict, it is a real deadlock in the original program (these are some of the most subtle and hard to detect concurrency errors).
This is a beta product, offered free of charge for evaluation purposes. While we did our best to test it extensively, it likely still has bugs. Please help us improve RV predict by reporting any bugs to predict@runtimeverification.com. Suggestions for improvement are also welcome.