Starting a new DPOR implementation.
authorrtrimana <rtrimana@uci.edu>
Wed, 1 Apr 2020 18:20:05 +0000 (11:20 -0700)
committerrtrimana <rtrimana@uci.edu>
Wed, 1 Apr 2020 18:20:05 +0000 (11:20 -0700)
main.jpf
src/main/gov/nasa/jpf/listener/DPORStateReducer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StateReducer.java

index fdeadac..0948c38 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -6,13 +6,10 @@ target = main
 #listener=gov.nasa.jpf.listener.StateReducerOld
 #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
-#listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
-#listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerSimple
-listener=gov.nasa.jpf.listener.ConflictTrackerOld
-
-#listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean
-#listener=gov.nasa.jpf.listener.StateReducerClean
-#listener=gov.nasa.jpf.listener.StateReducer
+##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
+##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer
+##listener=gov.nasa.jpf.listener.ConflictTrackerOld
+listener=gov.nasa.jpf.listener.DPORStateReducer
 
 # Potentially conflicting variables
 # Alarms
@@ -46,10 +43,10 @@ apps=App1,App2
 
 # Debug mode for ConflictTracker
 # We do not report any conflicts if the value is true
-debug_mode=true
+#debug_mode=true
 
 # Debug mode for StateReducer
-#debug_state_transition=true
+#printout_state_transition=true
 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)
diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
new file mode 100644 (file)
index 0000000..746adfe
--- /dev/null
@@ -0,0 +1,129 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ *        http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.listener;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.jvm.bytecode.*;
+import gov.nasa.jpf.vm.*;
+import gov.nasa.jpf.vm.bytecode.ReadInstruction;
+import gov.nasa.jpf.vm.bytecode.WriteInstruction;
+import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
+import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
+
+import java.io.PrintWriter;
+import java.util.*;
+
+// TODO: Fix for Groovy's model-checking
+// TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
+/**
+ * Simple tool to log state changes.
+ *
+ * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
+ * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
+ *
+ * The algorithm is presented on page 11 of the paper. Basically, we create a graph G
+ * (i.e., visible operation dependency graph)
+ * that maps inter-related threads/sub-programs that trigger state changes.
+ * The key to this approach is that we evaluate graph G in every iteration/recursion to
+ * only update the backtrack sets of the threads/sub-programs that are reachable in graph G
+ * from the currently running thread/sub-program.
+ */
+public class DPORStateReducer extends ListenerAdapter {
+
+  // Debug info fields
+  private boolean verboseMode;
+  private boolean stateReductionMode;
+  private final PrintWriter out;
+  private String detail;
+  private int depth;
+  private int id;
+  private Transition transition;
+
+  public DPORStateReducer(Config config, JPF jpf) {
+    verboseMode = config.getBoolean("printout_state_transition", false);
+    stateReductionMode = config.getBoolean("activate_state_reduction", true);
+    if (verboseMode) {
+      out = new PrintWriter(System.out, true);
+    } else {
+      out = null;
+    }
+  }
+
+  @Override
+  public void stateRestored(Search search) {
+    if (verboseMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      detail = null;
+      out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
+              " and depth: " + depth + "\n");
+    }
+  }
+
+  @Override
+  public void searchStarted(Search search) {
+    if (verboseMode) {
+      out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
+    }
+  }
+
+  @Override
+  public void stateAdvanced(Search search) {
+    if (verboseMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      if (search.isNewState()) {
+        detail = "new";
+      } else {
+        detail = "visited";
+      }
+
+      if (search.isEndState()) {
+        out.println("\n==> DEBUG: This is the last state!\n");
+        detail += " end";
+      }
+      out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
+              " which is " + detail + " Transition: " + transition + "\n");
+    }
+  }
+
+  @Override
+  public void stateBacktracked(Search search) {
+    if (verboseMode) {
+      id = search.getStateId();
+      depth = search.getDepth();
+      transition = search.getTransition();
+      detail = null;
+
+      out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
+              " and depth: " + depth + "\n");
+    }
+  }
+
+  @Override
+  public void searchFinished(Search search) {
+    if (verboseMode) {
+      out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
+    }
+  }
+}
index ba5994d..a1a01c2 100644 (file)
@@ -28,9 +28,7 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
-import java.awt.*;
 import java.io.PrintWriter;
-
 import java.util.*;
 
 // TODO: Fix for Groovy's model-checking