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.model.common.ModelBuilderWorker.java
hasNextTimeCountCall?
parProcFunctions
runProcFunctions
bundleableEncountered
bundleableTypeList
callStatements
callEvents
functionMap
handledObjectTypes

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