jpf-core.git
19 months agoFixing a few bugs in the statistics printout. master
rtrimana [Tue, 20 Apr 2021 16:16:33 +0000 (09:16 -0700)]
Fixing a few bugs in the statistics printout.

22 months agoAnother fix for the counter for unique transitions.
rtrimana [Fri, 29 Jan 2021 05:12:51 +0000 (21:12 -0800)]
Another fix for the counter for unique transitions.

22 months agoAnother fix for the counter for unique transitions.
rtrimana [Fri, 29 Jan 2021 05:05:57 +0000 (21:05 -0800)]
Another fix for the counter for unique transitions.

22 months agoFixing the counter for unique transitions.
rtrimana [Thu, 28 Jan 2021 23:23:11 +0000 (15:23 -0800)]
Fixing the counter for unique transitions.

22 months agoAdding a counter for unique transitions.
rtrimana [Thu, 28 Jan 2021 21:39:56 +0000 (13:39 -0800)]
Adding a counter for unique transitions.

22 months agoBug fix: need to check for conflicts between events extracted from the state summary...
rtrimana [Fri, 22 Jan 2021 00:06:22 +0000 (16:06 -0800)]
Bug fix: need to check for conflicts between events extracted from the state summary and the current transition in updateBacktrackSetsFromGraph.

22 months agoFixing bug due to refactoring/moving of code in the previous commit to handle apps...
rtrimana [Tue, 19 Jan 2021 18:22:39 +0000 (10:22 -0800)]
Fixing bug due to refactoring/moving of code in the previous commit to handle apps with no events.

