2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
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;
29 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
30 import java.util.ArrayList;
31 import java.util.HashMap;
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.
41 * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
43 * To use this jpf.properties includes,
44 * vm.class = gov.nasa.jpf.vm.MultiProcessVM
46 public class MultiProcessVM extends VM {
48 static final int MAX_APP = 32;
50 ApplicationContext[] appCtxs;
52 MultiProcessPredicate runnablePredicate;
53 MultiProcessPredicate appTimedoutRunnablePredicate;
54 MultiProcessPredicate appDaemonRunnablePredicate;
55 MultiProcessPredicate appPredicate;
56 protected Predicate<ThreadInfo> systemInUsePredicate;
58 public MultiProcessVM (JPF jpf, Config conf) {
61 appCtxs = createApplicationContexts();
63 initializePredicates();
66 void initializePredicates() {
67 runnablePredicate = new MultiProcessPredicate() {
69 public boolean isTrue (ThreadInfo t){
70 return (t.isRunnable() && this.appCtx == t.appCtx);
74 appTimedoutRunnablePredicate = new MultiProcessPredicate() {
76 public boolean isTrue (ThreadInfo t){
77 return (this.appCtx == t.appCtx && t.isTimeoutRunnable());
81 appDaemonRunnablePredicate = new MultiProcessPredicate() {
83 public boolean isTrue (ThreadInfo t){
84 return (this.appCtx == t.appCtx && t.isRunnable() && t.isDaemon());
88 appPredicate = new MultiProcessPredicate() {
90 public boolean isTrue (ThreadInfo t){
91 return (this.appCtx == t.appCtx);
96 // this predicates collects those finalizers which are either runnable or
97 // have some queued objects to process.
98 systemInUsePredicate = new Predicate<ThreadInfo> () {
100 public boolean isTrue (ThreadInfo t){
101 boolean isTrue = false;
102 if(t.isSystemThread()) {
106 FinalizerThreadInfo finalizer = (FinalizerThreadInfo) t;
107 isTrue = !finalizer.isIdle();
116 * <2do> this should also handle command line specs such as "jpf ... tgt1 tgt1_arg ... -- tgt2 tgt2_arg ...
118 ApplicationContext[] createApplicationContexts(){
121 int replicate = config.getInt("target.replicate", 0);
123 String target = config.getProperty("target");
124 targets = new String[replicate];
125 for(int i=0; i<replicate; i++) {
129 targets = config.getStringEnumeration("target", MAX_APP);
132 if (targets == null){
133 throw new JPFConfigException("no applications specified, check 'target.N' settings");
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);
148 argsKey = "target.args";
149 entryKey = "target.entry";
150 hostKey = "target.host";
152 argsKey = "target.args." + i;
153 entryKey = "target.entry." + i;
154 hostKey = "target.host." + i;
157 String[] args = config.getCompactStringArray(argsKey);
162 String mainEntry = config.getString(entryKey, "main([Ljava/lang/String;)V");
164 String host = config.getString(hostKey, "localhost");
166 SystemClassLoaderInfo sysCli = createSystemClassLoaderInfo(list.size());
168 ApplicationContext appCtx = new ApplicationContext( i, clsName, mainEntry, args, host, sysCli);
173 return list.toArray(new ApplicationContext[list.size()]);
177 public boolean initialize(){
179 ThreadInfo tiFirst = null;
181 for (int i=0; i<appCtxs.length; i++){
182 ApplicationContext appCtx = appCtxs[i];
184 // this has to happen before we load the startup classes during initializeMainThread
185 scheduler.initialize(this, appCtx);
187 ThreadInfo tiMain = initializeMainThread(appCtx, i);
188 initializeFinalizerThread(appCtx, appCtxs.length+i);
190 if (tiMain == null) {
191 return false; // bail out
193 if (tiFirst == null){
198 initSystemState(tiFirst);
200 notifyVMInitialized();
204 } catch (JPFConfigException cfe){
205 log.severe(cfe.getMessage());
207 } catch (ClassInfoException cie){
208 log.severe(cie.getMessage());
211 // all other exceptions are JPF errors that should cause stack traces
215 public int getNumberOfApplications(){
216 return appCtxs.length;
220 public ApplicationContext getApplicationContext(int objRef) {
223 ClassInfo ci = vm.getElementInfo(objRef).getClassInfo();
224 while(!ci.isObjectClassInfo()) {
225 ci = ci.getSuperClass();
228 ClassLoaderInfo sysLoader = ci.getClassLoaderInfo();
229 ApplicationContext[] appContext = vm.getApplicationContexts();
231 for(int i=0; i<appContext.length; i++) {
232 if(appContext[i].getSystemClassLoader() == sysLoader) {
233 return appContext[i];
240 public ApplicationContext[] getApplicationContexts(){
245 public ApplicationContext getCurrentApplicationContext(){
246 ThreadInfo ti = ThreadInfo.getCurrentThread();
248 return ti.getApplicationContext();
250 // return the last defined one
251 return appCtxs[appCtxs.length-1];
257 public String getSUTName() {
258 StringBuilder sb = new StringBuilder();
260 for (int i=0; i<appCtxs.length; i++){
264 sb.append(appCtxs[i].mainClassName);
267 return sb.toString();
271 public String getSUTDescription(){
272 StringBuilder sb = new StringBuilder();
274 for (int i=0; i<appCtxs.length; i++){
276 sb.append('+'); // "||" would be more fitting, but would screw up filenames
279 ApplicationContext appCtx = appCtxs[i];
280 sb.append(appCtx.mainClassName);
282 sb.append(Misc.upToFirst(appCtx.mainEntry, '('));
285 String[] args = appCtx.args;
286 for (int j = 0; j < args.length; j++) {
297 return sb.toString();
302 public boolean isSingleProcess() {
307 public boolean isEndState () {
308 boolean hasNonTerminatedDaemon = getThreadList().hasAnyMatching(getUserLiveNonDaemonPredicate());
309 boolean hasRunnable = getThreadList().hasAnyMatching(getUserTimedoutRunnablePredicate());
310 boolean isEndState = !(hasNonTerminatedDaemon && hasRunnable);
312 if(processFinalizers) {
314 int n = getThreadList().getMatchingCount(systemInUsePredicate);
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;
331 if (ss.isBlockedInAtomicSection()) {
332 return true; // blocked in atomic section
335 ThreadInfo[] threads = getThreadList().getThreads();
336 int len = threads.length;
338 boolean hasUserThreads = false;
339 for (int i=0; i<len; i++){
340 ThreadInfo ti = threads[i];
343 hasNonDaemons |= !ti.isDaemon();
345 // shortcut - if there is at least one runnable, we are not deadlocked
346 if (ti.isTimeoutRunnable()) { // willBeRunnable() ?
350 if(!ti.isSystemThread()) {
351 hasUserThreads = true;
354 // means it is not NEW or TERMINATED, i.e. live & blocked
355 hasBlockedThreads = true;
359 boolean isDeadlock = hasNonDaemons && hasBlockedThreads;
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);
371 public void terminateProcess (ThreadInfo ti) {
372 SystemState ss = getSystemState();
373 ThreadInfo[] appThreads = getThreadList().getAllMatching(getAppPredicate(ti));
374 ThreadInfo finalizerTi = null;
376 for (int i = 0; i < appThreads.length; i++) {
377 ThreadInfo t = appThreads[i];
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()) {
385 // keep the stack frames around, so that we can inspect the snapshot
390 ThreadList tl = getThreadList();
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);
399 cg = new BreakGenerator("exit", ti, true);
402 ss.setMandatoryNextChoiceGenerator(cg, "exit without break CG");
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();
412 public Map<Integer,IntTable<String>> getInitialInternStringsMap() {
413 Map<Integer,IntTable<String>> interns = new HashMap<Integer,IntTable<String>>();
415 for(ApplicationContext appCtx:getApplicationContexts()) {
416 interns.put(appCtx.getId(), appCtx.getInternStrings());
422 //---------- Predicates used to query threads from ThreadList ----------//
424 abstract class MultiProcessPredicate implements Predicate<ThreadInfo> {
425 ApplicationContext appCtx;
427 public void setAppCtx (ApplicationContext appCtx) {
428 this.appCtx = appCtx;
433 public Predicate<ThreadInfo> getRunnablePredicate() {
434 runnablePredicate.setAppCtx(getCurrentApplicationContext());
435 return runnablePredicate;
439 public Predicate<ThreadInfo> getAppTimedoutRunnablePredicate() {
440 appTimedoutRunnablePredicate.setAppCtx(getCurrentApplicationContext());
441 return appTimedoutRunnablePredicate;
445 public Predicate<ThreadInfo> getDaemonRunnablePredicate() {
446 appDaemonRunnablePredicate.setAppCtx(getCurrentApplicationContext());
447 return appDaemonRunnablePredicate;
451 * Returns a predicate used to obtain all the threads that belong to the same application as ti
453 Predicate<ThreadInfo> getAppPredicate (final ThreadInfo ti){
454 appPredicate.setAppCtx(ti.getApplicationContext());
458 // ---------- Methods for handling finalizers ---------- //
461 void updateFinalizerQueues () {
462 for(ApplicationContext appCtx: appCtxs) {
463 appCtx.getFinalizerThread().processNewFinalizables();