From: rtrimana Date: Wed, 1 Apr 2020 18:20:05 +0000 (-0700) Subject: Starting a new DPOR implementation. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=c003a76b9c164b2b07f2fd8515ea36af2a6167e8 Starting a new DPOR implementation. --- diff --git a/main.jpf b/main.jpf index fdeadac..0948c38 100644 --- 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 index 0000000..746adfe --- /dev/null +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -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"); + } + } +} diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index ba5994d..a1a01c2 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -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