gov.nasa.jpf.vm

Class MultiProcessVM

java.lang.Object

gov.nasa.jpf.vm.VM

gov.nasa.jpf.vm.MultiProcessVM

public class MultiProcessVM
extends VM

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.

Field Summary

Fields

Modifier and Type	Field and Description
protected Predicate<ThreadInfo>	systemInUsePredicate

Fields inherited from class gov.nasa.jpf.vm.VM

alivePredicate, backtracker, CHECK_CONSISTENCY, config, EMPTY_ARGS, error_id, funcObjFactory, indentOutput, initialized, isBigEndian, isTraceReplay, jpf, lastTrailInfo, listeners, log, newStateId, out, path, pathOutput, postGcActions, processFinalizers, restorer, runGc, scheduler, serializer, ss, stateSet, timedoutRunnablePredicate, timeModel, transitionOccurred, treeOutput, userliveNonDaemonPredicate, userTimedoutRunnablePredicate, vm

Constructor Summary

Constructors

Constructor and Description
MultiProcessVM(JPF jpf, Config conf)

Method Summary

Modifier and Type	Method and Description
ApplicationContext	getApplicationContext(int objRef)
ApplicationContext[]	getApplicationContexts()
Predicate<ThreadInfo>	getAppTimedoutRunnablePredicate()
ApplicationContext	getCurrentApplicationContext() given an object reference, it returns the ApplicationContext of the process to which this object belongs
Predicate<ThreadInfo>	getDaemonRunnablePredicate()
java.util.Map<java.lang.Integer,IntTable<java.lang.String>>	getInitialInternStringsMap()
int	getNumberOfApplications()
Predicate<ThreadInfo>	getRunnablePredicate()
java.lang.String	getSUTDescription()
java.lang.String	getSUTName()
boolean	initialize() this is the main initialization point that sets up startup objects threads and callstacks.
boolean	isDeadlocked()
boolean	isEndState() We made this to be overriden by Single/MultiprcessesVM implementations, since for MultiprcessesVM one can decide when to terminate (after the the termination of all processes or only one process).
boolean	isSingleProcess()
void	terminateProcess(ThreadInfo ti)

Methods inherited from class gov.nasa.jpf.vm.VM

activateGC, addListener, addPostGcAction, backtrack, breakTransition, checkConsistency, cleanUp, createFinalizerThreadInfo, createMainThreadInfo, createSystemClassLoaderInfo, createSystemClassLoaderObject, createThreadInfo, currentTimeMillis, dumpThreadStates, finalizersEnabled, forceState, forward, getAlivePredicate, getBacktracker, getChoiceGenerator, getChoiceGenerators, getChoiceGeneratorsOfType, getClassInfo, getClassLoader, getClassLoaderList, getClonedPath, getConfig, getCurrentChoiceGenerator, getCurrentThread, getCurrentTransition, getElementInfo, getException, getFinalizerThread, getFunctionObjectFacotry, getHeap, getInstruction, getJPF, getKernelState, getLastChoiceGeneratorInThread, getLastChoiceGeneratorOfType, getLastStep, getLastTransition, getLiveThreads, getMainClassInfo, getMainEntryMethodInfo, getModifiableElementInfo, getNextChoiceGenerator, getNextListenerOfType, getPath, getPathLength, getPendingException, getPendingOutput, getPlatformEndianness, getRestorableState, getRestorer, getScheduler, getSearch, getSerializer, getStartupSystemClassInfos, getStartupSystemClassNames, getStateCount, getStateId, getStateSet, getSystemState, getThreadList, getThreadName, getTimedoutRunnablePredicate, getUserLiveNonDaemonPredicate, getUserTimedoutRunnablePredicate, getVM, handleException, hasListenerOfType, hasNextChoiceGenerator, hasPendingException, hasToRecordPathOutput, hasToRecordSteps, ignoreState, ignoreState, initFields, initializeFinalizerThread, initializeMainThread, initSubsystems, initSystemState, initTimeModel, isBigEndianPlatform, isBoringState, isIgnoredState, isInitialized, isInterestingState, isNewState, isTraceReplay, isVisitedState, kernelStateChanged, nanoTime, notifyChoiceGeneratorAdvanced, notifyChoiceGeneratorProcessed, notifyChoiceGeneratorRegistered, notifyChoiceGeneratorSet, notifyClassLoaded, notifyExceptionBailout, notifyExceptionHandled, notifyExceptionThrown, notifyExecuteInstruction, notifyGCBegin, notifyGCEnd, notifyInstructionExecuted, notifyLoadClass, notifyMethodEntered, notifyMethodExited, notifyObjectCreated, notifyObjectExposed, notifyObjectLocked, notifyObjectNotifies, notifyObjectNotifiesAll, notifyObjectReleased, notifyObjectShared, notifyObjectUnlocked, notifyObjectWait, notifyThreadBlocked, notifyThreadInterrupted, notifyThreadNotified, notifyThreadScheduled, notifyThreadStarted, notifyThreadTerminated, notifyThreadWaiting, notifyVMInitialized, print, print, print, print, print, print, print, printChoiceGeneratorStack, printCurrentStackTrace, printLiveThreadStatus, println, println, processFinalizers, processPostGcActions, pushClinits, pushMainEntry, pushMainEntryArgs, recordSteps, registerClassLoader, registerThread, registerThreadListCleanup, removeListener, resetNextCG, restoreState, retainStateAttributes, setMandatoryNextChoiceGenerator, setNextChoiceGenerator, setRootCG, setSerializer, setTraceReplay, storePathOutput, storeTrace, transitionOccurred, updatePath

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

