Welcome to GMC

Multi-Core Model Checking

Stateful classes in CIVL that may not be necessary to be stateful:

edu.udel.cis.vsl.civl.kripke.semantics.CommonEvaluator.java
boundVariableStack
originalState
originalPid
valueAtOrRemoteCount
Possible solution: spawn an EvaluatorWorker

edu.udel.cis.vsl.civl.semantics.common.CommonExecutor.java
numSteps
Possible solution: Each thread has its own copy of Executor.

edu.udel.cis.vsl.civl.kripke.common.CommonStateManager.java
maxProcs
maxCanonicId
numStatesExplored
stack
expandedStateIDs

edu.udel.cis.vsl.civl.state.common.immutable.ImmutableStateFactory.java
processMap
scopeMap
stateCount
stateMap
savedCanonicStates
dyscopeSubMap

edu.udel.cis.vsl.sarl.object.common.CommonObjectFactory.java
objectMap
objectList

edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.java
validCount
proverValidCount
int2bvConstants

edu.udel.cis.vsl.civl.model.common.CommonModelFactory.java
processValues
scopeValues

edu.udel.cis.vsl.civl.semantics.common.UFExtender.java
Possible Solution:Initialize the field uninterpretedFunctions exactly once in constructor with all known abstract functions and never change again.

edu.udel.cis.vsl.civl.kripke.common.OutputCollector.java

/CIVL/src/edu/udel/cis/vsl/civl/model/common/type/CommonType.java
dynamicType

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/CommonReasoner.java
prover
validityCache

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/SimpleReasoner.java
validityCache

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonExecutor.java ? (setValue, setLocation)
stateFactory

/CIVL/src/edu/udel/cis/vsl/civl/state/common/immutable/ImmutableState.java (can be removed)
snapshotsQueues

/SARL/src/edu/udel/cis/vsl/sarl/number/real/RealNumberFactory.java
integerMap
rationalMap

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/CommonReasonerFactory.java
reasonerCache

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/ContextMinimizingReasonerFactory.java
reasonerMap

/SARL/src/edu/udel/cis/vsl/sarl/ideal/simplify/IdealSimplifier.java
fullContext
substitutionMap

/SARL/src/edu/udel/cis/vsl/sarl/preuniverse/common/ExpressionSubstituter.java
cache

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/ContextMinimizingReasoner.java
validityCache
prover

/GMC/src/edu/udel/cis/vsl/gmc/ErrorLog.java
minimalCounterexampleSize
entryMap
searchTruncated

/SARL/src/edu/udel/cis/vsl/sarl/simplify/common/CommonContextPartition.java
minimalContextMap

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonLibraryExecutorLoader.java
libraryExecutorCache

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonLibraryEvaluatorLoader.java
libraryEvaluatorCache

/CIVL/src/edu/udel/cis/vsl/civl/dynamic/common/CommonSymbolicUtility.java
typeExpressionMap
typeExpressionMap2

/CIVL/src/edu/udel/cis/vsl/civl/kripke/common/CommonLibraryEnablerLoader.java
libraryEnablerCache