22 months agoRefactoring/moving handler in the listener to check if the benchmark has no event...
rtrimana [Tue, 19 Jan 2021 00:21:18 +0000 (16:21 -0800)]
Refactoring/moving handler in the listener to check if the benchmark has no event (in this case we don't do DPOR).

22 months agoAdding a handler in the listener to check if the benchmark has no event (in this...
rtrimana [Tue, 19 Jan 2021 00:09:59 +0000 (16:09 -0800)]
Adding a handler in the listener to check if the benchmark has no event (in this case we don't do DPOR).

22 months agoFixed a typo in the new class.
rtrimana [Thu, 14 Jan 2021 18:31:14 +0000 (10:31 -0800)]
Fixed a typo in the new class.

22 months agoAdding another version of DPOR implementation that considers only the end states...
rtrimana [Thu, 14 Jan 2021 18:18:34 +0000 (10:18 -0800)]
Adding another version of DPOR implementation that considers only the end states of transitions.

22 months agoRecording predecessors per state as opposed to per transition.
rtrimana [Wed, 13 Jan 2021 20:09:43 +0000 (12:09 -0800)]
Recording predecessors per state as opposed to per transition.

22 months agoFixing bugs: the main one is to create a local copy of the set that contains accesses...
rtrimana [Wed, 6 Jan 2021 22:19:32 +0000 (14:19 -0800)]
Fixing bugs: the main one is to create a local copy of the set that contains accesses in updateBacktrackSetDFS().

23 months agoFixing a few bugs, e.g., missing rwSet.copy(), misplaced check for empty rwSet, etc.
rtrimana [Wed, 16 Dec 2020 17:46:48 +0000 (09:46 -0800)]
Fixing a few bugs, e.g., missing rwSet.copy(), misplaced check for empty rwSet, etc.

23 months agoMore cleanups for comments and variable names.
rtrimana [Tue, 15 Dec 2020 17:49:27 +0000 (09:49 -0800)]
More cleanups for comments and variable names.

23 months agoCleaning up: checking source code for (potential) bugs.
rtrimana [Tue, 15 Dec 2020 17:43:59 +0000 (09:43 -0800)]
Cleaning up: checking source code for (potential) bugs.

23 months agoCleaning up: checking source code for (potential) bugs.
rtrimana [Tue, 15 Dec 2020 17:38:17 +0000 (09:38 -0800)]
Cleaning up: checking source code for (potential) bugs.

23 months agoAdding untested summary code in DPORStateReducerWithSummary.java.
rtrimana [Mon, 14 Dec 2020 18:57:06 +0000 (10:57 -0800)]
Adding untested summary code in DPORStateReducerWithSummary.java.

23 months agoFixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was...
rtrimana [Fri, 11 Dec 2020 00:01:36 +0000 (16:01 -0800)]
Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was only called once.

23 months agoMoving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always...
rtrimana [Mon, 7 Dec 2020 18:44:11 +0000 (10:44 -0800)]
Moving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always executed after updateBacktrackSet following Algorithm 2.

23 months agoCleaning up DPORStateReducer.java
rtrimana [Mon, 7 Dec 2020 17:40:08 +0000 (09:40 -0800)]
Cleaning up DPORStateReducer.java

23 months agoAdding untested summary code in DPORStateReducerWithSummary.java.
UCI Networking Group [Mon, 14 Dec 2020 18:57:06 +0000 (10:57 -0800)]
Adding untested summary code in DPORStateReducerWithSummary.java.

23 months agoFixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was...
UCI Networking Group [Fri, 11 Dec 2020 00:01:36 +0000 (16:01 -0800)]
Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was only called once.

23 months agoMoving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always...
UCI Networking Group [Mon, 7 Dec 2020 18:44:11 +0000 (10:44 -0800)]
Moving updateBacktrackSetsFromGraph into choiceGeneratorAdvanced so that it's always executed after updateBacktrackSet following Algorithm 2.

23 months agoCleaning up DPORStateReducer.java
UCI Networking Group [Mon, 7 Dec 2020 17:40:08 +0000 (09:40 -0800)]
Cleaning up DPORStateReducer.java

2 years agoRefresh the cached conflict transitions when performing backward DFS due to revisitin...
rtrimana [Thu, 24 Sep 2020 18:02:47 +0000 (11:02 -0700)]
Refresh the cached conflict transitions when performing backward DFS due to revisiting the same state.

2 years agoRemoving dead/commented code.
rtrimana [Wed, 23 Sep 2020 18:30:02 +0000 (11:30 -0700)]
Removing dead/commented code.

2 years agoFixing a bug: summary of conflict transitions is to be paired up with a transition...
rtrimana [Tue, 22 Sep 2020 22:58:58 +0000 (15:58 -0700)]
Fixing a bug: summary of conflict transitions is to be paired up with a transition that stems from a state ID.

2 years agoFixing a bug: should use equals() to compare the values of Integer objects.
rtrimana [Tue, 22 Sep 2020 18:53:43 +0000 (11:53 -0700)]
Fixing a bug: should use equals() to compare the values of Integer objects.

2 years agoFixing bug: 1) pushed transition should have been the predecessor transition after...
rtrimana [Tue, 22 Sep 2020 18:17:59 +0000 (11:17 -0700)]
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.

2 years agoFixing a bug: summary of conflict transition and ReadWriteSet need to be stored in...
rtrimana [Mon, 21 Sep 2020 22:01:05 +0000 (15:01 -0700)]
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.

2 years agoMinor changes to input arguments of some methods/functions.
rtrimana [Fri, 18 Sep 2020 18:24:47 +0000 (11:24 -0700)]
Minor changes to input arguments of some methods/functions.

2 years agoAdding checks to ensure that a predecessor is only recorded once for a transition.
rtrimana [Thu, 17 Sep 2020 16:46:29 +0000 (09:46 -0700)]
Adding checks to ensure that a predecessor is only recorded once for a transition.

2 years agoTesting the implementation; fixing a bug.
rtrimana [Fri, 11 Sep 2020 18:54:27 +0000 (11:54 -0700)]
Testing the implementation; fixing a bug.

2 years agoSmall edits in method updateBacktrackSetsFromPreviousExecution.
rtrimana [Thu, 10 Sep 2020 19:00:40 +0000 (12:00 -0700)]
Small edits in method updateBacktrackSetsFromPreviousExecution.

2 years agoCleaning up the code; still need to test everything.
rtrimana [Wed, 9 Sep 2020 19:00:04 +0000 (12:00 -0700)]
Cleaning up the code; still need to test everything.

2 years agoMaking the implementation of updateBacktrackSetDFS closer to the paper in DPORStateRe...
rtrimana [Tue, 8 Sep 2020 18:22:47 +0000 (11:22 -0700)]
Making the implementation of updateBacktrackSetDFS closer to the paper in DPORStateReducer.java.

2 years agoInitial implementation of more efficient traversal with graph summary; pretty much...
rtrimana [Fri, 4 Sep 2020 19:34:24 +0000 (12:34 -0700)]
Initial implementation of more efficient traversal with graph summary; pretty much untested and un-double-checked yet.

2 years agoAdding a new file for a more efficient implementation; the implementation for updateB...
rtrimana [Thu, 3 Sep 2020 19:10:58 +0000 (12:10 -0700)]
Adding a new file for a more efficient implementation; the implementation for updateBacktrackSetDFS is made closer to the paper.

2 years agoAdding missing 'add' into HashSet. aug2020
rtrimana [Fri, 10 Jul 2020 18:07:48 +0000 (11:07 -0700)]
Adding missing 'add' into HashSet.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Fri, 10 Jul 2020 18:04:49 +0000 (11:04 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoChanging StringBuilder into HashMap and HashSet.
rtrimana [Fri, 10 Jul 2020 18:04:29 +0000 (11:04 -0700)]
Changing StringBuilder into HashMap and HashSet.

2 years agoGenerate a new RestorableVMState object only when it's still not available in the...
rtrimana [Thu, 9 Jul 2020 22:02:54 +0000 (15:02 -0700)]
Generate a new RestorableVMState object only when it's still not available in the HashMap.

2 years agoAdding notes in the latest changes for the serializer bug fix.
rtrimana [Tue, 7 Jul 2020 22:40:53 +0000 (15:40 -0700)]
Adding notes in the latest changes for the serializer bug fix.

2 years agoMore filtering: never define a method call 'call' since Groovy generates a lot of...
rtrimana [Sat, 4 Jul 2020 00:14:00 +0000 (17:14 -0700)]
More filtering: never define a method call 'call' since Groovy generates a lot of those.

2 years agoIntegrating bug fix for CFSerializer.
rtrimana [Fri, 3 Jul 2020 16:15:17 +0000 (09:15 -0700)]
Integrating bug fix for CFSerializer.

2 years agoFixing a bug: in the second round of boolean CG, we might encounter states in the...
rtrimana [Thu, 2 Jul 2020 22:31:13 +0000 (15:31 -0700)]
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.

2 years agoAdding debug mode guards for all main methods.
rtrimana [Fri, 26 Jun 2020 22:30:12 +0000 (15:30 -0700)]
Adding debug mode guards for all main methods.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Mon, 22 Jun 2020 23:57:40 +0000 (16:57 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoAdding a way for JPF to be informed that this is DPOR; otherwise number the hacked...
rtrimana [Mon, 22 Jun 2020 23:57:06 +0000 (16:57 -0700)]
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.

2 years agoCommenting out a line that causes a lot of loops; let the exclusion trace continue...
rtrimana [Mon, 22 Jun 2020 02:53:09 +0000 (19:53 -0700)]
Commenting out a line that causes a lot of loops; let the exclusion trace continue to build up.

2 years agoBug fix: when state is not found in rGraph, that means the state is being visited...
rtrimana [Fri, 19 Jun 2020 18:50:50 +0000 (11:50 -0700)]
Bug fix: when state is not found in rGraph, that means the state is being visited and this is a loop (self-predecessor).

2 years agoA few hacks to make the list circular: this lets the CG not signal the JPF that the...
rtrimana [Fri, 19 Jun 2020 16:42:07 +0000 (09:42 -0700)]
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.

2 years agoExplored trace needs to be constructed and modified as there are predecessor branches.
rtrimana [Wed, 17 Jun 2020 23:17:20 +0000 (16:17 -0700)]
Explored trace needs to be constructed and modified as there are predecessor branches.

2 years agoRenaming a variable.
rtrimana [Wed, 17 Jun 2020 20:55:17 +0000 (13:55 -0700)]
Renaming a variable.

2 years agoFixing a bug in isConflict method.
rtrimana [Wed, 17 Jun 2020 18:25:42 +0000 (11:25 -0700)]
Fixing a bug in isConflict method.

2 years agoMaking field exclusion checks more efficient.
rtrimana [Sat, 13 Jun 2020 22:50:31 +0000 (15:50 -0700)]
Making field exclusion checks more efficient.

2 years agoCommitting main.jpf.
rtrimana [Wed, 10 Jun 2020 16:39:04 +0000 (09:39 -0700)]
Committing main.jpf.

2 years agoFurther cleaning up (naming, comments, etc.).
rtrimana [Wed, 10 Jun 2020 16:11:54 +0000 (09:11 -0700)]
Further cleaning up (naming, comments, etc.).

2 years agoAdding happens-before push back.
rtrimana [Tue, 9 Jun 2020 21:24:37 +0000 (14:24 -0700)]
Adding happens-before push back.

2 years agoCleaning up.
rtrimana [Tue, 9 Jun 2020 19:08:07 +0000 (12:08 -0700)]
Cleaning up.

2 years agoNew algorithm implementation; without pushing forward hb transaction; untested/undebu...
rtrimana [Fri, 5 Jun 2020 20:45:40 +0000 (13:45 -0700)]
New algorithm implementation; without pushing forward hb transaction; untested/undebugged yet.

2 years agoAdding different main.jpf files for different detections.
rtrimana [Thu, 21 May 2020 18:27:06 +0000 (11:27 -0700)]
Adding different main.jpf files for different detections.

2 years agoEditing main.jpf
rtrimana [Thu, 21 May 2020 18:19:14 +0000 (11:19 -0700)]
Editing main.jpf

2 years agoAdding a script to set the environment variables for groovyc.
rtrimana [Thu, 21 May 2020 18:12:50 +0000 (11:12 -0700)]
Adding a script to set the environment variables for groovyc.

2 years agoFixing a bug: need to get the right choice/event number for IntIntervalGenerator...
rtrimana [Tue, 19 May 2020 16:38:08 +0000 (09:38 -0700)]
Fixing a bug: need to get the right choice/event number for IntIntervalGenerator CGs.

2 years agoTested updating backtrack sets in the reachability graph.
rtrimana [Fri, 15 May 2020 23:27:23 +0000 (16:27 -0700)]
Tested updating backtrack sets in the reachability graph.

2 years agoTested backtrack in a cycle (local).
rtrimana [Fri, 15 May 2020 19:31:39 +0000 (12:31 -0700)]
Tested backtrack in a cycle (local).

2 years agoAdjusting support methods for reachability analysis with the new algorithm; untested...
rtrimana [Thu, 14 May 2020 23:36:02 +0000 (16:36 -0700)]
Adjusting support methods for reachability analysis with the new algorithm; untested yet.

2 years agoModifying the algorithm: 1) Find the first conflict and stop; 2) Perform backward...
rtrimana [Thu, 14 May 2020 21:03:40 +0000 (14:03 -0700)]
Modifying the algorithm: 1) Find the first conflict and stop; 2) Perform backward DFS to find conflicts in the execution graph.

