--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/vm/MultiProcessVM.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,466 @@
+/*
+ * 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.vm;
+
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.JPFConfigException;
+import gov.nasa.jpf.util.IntTable;
+import gov.nasa.jpf.util.Misc;
+import gov.nasa.jpf.util.Predicate;
+import gov.nasa.jpf.vm.choice.BreakGenerator;
+
+import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * A VM implementation that simulates running multiple applications within the same
+ * JPF process (centralized model checking of distributed applications).
+ * This is achieved by executing each application in a separate thread group,
+ * using separate SystemClassLoader instances to ensure proper separation of types / static fields.
+ * 
+ * 
+ * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
+ * 
+ * To use this jpf.properties includes,
+ *              vm.class = gov.nasa.jpf.vm.MultiProcessVM 
+ */
+public class MultiProcessVM extends VM {
+
+  static final int MAX_APP = 32;
+
+  ApplicationContext[] appCtxs;
+  
+  MultiProcessPredicate runnablePredicate;
+  MultiProcessPredicate appTimedoutRunnablePredicate;
+  MultiProcessPredicate appDaemonRunnablePredicate;
+  MultiProcessPredicate appPredicate;
+  protected Predicate<ThreadInfo> systemInUsePredicate;
+  
+  public MultiProcessVM (JPF jpf, Config conf) {
+    super(jpf, conf);
+    
+    appCtxs = createApplicationContexts();
+    
+    initializePredicates();
+  }
+  
+  void initializePredicates() {
+    runnablePredicate = new MultiProcessPredicate() {
+      @Override
+	public boolean isTrue (ThreadInfo t){
+        return (t.isRunnable() && this.appCtx == t.appCtx);
+      }
+    };
+    
+    appTimedoutRunnablePredicate = new MultiProcessPredicate() {
+      @Override
+	public boolean isTrue (ThreadInfo t){
+        return (this.appCtx == t.appCtx && t.isTimeoutRunnable());
+      }
+    }; 
+    
+    appDaemonRunnablePredicate = new MultiProcessPredicate() {
+      @Override
+	public boolean isTrue (ThreadInfo t){
+        return (this.appCtx == t.appCtx && t.isRunnable() && t.isDaemon());
+      }
+    };
+    
+    appPredicate = new MultiProcessPredicate() {
+      @Override
+	public boolean isTrue (ThreadInfo t){
+        return (this.appCtx == t.appCtx);
+      }
+    };
+    
+    
+    // this predicates collects those finalizers which are either runnable or
+    // have some queued objects to process.
+    systemInUsePredicate = new Predicate<ThreadInfo> () {
+      @Override
+	public boolean isTrue (ThreadInfo t){
+        boolean isTrue = false;
+        if(t.isSystemThread()) {
+          if(t.isRunnable()) {
+            isTrue = true;
+          } else {
+            FinalizerThreadInfo finalizer = (FinalizerThreadInfo) t;
+            isTrue = !finalizer.isIdle();
+          }
+        }
+        return isTrue;
+      }
+    };
+  }
+
+  /**
+   * <2do> this should also handle command line specs such as "jpf ... tgt1 tgt1_arg ... -- tgt2 tgt2_arg ... 
+   */
+  ApplicationContext[] createApplicationContexts(){
+    String[] targets;
+
+    int replicate = config.getInt("target.replicate", 0);
+    if(replicate>0) {
+      String target = config.getProperty("target");
+      targets = new String[replicate];
+      for(int i=0; i<replicate; i++) {
+        targets[i] = target;
+      }
+    } else {
+      targets = config.getStringEnumeration("target", MAX_APP);
+    }
+
+    if (targets == null){
+      throw new JPFConfigException("no applications specified, check 'target.N' settings");
+    }
+    
+    ArrayList<ApplicationContext> list = new ArrayList<ApplicationContext>(targets.length);
+    for (int i=0; i<targets.length; i++){
+      if (targets[i] != null){ // there might be holes in the array
+        String clsName = targets[i];
+        if (!isValidClassName(clsName)) {
+          throw new JPFConfigException("main class not a valid class name: " + clsName);
+        }
+        
+        String argsKey;
+        String entryKey;
+        String hostKey;
+        if(replicate>0) {
+          argsKey = "target.args";
+          entryKey = "target.entry";
+          hostKey = "target.host";
+        } else {
+          argsKey = "target.args." + i;
+          entryKey = "target.entry." + i;
+          hostKey = "target.host." + i;
+        }
+        
+        String[] args = config.getCompactStringArray(argsKey);
+        if (args == null){
+          args = EMPTY_ARGS;
+        }
+        
+        String mainEntry = config.getString(entryKey, "main([Ljava/lang/String;)V");
+        
+        String host = config.getString(hostKey, "localhost");
+        
+        SystemClassLoaderInfo sysCli = createSystemClassLoaderInfo(list.size());
+    
+        ApplicationContext appCtx = new ApplicationContext( i, clsName, mainEntry, args, host, sysCli);
+        list.add( appCtx);
+      }
+    }
+    
+    return list.toArray(new ApplicationContext[list.size()]);
+  }
+
+  @Override
+  public boolean initialize(){
+    try {
+      ThreadInfo tiFirst = null;
+      
+      for (int i=0; i<appCtxs.length; i++){
+        ApplicationContext appCtx = appCtxs[i];
+    
+        // this has to happen before we load the startup classes during initializeMainThread
+        scheduler.initialize(this, appCtx);
+    
+        ThreadInfo tiMain = initializeMainThread(appCtx, i);
+        initializeFinalizerThread(appCtx, appCtxs.length+i);
+        
+        if (tiMain == null) {
+          return false; // bail out
+        }
+        if (tiFirst == null){
+          tiFirst = tiMain;
+        }
+      }
+
+      initSystemState(tiFirst);
+      initialized = true;
+      notifyVMInitialized();
+      
+      return true;
+      
+    } catch (JPFConfigException cfe){
+      log.severe(cfe.getMessage());
+      return false;
+    } catch (ClassInfoException cie){
+      log.severe(cie.getMessage());
+      return false;
+    }
+    // all other exceptions are JPF errors that should cause stack traces
+  }
+
+  @Override
+  public int getNumberOfApplications(){
+    return appCtxs.length;
+  }
+    
+  @Override
+  public ApplicationContext getApplicationContext(int objRef) {
+    VM vm = VM.getVM();
+
+    ClassInfo ci = vm.getElementInfo(objRef).getClassInfo();
+    while(!ci.isObjectClassInfo()) {
+      ci = ci.getSuperClass();
+    }
+
+    ClassLoaderInfo sysLoader = ci.getClassLoaderInfo();
+    ApplicationContext[] appContext = vm.getApplicationContexts();
+    
+    for(int i=0; i<appContext.length; i++) {
+      if(appContext[i].getSystemClassLoader() == sysLoader) {
+        return appContext[i];
+      }
+    }
+    return null;
+  }
+  
+  @Override
+  public ApplicationContext[] getApplicationContexts(){
+    return appCtxs;
+  }
+
+  @Override
+  public ApplicationContext getCurrentApplicationContext(){
+    ThreadInfo ti = ThreadInfo.getCurrentThread();
+    if (ti != null){
+      return ti.getApplicationContext();
+    } else {
+      // return the last defined one
+      return appCtxs[appCtxs.length-1];
+    }
+  }
+
+  
+  @Override
+  public String getSUTName() {
+    StringBuilder sb = new StringBuilder();
+    
+    for (int i=0; i<appCtxs.length; i++){
+      if (i>0){
+        sb.append("+");
+      }
+      sb.append(appCtxs[i].mainClassName);
+    }
+    
+    return sb.toString();
+  }
+
+  @Override
+  public String getSUTDescription(){
+    StringBuilder sb = new StringBuilder();
+    
+    for (int i=0; i<appCtxs.length; i++){
+      if (i>0){
+        sb.append('+'); // "||" would be more fitting, but would screw up filenames
+      }
+
+      ApplicationContext appCtx = appCtxs[i];
+      sb.append(appCtx.mainClassName);
+      sb.append('.');
+      sb.append(Misc.upToFirst(appCtx.mainEntry, '('));
+
+      sb.append('(');
+      String[] args = appCtx.args;
+      for (int j = 0; j < args.length; j++) {
+        if (j > 0) {
+          sb.append(',');
+        }
+        sb.append('"');
+        sb.append(args[j]);
+        sb.append('"');
+      }
+      sb.append(')');
+    }
+    
+    return sb.toString();
+  }
+
+  
+  @Override
+  public boolean isSingleProcess() {
+    return false;
+  }
+
+  @Override
+  public boolean isEndState () {
+    boolean hasNonTerminatedDaemon = getThreadList().hasAnyMatching(getUserLiveNonDaemonPredicate());
+    boolean hasRunnable = getThreadList().hasAnyMatching(getUserTimedoutRunnablePredicate());
+    boolean isEndState = !(hasNonTerminatedDaemon && hasRunnable);
+    
+    if(processFinalizers) {
+      if(isEndState) {
+        int n = getThreadList().getMatchingCount(systemInUsePredicate);
+        if(n>0) {
+          return false;
+        }
+      }
+    }
+    
+    return isEndState;
+  }
+
+  @Override
+  // Note - for now we just check for global deadlocks not the local ones which occur within a
+  // scope of a single progress
+  public boolean isDeadlocked () { 
+    boolean hasNonDaemons = false;
+    boolean hasBlockedThreads = false;
+
+    if (ss.isBlockedInAtomicSection()) {
+      return true; // blocked in atomic section
+    }
+
+    ThreadInfo[] threads = getThreadList().getThreads();
+    int len = threads.length;
+
+    boolean hasUserThreads = false;
+    for (int i=0; i<len; i++){
+      ThreadInfo ti = threads[i];
+      
+      if (ti.isAlive()) {
+        hasNonDaemons |= !ti.isDaemon();
+
+        // shortcut - if there is at least one runnable, we are not deadlocked
+        if (ti.isTimeoutRunnable()) { // willBeRunnable() ?
+          return false;
+        }
+        
+        if(!ti.isSystemThread()) {
+          hasUserThreads = true;
+        }
+
+        // means it is not NEW or TERMINATED, i.e. live & blocked
+        hasBlockedThreads = true;
+      }
+    }
+
+    boolean isDeadlock = hasNonDaemons && hasBlockedThreads;
+    
+    if(processFinalizers && isDeadlock && !hasUserThreads) {
+      // all threads are blocked, system threads. If at least one of them 
+      // is in-use, then this is a deadlocked state.
+      return (getThreadList().getMatchingCount(systemInUsePredicate)>0);
+    }
+    
+    return isDeadlock;
+  }
+  
+  @Override
+  public void terminateProcess (ThreadInfo ti) {
+    SystemState ss = getSystemState();
+    ThreadInfo[] appThreads = getThreadList().getAllMatching(getAppPredicate(ti));
+    ThreadInfo finalizerTi = null;
+
+    for (int i = 0; i < appThreads.length; i++) {
+      ThreadInfo t = appThreads[i];
+      
+      // if finalizers have to be processed, FinalizerThread is not killed at this 
+      // point. We need to keep it around in case fianlizable objects are GCed after 
+      // System.exit() returns.
+      if(processFinalizers && t.isSystemThread()) {
+        finalizerTi = t;
+      } else {
+        // keep the stack frames around, so that we can inspect the snapshot
+        t.setTerminated();
+      }
+    }
+    
+    ThreadList tl = getThreadList();
+    
+    ChoiceGenerator<ThreadInfo> cg;
+    if (tl.hasAnyMatching(getAlivePredicate())) {
+      ThreadInfo[] runnables = getThreadList().getAllMatching(getTimedoutRunnablePredicate());
+      cg = new ThreadChoiceFromSet( "PROCESS_TERMINATE", runnables, true);
+      GlobalSchedulingPoint.setGlobal(cg);
+      
+    } else {
+      cg = new BreakGenerator("exit", ti, true);
+    }
+    
+    ss.setMandatoryNextChoiceGenerator(cg, "exit without break CG");
+    
+    // if there is a finalizer thread, we have to run the last GC, to queue finalizable objects, if any
+    if(finalizerTi != null) {
+      assert finalizerTi.isAlive();
+      activateGC();
+    }
+  }
+  
+  @Override
+  public Map<Integer,IntTable<String>> getInitialInternStringsMap() {
+    Map<Integer,IntTable<String>> interns = new HashMap<Integer,IntTable<String>>();
+     
+    for(ApplicationContext appCtx:getApplicationContexts()) {
+      interns.put(appCtx.getId(), appCtx.getInternStrings());
+    }
+    
+    return interns;
+  }
+  
+  //---------- Predicates used to query threads from ThreadList ----------//
+  
+  abstract class MultiProcessPredicate implements Predicate<ThreadInfo> {
+    ApplicationContext appCtx;
+
+    public void setAppCtx (ApplicationContext appCtx) { 
+      this.appCtx = appCtx; 
+    }
+  }
+  
+  @Override
+  public Predicate<ThreadInfo> getRunnablePredicate() {
+    runnablePredicate.setAppCtx(getCurrentApplicationContext());
+    return runnablePredicate;
+  }
+  
+  @Override
+  public Predicate<ThreadInfo> getAppTimedoutRunnablePredicate() {
+    appTimedoutRunnablePredicate.setAppCtx(getCurrentApplicationContext());
+    return appTimedoutRunnablePredicate;
+  }
+  
+  @Override
+  public Predicate<ThreadInfo> getDaemonRunnablePredicate() {
+    appDaemonRunnablePredicate.setAppCtx(getCurrentApplicationContext());
+    return appDaemonRunnablePredicate;
+  }
+  
+  /**
+   * Returns a predicate used to obtain all the threads that belong to the same application as ti
+   */
+  Predicate<ThreadInfo> getAppPredicate (final ThreadInfo ti){
+    appPredicate.setAppCtx(ti.getApplicationContext());
+    return appPredicate;
+  }
+  
+  // ---------- Methods for handling finalizers ---------- //
+
+  @Override
+  void updateFinalizerQueues () {
+    for(ApplicationContext appCtx: appCtxs) {
+      appCtx.getFinalizerThread().processNewFinalizables();
+    }
+  }
+}