src/main/gov/nasa/jpf/vm/MultiProcessVM.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.JPFConfigException;
  24 import gov.nasa.jpf.util.IntTable;
  25 import gov.nasa.jpf.util.Misc;
  26 import gov.nasa.jpf.util.Predicate;
  27 import gov.nasa.jpf.vm.choice.BreakGenerator;
  28
  29 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
  30 import java.util.ArrayList;
  31 import java.util.HashMap;
  32 import java.util.Map;
  33
  34 /**
  35  * A VM implementation that simulates running multiple applications within the same
  36  * JPF process (centralized model checking of distributed applications).
  37  * This is achieved by executing each application in a separate thread group,
  38  * using separate SystemClassLoader instances to ensure proper separation of types / static fields.
  39  *
  40  *
  41  * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
  42  *
  43  * To use this jpf.properties includes,
  44  *              vm.class = gov.nasa.jpf.vm.MultiProcessVM
  45  */
  46 public class MultiProcessVM extends VM {
  47
  48   static final int MAX_APP = 32;
  49
  50   ApplicationContext[] appCtxs;
  51
  52   MultiProcessPredicate runnablePredicate;
  53   MultiProcessPredicate appTimedoutRunnablePredicate;
  54   MultiProcessPredicate appDaemonRunnablePredicate;
  55   MultiProcessPredicate appPredicate;
  56   protected Predicate<ThreadInfo> systemInUsePredicate;
  57
  58   public MultiProcessVM (JPF jpf, Config conf) {
  59     super(jpf, conf);
  60
  61     appCtxs = createApplicationContexts();
  62
  63     initializePredicates();
  64   }
  65
  66   void initializePredicates() {
  67     runnablePredicate = new MultiProcessPredicate() {
  68       @Override
  69         public boolean isTrue (ThreadInfo t){
  70         return (t.isRunnable() && this.appCtx == t.appCtx);
  71       }
  72     };
  73
  74     appTimedoutRunnablePredicate = new MultiProcessPredicate() {
  75       @Override
  76         public boolean isTrue (ThreadInfo t){
  77         return (this.appCtx == t.appCtx && t.isTimeoutRunnable());
  78       }
  79     };
  80
  81     appDaemonRunnablePredicate = new MultiProcessPredicate() {
  82       @Override
  83         public boolean isTrue (ThreadInfo t){
  84         return (this.appCtx == t.appCtx && t.isRunnable() && t.isDaemon());
  85       }
  86     };
  87
  88     appPredicate = new MultiProcessPredicate() {
  89       @Override
  90         public boolean isTrue (ThreadInfo t){
  91         return (this.appCtx == t.appCtx);
  92       }
  93     };
  94
  95
  96     // this predicates collects those finalizers which are either runnable or
  97     // have some queued objects to process.
  98     systemInUsePredicate = new Predicate<ThreadInfo> () {
  99       @Override
 100         public boolean isTrue (ThreadInfo t){
 101         boolean isTrue = false;
 102         if(t.isSystemThread()) {
 103           if(t.isRunnable()) {
 104             isTrue = true;
 105           } else {
 106             FinalizerThreadInfo finalizer = (FinalizerThreadInfo) t;
 107             isTrue = !finalizer.isIdle();
 108           }
 109         }
 110         return isTrue;
 111       }
 112     };
 113   }
 114
 115   /**
 116    * <2do> this should also handle command line specs such as "jpf ... tgt1 tgt1_arg ... -- tgt2 tgt2_arg ...
 117    */
 118   ApplicationContext[] createApplicationContexts(){
 119     String[] targets;
 120
 121     int replicate = config.getInt("target.replicate", 0);
 122     if(replicate>0) {
 123       String target = config.getProperty("target");
 124       targets = new String[replicate];
 125       for(int i=0; i<replicate; i++) {
 126         targets[i] = target;
 127       }
 128     } else {
 129       targets = config.getStringEnumeration("target", MAX_APP);
 130     }
 131
 132     if (targets == null){
 133       throw new JPFConfigException("no applications specified, check 'target.N' settings");
 134     }
 135
 136     ArrayList<ApplicationContext> list = new ArrayList<ApplicationContext>(targets.length);
 137     for (int i=0; i<targets.length; i++){
 138       if (targets[i] != null){ // there might be holes in the array
 139         String clsName = targets[i];
 140         if (!isValidClassName(clsName)) {
 141           throw new JPFConfigException("main class not a valid class name: " + clsName);
 142         }
 143
 144         String argsKey;
 145         String entryKey;
 146         String hostKey;
 147         if(replicate>0) {
 148           argsKey = "target.args";
 149           entryKey = "target.entry";
 150           hostKey = "target.host";
 151         } else {
 152           argsKey = "target.args." + i;
 153           entryKey = "target.entry." + i;
 154           hostKey = "target.host." + i;
 155         }
 156
 157         String[] args = config.getCompactStringArray(argsKey);
 158         if (args == null){
 159           args = EMPTY_ARGS;
 160         }
 161
 162         String mainEntry = config.getString(entryKey, "main([Ljava/lang/String;)V");
 163
 164         String host = config.getString(hostKey, "localhost");
 165
 166         SystemClassLoaderInfo sysCli = createSystemClassLoaderInfo(list.size());
 167
 168         ApplicationContext appCtx = new ApplicationContext( i, clsName, mainEntry, args, host, sysCli);
 169         list.add( appCtx);
 170       }
 171     }
 172
 173     return list.toArray(new ApplicationContext[list.size()]);
 174   }
 175
 176   @Override
 177   public boolean initialize(){
 178     try {
 179       ThreadInfo tiFirst = null;
 180
 181       for (int i=0; i<appCtxs.length; i++){
 182         ApplicationContext appCtx = appCtxs[i];
 183
 184         // this has to happen before we load the startup classes during initializeMainThread
 185         scheduler.initialize(this, appCtx);
 186
 187         ThreadInfo tiMain = initializeMainThread(appCtx, i);
 188         initializeFinalizerThread(appCtx, appCtxs.length+i);
 189
 190         if (tiMain == null) {
 191           return false; // bail out
 192         }
 193         if (tiFirst == null){
 194           tiFirst = tiMain;
 195         }
 196       }
 197
 198       initSystemState(tiFirst);
 199       initialized = true;
 200       notifyVMInitialized();
 201
 202       return true;
 203
 204     } catch (JPFConfigException cfe){
 205       log.severe(cfe.getMessage());
 206       return false;
 207     } catch (ClassInfoException cie){
 208       log.severe(cie.getMessage());
 209       return false;
 210     }
 211     // all other exceptions are JPF errors that should cause stack traces
 212   }
 213
 214   @Override
 215   public int getNumberOfApplications(){
 216     return appCtxs.length;
 217   }
 218
 219   @Override
 220   public ApplicationContext getApplicationContext(int objRef) {
 221     VM vm = VM.getVM();
 222
 223     ClassInfo ci = vm.getElementInfo(objRef).getClassInfo();
 224     while(!ci.isObjectClassInfo()) {
 225       ci = ci.getSuperClass();
 226     }
 227
 228     ClassLoaderInfo sysLoader = ci.getClassLoaderInfo();
 229     ApplicationContext[] appContext = vm.getApplicationContexts();
 230
 231     for(int i=0; i<appContext.length; i++) {
 232       if(appContext[i].getSystemClassLoader() == sysLoader) {
 233         return appContext[i];
 234       }
 235     }
 236     return null;
 237   }
 238
 239   @Override
 240   public ApplicationContext[] getApplicationContexts(){
 241     return appCtxs;
 242   }
 243
 244   @Override
 245   public ApplicationContext getCurrentApplicationContext(){
 246     ThreadInfo ti = ThreadInfo.getCurrentThread();
 247     if (ti != null){
 248       return ti.getApplicationContext();
 249     } else {
 250       // return the last defined one
 251       return appCtxs[appCtxs.length-1];
 252     }
 253   }
 254
 255
 256   @Override
 257   public String getSUTName() {
 258     StringBuilder sb = new StringBuilder();
 259
 260     for (int i=0; i<appCtxs.length; i++){
 261       if (i>0){
 262         sb.append("+");
 263       }
 264       sb.append(appCtxs[i].mainClassName);
 265     }
 266
 267     return sb.toString();
 268   }
 269
 270   @Override
 271   public String getSUTDescription(){
 272     StringBuilder sb = new StringBuilder();
 273
 274     for (int i=0; i<appCtxs.length; i++){
 275       if (i>0){
 276         sb.append('+'); // "||" would be more fitting, but would screw up filenames
 277       }
 278
 279       ApplicationContext appCtx = appCtxs[i];
 280       sb.append(appCtx.mainClassName);
 281       sb.append('.');
 282       sb.append(Misc.upToFirst(appCtx.mainEntry, '('));
 283
 284       sb.append('(');
 285       String[] args = appCtx.args;
 286       for (int j = 0; j < args.length; j++) {
 287         if (j > 0) {
 288           sb.append(',');
 289         }
 290         sb.append('"');
 291         sb.append(args[j]);
 292         sb.append('"');
 293       }
 294       sb.append(')');
 295     }
 296
 297     return sb.toString();
 298   }
 299
 300
 301   @Override
 302   public boolean isSingleProcess() {
 303     return false;
 304   }
 305
 306   @Override
 307   public boolean isEndState () {
 308     boolean hasNonTerminatedDaemon = getThreadList().hasAnyMatching(getUserLiveNonDaemonPredicate());
 309     boolean hasRunnable = getThreadList().hasAnyMatching(getUserTimedoutRunnablePredicate());
 310     boolean isEndState = !(hasNonTerminatedDaemon && hasRunnable);
 311
 312     if(processFinalizers) {
 313       if(isEndState) {
 314         int n = getThreadList().getMatchingCount(systemInUsePredicate);
 315         if(n>0) {
 316           return false;
 317         }
 318       }
 319     }
 320
 321     return isEndState;
 322   }
 323
 324   @Override
 325   // Note - for now we just check for global deadlocks not the local ones which occur within a
 326   // scope of a single progress
 327   public boolean isDeadlocked () {
 328     boolean hasNonDaemons = false;
 329     boolean hasBlockedThreads = false;
 330
 331     if (ss.isBlockedInAtomicSection()) {
 332       return true; // blocked in atomic section
 333     }
 334
 335     ThreadInfo[] threads = getThreadList().getThreads();
 336     int len = threads.length;
 337
 338     boolean hasUserThreads = false;
 339     for (int i=0; i<len; i++){
 340       ThreadInfo ti = threads[i];
 341
 342       if (ti.isAlive()) {
 343         hasNonDaemons |= !ti.isDaemon();
 344
 345         // shortcut - if there is at least one runnable, we are not deadlocked
 346         if (ti.isTimeoutRunnable()) { // willBeRunnable() ?
 347           return false;
 348         }
 349
 350         if(!ti.isSystemThread()) {
 351           hasUserThreads = true;
 352         }
 353
 354         // means it is not NEW or TERMINATED, i.e. live & blocked
 355         hasBlockedThreads = true;
 356       }
 357     }
 358
 359     boolean isDeadlock = hasNonDaemons && hasBlockedThreads;
 360
 361     if(processFinalizers && isDeadlock && !hasUserThreads) {
 362       // all threads are blocked, system threads. If at least one of them
 363       // is in-use, then this is a deadlocked state.
 364       return (getThreadList().getMatchingCount(systemInUsePredicate)>0);
 365     }
 366
 367     return isDeadlock;
 368   }
 369
 370   @Override
 371   public void terminateProcess (ThreadInfo ti) {
 372     SystemState ss = getSystemState();
 373     ThreadInfo[] appThreads = getThreadList().getAllMatching(getAppPredicate(ti));
 374     ThreadInfo finalizerTi = null;
 375
 376     for (int i = 0; i < appThreads.length; i++) {
 377       ThreadInfo t = appThreads[i];
 378
 379       // if finalizers have to be processed, FinalizerThread is not killed at this
 380       // point. We need to keep it around in case fianlizable objects are GCed after
 381       // System.exit() returns.
 382       if(processFinalizers && t.isSystemThread()) {
 383         finalizerTi = t;
 384       } else {
 385         // keep the stack frames around, so that we can inspect the snapshot
 386         t.setTerminated();
 387       }
 388     }
 389
 390     ThreadList tl = getThreadList();
 391
 392     ChoiceGenerator<ThreadInfo> cg;
 393     if (tl.hasAnyMatching(getAlivePredicate())) {
 394       ThreadInfo[] runnables = getThreadList().getAllMatching(getTimedoutRunnablePredicate());
 395       cg = new ThreadChoiceFromSet( "PROCESS_TERMINATE", runnables, true);
 396       GlobalSchedulingPoint.setGlobal(cg);
 397
 398     } else {
 399       cg = new BreakGenerator("exit", ti, true);
 400     }
 401
 402     ss.setMandatoryNextChoiceGenerator(cg, "exit without break CG");
 403
 404     // if there is a finalizer thread, we have to run the last GC, to queue finalizable objects, if any
 405     if(finalizerTi != null) {
 406       assert finalizerTi.isAlive();
 407       activateGC();
 408     }
 409   }
 410
 411   @Override
 412   public Map<Integer,IntTable<String>> getInitialInternStringsMap() {
 413     Map<Integer,IntTable<String>> interns = new HashMap<Integer,IntTable<String>>();
 414
 415     for(ApplicationContext appCtx:getApplicationContexts()) {
 416       interns.put(appCtx.getId(), appCtx.getInternStrings());
 417     }
 418
 419     return interns;
 420   }
 421
 422   //---------- Predicates used to query threads from ThreadList ----------//
 423
 424   abstract class MultiProcessPredicate implements Predicate<ThreadInfo> {
 425     ApplicationContext appCtx;
 426
 427     public void setAppCtx (ApplicationContext appCtx) {
 428       this.appCtx = appCtx;
 429     }
 430   }
 431
 432   @Override
 433   public Predicate<ThreadInfo> getRunnablePredicate() {
 434     runnablePredicate.setAppCtx(getCurrentApplicationContext());
 435     return runnablePredicate;
 436   }
 437
 438   @Override
 439   public Predicate<ThreadInfo> getAppTimedoutRunnablePredicate() {
 440     appTimedoutRunnablePredicate.setAppCtx(getCurrentApplicationContext());
 441     return appTimedoutRunnablePredicate;
 442   }
 443
 444   @Override
 445   public Predicate<ThreadInfo> getDaemonRunnablePredicate() {
 446     appDaemonRunnablePredicate.setAppCtx(getCurrentApplicationContext());
 447     return appDaemonRunnablePredicate;
 448   }
 449
 450   /**
 451    * Returns a predicate used to obtain all the threads that belong to the same application as ti
 452    */
 453   Predicate<ThreadInfo> getAppPredicate (final ThreadInfo ti){
 454     appPredicate.setAppCtx(ti.getApplicationContext());
 455     return appPredicate;
 456   }
 457
 458   // ---------- Methods for handling finalizers ---------- //
 459
 460   @Override
 461   void updateFinalizerQueues () {
 462     for(ApplicationContext appCtx: appCtxs) {
 463       appCtx.getFinalizerThread().processNewFinalizables();
 464     }
 465   }
 466 }