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.

Author:

Nastaran Shafiei To use this jpf.properties includes, vm.class = gov.nasa.jpf.vm.MultiProcessVM

Field Summary

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

backtracker, CHECK_CONSISTENCY, config, EMPTY_ARGS, error_id, indentOutput, initialized, isBigEndian, isTraceReplay, lastTrailInfo, listeners, log, newStateId, out, path, pathOutput, postGcActions, restorer, runGc, serializer, ss, stateSet, timeModel, transitionOccurred, treeOutput, vm

Constructor Summary

Constructors

Constructor and Description
MultiProcessVM(JPF jpf, Config conf)

Method Summary

Methods

Modifier and Type	Method and Description
ApplicationContext	getApplicationContext(int objRef) given an object reference, it returns the ApplicationContext of the process to which this object belongs
ApplicationContext[]	getApplicationContexts()
ThreadInfo[]	getAppThreads(ThreadInfo ti) Returns all the threads that belong to the same application as ti
int	getNumberOfApplications()
int	getRunnableAppThreadCount(ThreadInfo ti)
ThreadInfo[]	getRunnableAppThreads(ThreadInfo ti)
ThreadInfo[]	getRunnableAppThreadsWith(ThreadInfo ti)
ThreadInfo[]	getRunnableAppThreadsWithout(ThreadInfo ti)
String	getSUTDescription()
String	getSUTName()
boolean	hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti)
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()

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

activateGC, addListener, addPostGcAction, backtrack, breakTransition, checkConsistency, cleanUp, createMainThreadGroup, createMainThreadInfo, createMainThreadObject, createSystemClassLoaderInfo, createSystemClassLoaderObject, createThreadInfo, currentTimeMillis, dumpThreadStates, forceState, forward, getAliveThreadCount, getBacktracker, getChoiceGenerator, getChoiceGenerators, getChoiceGeneratorsOfType, getClassInfo, getClassLoader, getClassLoaderList, getClonedPath, getConfig, getCurrentChoiceGenerator, getCurrentThread, getCurrentTransition, getElementInfo, getException, getHeap, getInstruction, getJPF, getKernelState, getLastChoiceGeneratorOfType, getLastStep, getLastTransition, getLiveThreads, getMainClassInfo, getMainEntryMethodInfo, getModifiableElementInfo, getNextChoiceGenerator, getNextListenerOfType, getPath, getPathLength, getPendingException, getPendingOutput, getPlatformEndianness, getRestorableState, getRestorer, getRunnableThreadCount, getSchedulerFactory, getSerializer, getStartupSystemClassInfos, getStartupSystemClassNames, getStateCount, getStateId, getStateSet, getSystemState, getThreadList, getThreadName, getVM, handleException, hasListenerOfType, hasOtherNonDaemonRunnablesThan, hasOtherRunnablesThan, hasPendingException, hasToRecordPathOutput, hasToRecordSteps, ignoreState, ignoreState, initFields, initializeMainThread, initSubsystems, initSystemState, initTimeModel, isAtomic, 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, notifyObjectLocked, notifyObjectNotifies, notifyObjectNotifiesAll, notifyObjectReleased, notifyObjectUnlocked, notifyObjectWait, notifyThreadBlocked, notifyThreadInterrupted, notifyThreadNotified, notifyThreadScheduled, notifyThreadStarted, notifyThreadTerminated, notifyThreadWaiting, notifyVMInitialized, print, print, print, print, print, print, print, printCurrentStackTrace, printLiveThreadStatus, println, println, processPostGcActions, pushClinits, pushMainEntry, pushMainEntryArgs, recordSteps, registerClassLoader, registerThread, registerThreadListCleanup, removeListener, resetNextCG, restoreState, retainStateAttributes, setMandatoryNextChoiceGenerator, setNextChoiceGenerator, setSerializer, setTraceReplay, storePathOutput, storeTrace, transitionOccurred, updatePath

Methods inherited from class java.lang.Object

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

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)

Description copied from class: VM

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

Specified by:

getApplicationContext in class VM

getApplicationContexts

public ApplicationContext[] getApplicationContexts()

Specified by:

getApplicationContexts in class VM

getSUTName

public String getSUTName()

Specified by:

getSUTName in class VM

getSUTDescription

public 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

hasOnlyDaemonRunnablesOtherThan

public boolean hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti)

Specified by:

hasOnlyDaemonRunnablesOtherThan in class VM

getAppThreads

public ThreadInfo[] getAppThreads(ThreadInfo ti)

Returns all the threads that belong to the same application as ti

getRunnableAppThreads

public ThreadInfo[] getRunnableAppThreads(ThreadInfo ti)

getRunnableAppThreadCount

public int getRunnableAppThreadCount(ThreadInfo ti)

getRunnableAppThreadsWith

public ThreadInfo[] getRunnableAppThreadsWith(ThreadInfo ti)

getRunnableAppThreadsWithout

public ThreadInfo[] getRunnableAppThreadsWithout(ThreadInfo ti)