systemInUsePredicate

protected Predicate<ThreadInfo> systemInUsePredicate

Constructor Detail

MultiProcessVM

public MultiProcessVM(JPF jpf,
                      Config conf)

Method Detail

initialize

public boolean initialize()

Description copied from class: VM

this is the main initialization point that sets up startup objects threads and callstacks. If this returns false VM initialization cannot proceed and JPF will terminate

Specified by:

initialize in class VM

getNumberOfApplications

public int getNumberOfApplications()

Specified by:

getNumberOfApplications in class VM

getApplicationContext

public ApplicationContext getApplicationContext(int objRef)

Specified by:

getApplicationContext in class VM

getApplicationContexts

public ApplicationContext[] getApplicationContexts()

Specified by:

getApplicationContexts in class VM

getCurrentApplicationContext

public ApplicationContext getCurrentApplicationContext()

Description copied from class: VM

given an object reference, it returns the ApplicationContext of the process to which this object belongs

Specified by:

getCurrentApplicationContext in class VM

getSUTName

public java.lang.String getSUTName()

Specified by:

getSUTName in class VM

getSUTDescription

public java.lang.String getSUTDescription()

Specified by:

getSUTDescription in class VM

isSingleProcess

public boolean isSingleProcess()

Overrides:

isSingleProcess in class VM

isEndState

public boolean isEndState()

Description copied from class: VM

We made this to be overriden by Single/MultiprcessesVM implementations, since for MultiprcessesVM one can decide when to terminate (after the the termination of all processes or only one process). todo - that needs to be specified through the properties file

Specified by:

isEndState in class VM

isDeadlocked

public boolean isDeadlocked()

Specified by:

isDeadlocked in class VM

terminateProcess

public void terminateProcess(ThreadInfo ti)

Specified by:

terminateProcess in class VM

getInitialInternStringsMap

public java.util.Map<java.lang.Integer,IntTable<java.lang.String>> getInitialInternStringsMap()

Specified by:

getInitialInternStringsMap in class VM

getRunnablePredicate

public Predicate<ThreadInfo> getRunnablePredicate()

Specified by:

getRunnablePredicate in class VM

getAppTimedoutRunnablePredicate

public Predicate<ThreadInfo> getAppTimedoutRunnablePredicate()

Specified by:

getAppTimedoutRunnablePredicate in class VM

getDaemonRunnablePredicate

public Predicate<ThreadInfo> getDaemonRunnablePredicate()

Specified by:

getDaemonRunnablePredicate in class VM