2 years agoFixing a bug: completing reachability graph with missing past traces.
rtrimana [Thu, 7 May 2020 18:14:42 +0000 (11:14 -0700)]
Fixing a bug: completing reachability graph with missing past traces.

2 years agoFixing bugs: state to reachability graph map has to be updated for every new state...
rtrimana [Sat, 2 May 2020 15:25:49 +0000 (08:25 -0700)]
Fixing bugs: state to reachability graph map has to be updated for every new state in the stateAdvanced method.

2 years agoAdding reachability graph for past executions.
rtrimana [Fri, 1 May 2020 22:47:12 +0000 (15:47 -0700)]
Adding reachability graph for past executions.

2 years agoAdditional logging feature.
rtrimana [Mon, 20 Apr 2020 19:29:48 +0000 (12:29 -0700)]
Additional logging feature.

2 years agoFixing a bug: mapping state to event has to be done after the execution termination...
rtrimana [Thu, 16 Apr 2020 21:44:45 +0000 (14:44 -0700)]
Fixing a bug: mapping state to event has to be done after the execution termination check, otherwise we stop too early.

2 years agoFixing more bugs with the reachability analysis.
rtrimana [Wed, 15 Apr 2020 23:34:11 +0000 (16:34 -0700)]
Fixing more bugs with the reachability analysis.

