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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

21 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

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

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

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

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

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

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

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

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

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

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

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

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

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

21 months agoFixing bugs: capturing object accesses (read/write) in iterators.
rtrimana [Tue, 31 Mar 2020 23:25:00 +0000 (16:25 -0700)]
Fixing bugs: capturing object accesses (read/write) in iterators.

21 months agoFixing a bug: off-by-one error in the executed trace checking.
rtrimana [Fri, 27 Mar 2020 23:49:04 +0000 (16:49 -0700)]
Fixing a bug: off-by-one error in the executed trace checking.

21 months agoRe-checking and cleaning up the code: most likely still have a bug in re-ordering...
rtrimana [Fri, 27 Mar 2020 22:55:00 +0000 (15:55 -0700)]
Re-checking and cleaning up the code: most likely still have a bug in re-ordering the two apps.

22 months agoAdding the old tracker variable for debugging/testing purposes.
rtrimana [Thu, 26 Mar 2020 18:52:49 +0000 (11:52 -0700)]
Adding the old tracker variable for debugging/testing purposes.

22 months agoFixing bugs and cleaning up: Continuing sub-graph executions when there is no matched...
rtrimana [Thu, 26 Mar 2020 01:56:27 +0000 (18:56 -0700)]
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.

22 months agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Wed, 25 Mar 2020 22:43:55 +0000 (15:43 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

22 months agoFixing bugs and cleaning up: making sure that the execution of the first trace has...
rtrimana [Wed, 25 Mar 2020 22:43:13 +0000 (15:43 -0700)]
Fixing bugs and cleaning up: making sure that the execution of the first trace has fair-scheduling with appropriate state-matching.

22 months agoMaking analysis compatible with infra
Seyed Amir Hossein Aqajari [Tue, 24 Mar 2020 22:51:11 +0000 (15:51 -0700)]
Making analysis compatible with infra

22 months agoMaking analysis compatible with new infrastructure
Seyed Amir Hossein Aqajari [Tue, 24 Mar 2020 22:50:03 +0000 (15:50 -0700)]
Making analysis compatible with new infrastructure

22 months agoCleaning up: Removing the full-blown graph traversal.
rtrimana [Mon, 23 Mar 2020 21:56:29 +0000 (14:56 -0700)]
Cleaning up: Removing the full-blown graph traversal.

22 months agoCleaning up, fixing bugs---commented out full-blown graph traversal code.
rtrimana [Mon, 23 Mar 2020 21:41:04 +0000 (14:41 -0700)]
Cleaning up, fixing bugs---commented out full-blown graph traversal code.

22 months agoRefactoring; Finding cycles without traversing the entire state graph.
rtrimana [Sat, 21 Mar 2020 04:34:59 +0000 (21:34 -0700)]
Refactoring; Finding cycles without traversing the entire state graph.

22 months agoFixing bugs: moving VOD-graph building into the CGAdvanced method to have the most...
rtrimana [Fri, 20 Mar 2020 21:11:09 +0000 (14:11 -0700)]
Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most up-to-date values.

22 months agoAdding graph traversal to find cycles; adding debug mode for ConflictTracker.
rtrimana [Thu, 19 Mar 2020 18:14:58 +0000 (11:14 -0700)]
Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

22 months agoSome fixes for the DPOR state-reducer.
rtrimana [Mon, 16 Mar 2020 20:44:02 +0000 (13:44 -0700)]
Some fixes for the DPOR state-reducer.

22 months agoFixing a bug: merging the analysis part for locationMode w.r.t manual interaction...
rtrimana [Mon, 2 Mar 2020 22:12:31 +0000 (14:12 -0800)]
Fixing a bug: merging the analysis part for locationMode w.r.t manual interaction flag.

22 months agoFix for a bug in finding the right integer values in the stack frame: need to find...
rtrimana [Fri, 28 Feb 2020 21:36:27 +0000 (13:36 -0800)]
Fix for a bug in finding the right integer values in the stack frame: need to find a value that's not 0 in the frame (previously we only look at offset 0 or 1 because of adapting the function getValue() from a listener for Java code).

22 months agoAdding attributes for dimmers.
rtrimana [Fri, 28 Feb 2020 19:31:36 +0000 (11:31 -0800)]
Adding attributes for dimmers.

22 months agoCode to print graph to output so that dot can be used to generate pdf of graph.
Brian Demsky [Wed, 26 Feb 2020 21:19:26 +0000 (13:19 -0800)]
Code to print graph to output so that dot can be used to generate pdf of graph.

23 months agoAdding manual transactions to the conflict tracker
Seyed Amir Hossein Aqajari [Wed, 19 Feb 2020 19:21:38 +0000 (11:21 -0800)]
Adding manual transactions to the conflict tracker

23 months agoSlight changes for safeguard.
rtrimana [Sat, 15 Feb 2020 00:11:23 +0000 (16:11 -0800)]
Slight changes for safeguard.

23 months agoFixing an out of bound bug.
rtrimana [Fri, 14 Feb 2020 18:32:06 +0000 (10:32 -0800)]
Fixing an out of bound bug.

23 months agoJPF ready to run with old infrastructure
Seyed Amir Hossein Aqajari [Thu, 13 Feb 2020 21:39:36 +0000 (13:39 -0800)]
JPF ready to run with old infrastructure

23 months agoAdding a prevChoiceValue class property to store the previous choice to update the...
rtrimana [Mon, 10 Feb 2020 21:38:03 +0000 (13:38 -0800)]
Adding a prevChoiceValue class property to store the previous choice to update the VOD graph correctly.

23 months agoAttempting state-based DPOR implementation from the SPIN paper.
rtrimana [Fri, 7 Feb 2020 23:08:59 +0000 (15:08 -0800)]
Attempting state-based DPOR implementation from the SPIN paper.

23 months agoAdding the first implementation of visible operation dependency graph for stateful...
rtrimana [Thu, 30 Jan 2020 20:08:01 +0000 (12:08 -0800)]
Adding the first implementation of visible operation dependency graph for stateful DPOR: need to do more test to make sure that it's really working.

2 years agoMake updates and not edges have manual property
Brian Demsky [Tue, 17 Dec 2019 06:57:19 +0000 (22:57 -0800)]
Make updates and not edges have manual property

2 years agoClean up comments
Brian Demsky [Tue, 17 Dec 2019 06:41:16 +0000 (22:41 -0800)]
Clean up comments

2 years agoRewrite of Conflict Tracker
Brian Demsky [Tue, 17 Dec 2019 06:35:45 +0000 (22:35 -0800)]
Rewrite of Conflict Tracker

2 years agoA change in updateTheOutSet in conflict tracker analysis
amiraj [Tue, 17 Dec 2019 01:03:33 +0000 (17:03 -0800)]
A change in updateTheOutSet in conflict tracker analysis

2 years agoA change in propagate method.
amiraj [Thu, 12 Dec 2019 22:30:53 +0000 (14:30 -0800)]
A change in propagate method.

2 years agoFixing a bug in Conflict Tracker + Make propagate method much simpler
amiraj [Thu, 12 Dec 2019 20:34:21 +0000 (12:34 -0800)]
Fixing a bug in Conflict Tracker + Make propagate method much simpler

2 years agoMake a change in ConflictTracker analysis
amiraj [Wed, 11 Dec 2019 21:21:41 +0000 (13:21 -0800)]
Make a change in ConflictTracker analysis

2 years agoCompacting the methods
Seyed Amir Hossein Aqajari [Sat, 7 Dec 2019 00:25:17 +0000 (16:25 -0800)]
Compacting the methods

2 years agoA change in propagate the change method
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 22:46:04 +0000 (14:46 -0800)]
A change in propagate the change method

