jpf-core.git
6 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.

8 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.

8 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.

8 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.

8 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.

9 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.

9 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.

9 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).

9 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).

9 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.

9 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.

9 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.

9 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().

10 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.

10 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.

10 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.

10 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.

10 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.

10 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.

10 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.

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

10 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.

10 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.

10 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.

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

12 months 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.

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

13 months 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.

13 months 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.

13 months 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.

13 months 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.

13 months 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.

13 months 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.

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

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

13 months 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.

13 months 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.

13 months 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.

13 months 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.

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

15 months 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

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

15 months 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.

15 months 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.

15 months 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.

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

15 months 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.

15 months 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.

16 months 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

16 months 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.

16 months 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.

16 months 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).

16 months 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.

16 months 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.

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

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

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

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

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

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

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

16 months 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.

17 months 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.

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

17 months 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.

17 months 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.

17 months 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.

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

17 months 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.

17 months 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.

17 months 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.

17 months 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.

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

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

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

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

18 months 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.

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

18 months 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.

18 months 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.

18 months 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.

18 months 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).

18 months 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

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

18 months 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.

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

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