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

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

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

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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

4 years 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.

4 years 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

4 years 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

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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.

4 years 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).

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

4 years 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.

4 years 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

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

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

4 years 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

4 years 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.

4 years 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.

4 years 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.

4 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

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

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

4 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

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

4 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

4 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

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

4 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

4 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

4 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

4 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

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

4 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!

4 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

4 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

4 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

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

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

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

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

4 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

4 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

4 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

4 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

4 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

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

4 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

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

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

4 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

4 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

5 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

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

5 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

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

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

5 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

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

5 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

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

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

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

5 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

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

5 years agoFixing a bug in ConflictTracker.java
amiraj [Fri, 18 Oct 2019 22:46:55 +0000 (15:46 -0700)]
Fixing a bug in ConflictTracker.java

5 years agoDetecting location mode read/write using the old method.
rtrimana [Fri, 18 Oct 2019 20:22:29 +0000 (13:22 -0700)]
Detecting location mode read/write using the old method.

5 years agoFixing a bug in listener!
amiraj [Fri, 18 Oct 2019 18:19:16 +0000 (11:19 -0700)]
Fixing a bug in listener!

5 years agoAdd required variables of the new listener to the config file.
amiraj [Thu, 17 Oct 2019 19:33:53 +0000 (12:33 -0700)]
Add required variables of the new listener to the config file.

5 years agoAdd the ConflictTracker to the main branch
amiraj [Thu, 17 Oct 2019 19:16:51 +0000 (12:16 -0700)]
Add the ConflictTracker to the main branch

5 years agoMore subtle changes to config file and state reducer listener.
rtrimana [Wed, 16 Oct 2019 23:40:04 +0000 (16:40 -0700)]
More subtle changes to config file and state reducer listener.

5 years agoFixing a few bugs. Still need to check for the backtrack analysis.
rtrimana [Wed, 16 Oct 2019 18:52:22 +0000 (11:52 -0700)]
Fixing a few bugs. Still need to check for the backtrack analysis.

5 years agoFirst version of POR; need to double check the backtrack set analysis.
rtrimana [Tue, 15 Oct 2019 22:04:51 +0000 (15:04 -0700)]
First version of POR; need to double check the backtrack set analysis.

5 years agoAdding more state reduction analysis.
rtrimana [Fri, 27 Sep 2019 22:04:28 +0000 (15:04 -0700)]
Adding more state reduction analysis.

5 years agoAdding the option to activate beam search: a HeuristicSearch with a state queue that...
rtrimana [Thu, 26 Sep 2019 21:04:01 +0000 (14:04 -0700)]
Adding the option to activate beam search: a HeuristicSearch with a state queue that is reset at each level.

5 years agoFixing a typo in option name.
rtrimana [Thu, 26 Sep 2019 20:32:38 +0000 (13:32 -0700)]
Fixing a typo in option name.

5 years agoUpdating main.jpf; Cleaning up the StateReducer.
rtrimana [Wed, 25 Sep 2019 20:52:48 +0000 (13:52 -0700)]
Updating main.jpf; Cleaning up the StateReducer.

5 years agoFirst version of the StateReducer class.
rtrimana [Wed, 25 Sep 2019 17:58:25 +0000 (10:58 -0700)]
First version of the StateReducer class.

5 years agoAdding cameras.
rtrimana [Sun, 11 Aug 2019 00:27:02 +0000 (17:27 -0700)]
Adding cameras.

5 years agoChecking for null value before storing the first write.
rtrimana [Thu, 8 Aug 2019 22:06:15 +0000 (15:06 -0700)]
Checking for null value before storing the first write.

5 years agoChanging main.jpf
rtrimana [Thu, 8 Aug 2019 17:17:54 +0000 (10:17 -0700)]
Changing main.jpf

5 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Thu, 8 Aug 2019 06:51:02 +0000 (23:51 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

5 years agoAdding a new variable.
rtrimana [Thu, 8 Aug 2019 06:50:25 +0000 (23:50 -0700)]
Adding a new variable.

5 years agoAdding a new conflict variable.
rtrimana [Thu, 8 Aug 2019 05:55:25 +0000 (22:55 -0700)]
Adding a new conflict variable.

5 years agoAdding a null value filter in the tracker; Adding a new conflict variable for lights.
rtrimana [Wed, 7 Aug 2019 17:21:49 +0000 (10:21 -0700)]
Adding a null value filter in the tracker; Adding a new conflict variable for lights.

5 years agoAdding conflict variable for Speeches.
rtrimana [Tue, 6 Aug 2019 22:35:28 +0000 (15:35 -0700)]
Adding conflict variable for Speeches.

5 years agoMore state reduction
bdemsky [Tue, 6 Aug 2019 19:45:05 +0000 (12:45 -0700)]
More state reduction

5 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
bdemsky [Tue, 6 Aug 2019 06:51:36 +0000 (23:51 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

5 years agoSmall improvment in state reduction
bdemsky [Tue, 6 Aug 2019 06:51:21 +0000 (23:51 -0700)]
Small improvment in state reduction

5 years agoAdding conflict variables for lights.
rtrimana [Mon, 5 Aug 2019 18:02:51 +0000 (11:02 -0700)]
Adding conflict variables for lights.

5 years agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
bdemsky [Sat, 3 Aug 2019 07:06:20 +0000 (00:06 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core