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.common.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.