Cleaning up: checking source code for (potential) bugs.

Cleaning up: checking source code for (potential) bugs.

Adding untested summary code in DPORStateReducerWithSummary.java.

Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was only called once.

Moving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always executed after updateBacktrackSet following Algorithm 2.

Cleaning up DPORStateReducer.java

Adding untested summary code in DPORStateReducerWithSummary.java.

Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was only called once.

Moving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always executed after updateBacktrackSet following Algorithm 2.

Cleaning up DPORStateReducer.java

Refresh the cached conflict transitions when performing backward DFS due to revisiting the same state.

Removing dead/commented code.

Fixing a bug: summary of conflict transitions is to be paired up with a transition that stems from a state ID.

Fixing a bug: should use equals() to compare the values of Integer objects.

Fixing bug: 1) pushed transition should have been the predecessor transition after a conflict is found, 2) execution should return immediately upon revisiting a transition during backtrack recursion.

Fixing a bug: summary of conflict transition and ReadWriteSet need to be stored in TransitionEvent; then summary of reachable transitions at a state can be stored in the RGraph object.

Minor changes to input arguments of some methods/functions.

Adding checks to ensure that a predecessor is only recorded once for a transition.

Testing the implementation; fixing a bug.

Small edits in method updateBacktrackSetsFromPreviousExecution.

Cleaning up the code; still need to test everything.

Making the implementation of updateBacktrackSetDFS closer to the paper in DPORStateReducer.java.

Initial implementation of more efficient traversal with graph summary; pretty much untested and un-double-checked yet.

Adding a new file for a more efficient implementation; the implementation for updateBacktrackSetDFS is made closer to the paper.

Adding missing 'add' into HashSet.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Changing StringBuilder into HashMap and HashSet.

Generate a new RestorableVMState object only when it's still not available in the HashMap.

Adding notes in the latest changes for the serializer bug fix.

More filtering: never define a method call 'call' since Groovy generates a lot of those.

Integrating bug fix for CFSerializer.

Fixing a bug: in the second round of boolean CG, we might encounter states in the first round that are considered new states; adding a guard condition for a map read.

Adding debug mode guards for all main methods.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Adding a way for JPF to be informed that this is DPOR; otherwise number the hacked number CGs only work for DPOR and it creates an infinite loop for a normal execution without DPOR.

Commenting out a line that causes a lot of loops; let the exclusion trace continue to build up.

Bug fix: when state is not found in rGraph, that means the state is being visited and this is a loop (self-predecessor).

A few hacks to make the list circular: this lets the CG not signal the JPF that the end of the list is the end of the CG execution.

Explored trace needs to be constructed and modified as there are predecessor branches.

Renaming a variable.

Fixing a bug in isConflict method.

Making field exclusion checks more efficient.

Committing main.jpf.

Further cleaning up (naming, comments, etc.).

Adding happens-before push back.

Cleaning up.

New algorithm implementation; without pushing forward hb transaction; untested/undebugged yet.

Adding different main.jpf files for different detections.

Editing main.jpf

Adding a script to set the environment variables for groovyc.

Fixing a bug: need to get the right choice/event number for IntIntervalGenerator CGs.

Tested updating backtrack sets in the reachability graph.

Tested backtrack in a cycle (local).

Adjusting support methods for reachability analysis with the new algorithm; untested yet.

Modifying the algorithm: 1) Find the first conflict and stop; 2) Perform backward DFS to find conflicts in the execution graph.

Fixing a bug: completing reachability graph with missing past traces.

Fixing bugs: state to reachability graph map has to be updated for every new state in the stateAdvanced method.

Adding reachability graph for past executions.

Additional logging feature.

Fixing a bug: mapping state to event has to be done after the execution termination check, otherwise we stop too early.

Fixing more bugs with the reachability analysis.

Fixing more potential bugs for the reachability analysis.

Fixing a bug: separating the state tracking for cycle analysis.

Adding reachability analysis when state matching occurs.

Modifying main.jpf

Adding a counter for number of conflicts.

Printing out the number of transitions.

Fixing a bug: misunderstood how the VOD graph is supposed to be generated; we basically track the transitions that produce new states.

Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the conflicts.

Fixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove a node from the queue.

Fixing a bug: VOD graph traversal should continue with the next neighbor when there is a loop (repeated node found).

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing a bug: restorable state has to be saved when backtrack point info is saved to get the appropriate CG type when restoring.

Optimization: Compare just the state and the fist event/choice of the trace to not repeat the same backtrack trace twice (the two will map to the same state and the algorithm will stop the second execution, so there is no need to record and explore it twice, e.g., the traces 2 0 1 3 and 2 1 0 3 at state 3.

Changing approach: Using vm.restoreState() method to restore JPF to the desired state when backtracking; everything looks correct but probably needs more tests.

Committing a version that almost works: bug to fix is that when an execution finishes and the first backtrack point requires to get back to a higher state, there is no mechanism to roll back to that state.

First part of boolean flip seems to be clean; need to debug the second part and figure out what to do when the current state is lower than the highest state ID for backtrack.

Fixing a potential bug: we now store the event number in the ArrayList together with the list of CGs for backtracking; getting the event number directly from the current array might be misleading because the array choices might have been modified for fair-scheduling.

Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to test with other pairs.

Fixing a bug: we need to start choiceCounter from 1 instead of 0 for subsequent executions since the first CG (number 0) is the backtrack CG itself.

Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points); need to test how CGs are explored with the current DFSearch.

Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and conflict analysis; cleaning up and refactoring.

Reimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access analysis.

Starting a new DPOR implementation.

Cleaning up and refactoring.

Fixing bugs: capturing object accesses (read/write) in iterators.

Fixing a bug: off-by-one error in the executed trace checking.

Re-checking and cleaning up the code: most likely still have a bug in re-ordering the two apps.

Adding the old tracker variable for debugging/testing purposes.

Fixing bugs and cleaning up: Continuing sub-graph executions when there is no matched states or cycles that contain all events; checking in the old ConflictTracker for testing.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing bugs and cleaning up: making sure that the execution of the first trace has fair-scheduling with appropriate state-matching.

Making analysis compatible with infra

Making analysis compatible with new infrastructure

Cleaning up: Removing the full-blown graph traversal.

Cleaning up, fixing bugs---commented out full-blown graph traversal code.

Refactoring; Finding cycles without traversing the entire state graph.

Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most up-to-date values.

Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

Some fixes for the DPOR state-reducer.