About JPF and the project
The Java Pathfinder Team is an open-source organization which maintains and contributes to the project named Java Pathfinder (JPF) which was initially implemented by NASA in 1999 to verify safety and mission-critical software for its space missions. JPF was made open source in 2005, and since then it has seen vast applications in many industries.
JPF is a model checking software, which uses a brute force technique to find any errors in a given piece of java code. To perform this, JPF uses symbolic execution and finds errors by finding out property violations while executing all the different execution paths possible. This is quite a slow process, and the purpose of this project is to parallelize the execution to make the error detection faster by making use of multicore processors.
This project is done under the Google Summer of Code program which is a three-month-long program conducted by Google every year, where students all around the world get the opportunity to work on open source projects under the supervision of experienced mentors
Goals and division of the project
In order to parallelize JPF, the following things have to be done
- The work has to be divided
- The divided work has to be run on different version of JPF running parallely
- It has to be ensured that the splitting and simultaneous execution works perfectly and covers all the choices in the process.
Each of these steps present uniques challenges and working on the proof of concept involves working on those challenges by implementing primitive solutions. The following sections explain each part.
Work division
In order to divide the work, the state space is shrunk in a coordinated fashion such that different parts are handled at different places. Currently, the range of choices that are to be made with respect to the first choice generator is reduced to half (either the first half of the second half).
Such changes takes place in the VM.java class and are performed in the concurrentForward() and concurrentForwardWithSystemStateClone() funtions.
Note: Currently, this function works only with the Verify.verifyInt() API and splits the first choice to divide work.
Running multiple versions of JPF
This is one of the most challenging problems faced because when two versions of JPF are run as two separate processes (on two different terminals or IDEs) , it shows the desirable result and a speedup of nearly 2x (when two versions are run simultaneously) showing that the hardware is capable of supporting the parallelization with a near perfect speedup, but when multiple versions of JPF are run as a part of two different threads, it runs into many unresolved concurrency errors which makes either one or both versions of JPF to stop working due to unexpected errors.
Recording and verifying choices made
In order to verify whether all expected choices are being covered by JPF execution, a choice recorder and a choice listener have been implemented. It records a pair of choice say m and n to ensure all combinations of m and n that are expected to execute are actually executed.
Changes made
- Implemented VerifyChoiceTest.java to check the default order of the choices made
- Implemented FirstChoiceTracker.java - a listener used to intercept the first choice
- Implemented the first choice interception and state space reduction in VM.java by reducing the choice range for the first choice made
- Implemented Choice Generator cloning in FirstChoiceTracker.java
- Implemented ConcurrentDFSearch.java which is derived from DFSearch.java
- Implemented SystemState cloning (partial hard copy + partial shallow copy)
- Resolved backtrack error when replacing SystemState instance in VM with a cloned and modified copy
- Implemented ChoiceCounter and ChoiceListener to listen to a pair of integer choices made and compare them with expected choices when the search completes
- Implemented sequential choice split in JPF by partially reducing (in a coordinated fashion) the state space in two different JPF instances run one after another.
- Implemented parallel version of JPF by running two JPF instances simultaneously on two different threads (isn’t functional presently due to concurrency issues)
The change made in the code are made in a fork of jpf-core and changes are made on the branch parallel-search, choice-counter and concurrent-jpf-run which can be seen in the following urls
https://github.com/javapathfinder/jpf-core/compare/master...manish3499:parallel-search
https://github.com/javapathfinder/jpf-core/compare/master...manish3499:choice-counter
https://github.com/javapathfinder/jpf-core/compare/master...manish3499:concurrent-jpf-run
Using JPF with sequential choice split
To use JPF with sequential choice splitting (branch parallel-search), add the following line to the JPF configuration file.
search.class = .search.ConcurrentDFSearch
Note: Currently it works only with the Verify.getInt() API
Recording and verifying a pair of choices
The class ChoiceCounter.java and the ChoiceListener.java are used for this purpose.
The ChoiceCounter.addActualChoicePair(m,n) function is used to input all pairs of choices expected to be recorded.
The ChoiceCounter.recordChoicePair(m,n) function is used to record a pair of choices.
The ChoiceListener.java listener is used to verify whether the recorded choices and the expected choices are the same. This is done when the search gets completed.
Future work
The following are some of the tasks that need to be worked upon in the future
- Resolving concurrency bugs when two JPF instances are run simultaneously in two separate threads (concurrent-jpf-run branch)
- Extend JPF choice splitting and sequential execution to non-integer cases.