2 years agoFixing more potential bugs for the reachability analysis.
rtrimana [Wed, 15 Apr 2020 19:11:07 +0000 (12:11 -0700)]
Fixing more potential bugs for the reachability analysis.

2 years agoFixing a bug: separating the state tracking for cycle analysis.
rtrimana [Wed, 15 Apr 2020 06:53:59 +0000 (23:53 -0700)]
Fixing a bug: separating the state tracking for cycle analysis.

2 years agoAdding reachability analysis when state matching occurs.
rtrimana [Tue, 14 Apr 2020 23:24:10 +0000 (16:24 -0700)]
Adding reachability analysis when state matching occurs.

2 years agoModifying main.jpf
rtrimana [Mon, 13 Apr 2020 20:16:26 +0000 (13:16 -0700)]
Modifying main.jpf

2 years agoAdding a counter for number of conflicts.
rtrimana [Sun, 12 Apr 2020 07:21:43 +0000 (00:21 -0700)]
Adding a counter for number of conflicts.

2 years agoPrinting out the number of transitions.
rtrimana [Sat, 11 Apr 2020 21:26:46 +0000 (14:26 -0700)]
Printing out the number of transitions.

2 years agoFixing a bug: misunderstood how the VOD graph is supposed to be generated; we basical...
rtrimana [Fri, 10 Apr 2020 22:29:50 +0000 (15:29 -0700)]
Fixing a bug: misunderstood how the VOD graph is supposed to be generated; we basically track the transitions that produce new states.