2 years agoMake the analysis more efficient
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 20:46:02 +0000 (12:46 -0800)]
Make the analysis more efficient

2 years agoFixing a small bug in Conflict Tracker
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 20:36:29 +0000 (12:36 -0800)]
Fixing a small bug in Conflict Tracker

2 years agoFixing bugs in Conflict Tracker
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 23:40:05 +0000 (15:40 -0800)]
Fixing bugs in Conflict Tracker

2 years agoFixing a bug
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:48:15 +0000 (14:48 -0800)]
Fixing a bug

2 years agoFixing a bug in checkForConflict method in Conflict Tracker analysis!
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:45:43 +0000 (14:45 -0800)]
Fixing a bug in checkForConflict method in Conflict Tracker analysis!

2 years agoFixing a bug in manual_write-non_conflict + setSet conflicts
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:15:39 +0000 (14:15 -0800)]
Fixing a bug in manual_write-non_conflict + setSet conflicts

2 years agoFixing a bug in Conflict Tracker analysis
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 19:47:54 +0000 (11:47 -0800)]
Fixing a bug in Conflict Tracker analysis

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Wed, 4 Dec 2019 21:20:19 +0000 (13:20 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoFixing bug: completing missing/unexplored event combinations.
rtrimana [Wed, 4 Dec 2019 21:20:00 +0000 (13:20 -0800)]
Fixing bug: completing missing/unexplored event combinations.

2 years agoChange in Analysis
amiraj [Wed, 4 Dec 2019 02:21:11 +0000 (18:21 -0800)]
Change in Analysis

2 years agoChange in conflict tracker!
amiraj [Wed, 4 Dec 2019 02:11:52 +0000 (18:11 -0800)]
Change in conflict tracker!

2 years agoChange in listener
amiraj [Tue, 3 Dec 2019 23:38:23 +0000 (15:38 -0800)]
Change in listener

2 years agoChange in the Conflict Tracker analysis
amiraj [Tue, 3 Dec 2019 22:31:21 +0000 (14:31 -0800)]
Change in the Conflict Tracker analysis

2 years agoA minor change in ConflictTracker.java
Seyed Amir Hossein Aqajari [Thu, 21 Nov 2019 01:27:46 +0000 (17:27 -0800)]
A minor change in ConflictTracker.java

2 years agoMinor bug fix in ConflictTracker.java
Seyed Amir Hossein Aqajari [Mon, 18 Nov 2019 23:47:44 +0000 (15:47 -0800)]
Minor bug fix in ConflictTracker.java

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
Seyed Amir Hossein Aqajari [Mon, 18 Nov 2019 23:33:03 +0000 (15:33 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoFixing a bug in ConflictTracker.java
Seyed Amir Hossein Aqajari [Mon, 18 Nov 2019 23:32:35 +0000 (15:32 -0800)]
Fixing a bug in ConflictTracker.java

2 years agoCode refactoring for sleep set and persistent set analyses.
rtrimana [Mon, 18 Nov 2019 21:08:29 +0000 (13:08 -0800)]
Code refactoring for sleep set and persistent set analyses.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Fri, 15 Nov 2019 23:22:22 +0000 (15:22 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoImplementing the sleep-set technique for the previous version to explore less combina...
rtrimana [Fri, 15 Nov 2019 23:22:03 +0000 (15:22 -0800)]
Implementing the sleep-set technique for the previous version to explore less combinations of events.

2 years agoMinor changes in ConflictTracker
Seyed Amir Hossein Aqajari [Fri, 15 Nov 2019 19:44:01 +0000 (11:44 -0800)]
Minor changes in ConflictTracker

2 years agoFix a bug in ConflictTracker
Seyed Amir Hossein Aqajari [Thu, 14 Nov 2019 21:31:16 +0000 (13:31 -0800)]
Fix a bug in ConflictTracker

2 years agoFix a bug in ConflictTracker.java
amiraj [Thu, 14 Nov 2019 19:21:53 +0000 (11:21 -0800)]
Fix a bug in ConflictTracker.java

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Tue, 12 Nov 2019 21:32:16 +0000 (13:32 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoChecking in (1) StateReducer, and (2) StateReducerEfficient; ISSUE: the StateReducerE...
rtrimana [Tue, 12 Nov 2019 21:32:02 +0000 (13:32 -0800)]
Checking in (1) StateReducer, and (2) StateReducerEfficient; ISSUE: the StateReducerEfficient doesn't traverse the sub-graphs completely and JPF ignores some of the child CGs---incomplete POR.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
amiraj [Thu, 7 Nov 2019 00:08:22 +0000 (16:08 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoMake some changes in ConflictTracker listener.
amiraj [Thu, 7 Nov 2019 00:06:15 +0000 (16:06 -0800)]
Make some changes in ConflictTracker listener.

2 years agoFixing a bug: wrong CGs were reset when recursing into a sub-graph.
rtrimana [Wed, 6 Nov 2019 19:41:20 +0000 (11:41 -0800)]
Fixing a bug: wrong CGs were reset when recursing into a sub-graph.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Tue, 5 Nov 2019 21:41:04 +0000 (13:41 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoCompleting POR implementation with complete recursions.
rtrimana [Tue, 5 Nov 2019 21:40:48 +0000 (13:40 -0800)]
Completing POR implementation with complete recursions.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
amiraj [Thu, 24 Oct 2019 23:17:21 +0000 (16:17 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoModifying conflict tracker
amiraj [Thu, 24 Oct 2019 23:16:47 +0000 (16:16 -0700)]
Modifying conflict tracker

2 years agoFurther excluding infrastructure/library field accesses.
rtrimana [Wed, 23 Oct 2019 19:19:08 +0000 (12:19 -0700)]
Further excluding infrastructure/library field accesses.

2 years agoFixing issues: counter bugs, object ID comparison, exclusion of non-event and non...
rtrimana [Tue, 22 Oct 2019 21:17:40 +0000 (14:17 -0700)]
Fixing issues: counter bugs, object ID comparison, exclusion of non-event and non-app field sharing.

2 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Mon, 21 Oct 2019 20:52:13 +0000 (13:52 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

2 years agoAdding more restrictions in conflict analysis: not to analyze fields from the Groovy...
rtrimana [Mon, 21 Oct 2019 20:51:52 +0000 (13:51 -0700)]
Adding more restrictions in conflict analysis: not to analyze fields from the Groovy library.