2 years agoTesting DPORStateReducer and ConflictTracker: JPF seems to work fine and find the...
rtrimana [Thu, 9 Apr 2020 23:44:57 +0000 (16:44 -0700)]
Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the conflicts.

2 years agoFixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove...
rtrimana [Thu, 9 Apr 2020 23:29:40 +0000 (16:29 -0700)]
Fixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove a node from the queue.

2 years agoFixing a bug: VOD graph traversal should continue with the next neighbor when there...
rtrimana [Thu, 9 Apr 2020 23:18:40 +0000 (16:18 -0700)]
Fixing a bug: VOD graph traversal should continue with the next neighbor when there is a loop (repeated node found).

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Thu, 9 Apr 2020 22:57:20 +0000 (15:57 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoFixing a bug: restorable state has to be saved when backtrack point info is saved...
rtrimana [Thu, 9 Apr 2020 22:57:06 +0000 (15:57 -0700)]
Fixing a bug: restorable state has to be saved when backtrack point info is saved to get the appropriate CG type when restoring.

2 years agoOptimization: Compare just the state and the fist event/choice of the trace to not...
rtrimana [Thu, 9 Apr 2020 16:40:28 +0000 (09:40 -0700)]
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.

2 years agoChanging approach: Using vm.restoreState() method to restore JPF to the desired state...
rtrimana [Thu, 9 Apr 2020 07:03:43 +0000 (00:03 -0700)]
Changing approach: Using vm.restoreState() method to restore JPF to the desired state when backtracking; everything looks correct but probably needs more tests.

2 years agoCommitting a version that almost works: bug to fix is that when an execution finishes...
rtrimana [Wed, 8 Apr 2020 21:30:55 +0000 (14:30 -0700)]
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.

2 years agoFirst part of boolean flip seems to be clean; need to debug the second part and figur...
rtrimana [Tue, 7 Apr 2020 23:53:36 +0000 (16:53 -0700)]
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.

2 years agoFixing a potential bug: we now store the event number in the ArrayList together with...
rtrimana [Tue, 7 Apr 2020 17:31:21 +0000 (10:31 -0700)]
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.

2 years agoCleaning up and fixing bugs; new DPOR implementation seems to be correct; need to...
rtrimana [Mon, 6 Apr 2020 23:31:08 +0000 (16:31 -0700)]
Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to test with other pairs.

2 years agoFixing a bug: we need to start choiceCounter from 1 instead of 0 for subsequent execu...
rtrimana [Sat, 4 Apr 2020 04:34:28 +0000 (21:34 -0700)]
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.

2 years agoReimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points...
rtrimana [Fri, 3 Apr 2020 23:13:34 +0000 (16:13 -0700)]
Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points); need to test how CGs are explored with the current DFSearch.

2 years agoReimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and...
rtrimana [Thu, 2 Apr 2020 23:20:26 +0000 (16:20 -0700)]
Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and conflict analysis; cleaning up and refactoring.

2 years agoReimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access...
rtrimana [Wed, 1 Apr 2020 23:44:57 +0000 (16:44 -0700)]
Reimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access analysis.

2 years agoStarting a new DPOR implementation.
rtrimana [Wed, 1 Apr 2020 18:20:05 +0000 (11:20 -0700)]
Starting a new DPOR implementation.

2 years agoCleaning up and refactoring.
rtrimana [Wed, 1 Apr 2020 18:09:26 +0000 (11:09 -0700)]
Cleaning up and refactoring.