Renamed master to main and slave to worker throughout

src/main/scala/Silicon.scala

@@ -22,7 +22,7 @@ import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificati
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
-import viper.silicon.verifier.DefaultMasterVerifier
+import viper.silicon.verifier.DefaultMainVerifier
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.logger.ViperStdOutLogger
@@ -104,7 +104,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
   }
 
   private var lifetimeState: LifetimeState = LifetimeState.Instantiated
-  private var verifier: DefaultMasterVerifier = _
+  private var verifier: DefaultMainVerifier = _
 
   private var startTime: Long = _
   private var elapsedMillis: Long = _
@@ -130,7 +130,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     setLogLevelsFromConfig()
 
-    verifier = new DefaultMasterVerifier(config, reporter)
+    verifier = new DefaultMainVerifier(config, reporter)
     verifier.start()
   }
 

src/main/scala/verifier/DefaultMasterVerifier.scala → src/main/scala/verifier/DefaultMainVerifier.scala

@@ -34,19 +34,19 @@ import viper.silver.cfg.silver.SilverCfg
 import viper.silver.reporter.{ConfigurationConfirmation, ExecutionTraceReport, Reporter, VerificationResultMessage, WarningsDuringTypechecking}
 import viper.silver.verifier.TypecheckerWarning
 
-/* TODO: Extract a suitable MasterVerifier interface, probably including
+/* TODO: Extract a suitable MainVerifier interface, probably including
  *         - def verificationPoolManager: VerificationPoolManager)
  *         - def uniqueIdCounter: String)
  */
 
-trait MasterVerifier extends Verifier {
+trait MainVerifier extends Verifier {
   def nextUniqueVerifierId(): String
   def verificationPoolManager: VerificationPoolManager
 }
 
-class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
+class DefaultMainVerifier(config: Config, override val reporter: Reporter)
     extends BaseVerifier(config, "00")
-       with MasterVerifier
+       with MainVerifier
        with DefaultFunctionVerificationUnitProvider
        with DefaultPredicateVerificationUnitProvider {
 

src/main/scala/verifier/VerificationPoolManager.scala

@@ -15,139 +15,139 @@ import viper.silver.components.StatefulComponent
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.state.terms.{Decl, Term}
 
-class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent {
-  private val numberOfSlaveVerifiers: Int = Verifier.config.numberOfParallelVerifiers()
+class VerificationPoolManager(mainVerifier: MainVerifier) extends StatefulComponent {
+  private val numberOfWorkers: Int = Verifier.config.numberOfParallelVerifiers()
 
-  /*private*/ var slaveVerifiers: Seq[SlaveVerifier] = _
-  /*private*/ var slaveVerifierExecutor: ForkJoinPool = _
-  /*private*/ var slaveVerifierPool: ObjectPool[SlaveVerifier] = _
+  /*private*/ var workerVerifiers: Seq[WorkerVerifier] = _
+  /*private*/ var threadPool: ForkJoinPool = _
+  /*private*/ var workerVerifierPool: ObjectPool[WorkerVerifier] = _
 
   private[verifier] object pooledVerifiers extends ProverLike {
-    def emit(content: String): Unit = slaveVerifiers foreach (_.decider.prover.emit(content))
-    override def emit(contents: Iterable[String]): Unit = slaveVerifiers foreach (_.decider.prover.emit(contents))
-    def assume(term: Term): Unit = slaveVerifiers foreach (_.decider.prover.assume(term))
-    def declare(decl: Decl): Unit =  slaveVerifiers foreach (_.decider.prover.declare(decl))
-    def comment(content: String): Unit = slaveVerifiers foreach (_.decider.prover.comment(content))
+    def emit(content: String): Unit = workerVerifiers foreach (_.decider.prover.emit(content))
+    override def emit(contents: Iterable[String]): Unit = workerVerifiers foreach (_.decider.prover.emit(contents))
+    def assume(term: Term): Unit = workerVerifiers foreach (_.decider.prover.assume(term))
+    def declare(decl: Decl): Unit =  workerVerifiers foreach (_.decider.prover.declare(decl))
+    def comment(content: String): Unit = workerVerifiers foreach (_.decider.prover.comment(content))
 
     def saturate(data: Option[Config.ProverStateSaturationTimeout]): Unit =
-      slaveVerifiers foreach (_.decider.prover.saturate(data))
+      workerVerifiers foreach (_.decider.prover.saturate(data))
 
     def saturate(timeout: Int, comment: String): Unit =
-      slaveVerifiers foreach (_.decider.prover.saturate(timeout, comment))
+      workerVerifiers foreach (_.decider.prover.saturate(timeout, comment))
 
     override def emitSettings(contents: Iterable[String]): Unit =
-      slaveVerifiers foreach (_.decider.prover.emitSettings(contents))
+      workerVerifiers foreach (_.decider.prover.emitSettings(contents))
   }
 
   /* Verifier pool management */
 
-  private def setupSlaveVerifierPool(): Unit = {
-    slaveVerifiers = Vector.empty
+  private def setupWorkerPool(): Unit = {
+    workerVerifiers = Vector.empty
 
-    val poolConfig: GenericObjectPoolConfig[SlaveVerifier] = new GenericObjectPoolConfig()
-    poolConfig.setMaxTotal(numberOfSlaveVerifiers)
-    poolConfig.setMaxIdle(numberOfSlaveVerifiers) /* Prevent pool from shutting down idle prover instances */
+    val poolConfig: GenericObjectPoolConfig[WorkerVerifier] = new GenericObjectPoolConfig()
+    poolConfig.setMaxTotal(numberOfWorkers)
+    poolConfig.setMaxIdle(numberOfWorkers) /* Prevent pool from shutting down idle prover instances */
     poolConfig.setBlockWhenExhausted(true)
 
-    val factory = PoolUtils.synchronizedPooledFactory(slaveVerifierPoolableObjectFactory)
+    val factory = PoolUtils.synchronizedPooledFactory(workerVerifierPoolableObjectFactory)
 
-    slaveVerifierPool = new GenericObjectPool[SlaveVerifier](factory, poolConfig)
+    workerVerifierPool = new GenericObjectPool[WorkerVerifier](factory, poolConfig)
 
-    slaveVerifierPool.addObjects(poolConfig.getMaxTotal)
+    workerVerifierPool.addObjects(poolConfig.getMaxTotal)
 
-    assert(slaveVerifiers.length == poolConfig.getMaxTotal)
-    slaveVerifiers foreach (_.start())
+    assert(workerVerifiers.length == poolConfig.getMaxTotal)
+    workerVerifiers foreach (_.start())
 
-    slaveVerifierExecutor = new ForkJoinPool(poolConfig.getMaxTotal, new SlaveBorrowingForkJoinThreadFactory(), null, false)
+    threadPool = new ForkJoinPool(poolConfig.getMaxTotal, new WorkerBorrowingForkJoinThreadFactory(), null, false)
   }
 
-  private def resetSlaveVerifierPool(): Unit = {
-    slaveVerifierExecutor.awaitQuiescence(10, TimeUnit.SECONDS)
-    slaveVerifiers foreach (_.reset())
+  private def resetWorkerPool(): Unit = {
+    threadPool.awaitQuiescence(10, TimeUnit.SECONDS)
+    workerVerifiers foreach (_.reset())
   }
 
-  private def teardownSlaveVerifierPool(): Unit = {
-    if (slaveVerifiers != null) {
-      slaveVerifierExecutor.awaitQuiescence(10, TimeUnit.SECONDS)
-      slaveVerifiers foreach (_.stop())
+  private def teardownWorkerPool(): Unit = {
+    if (workerVerifiers != null) {
+      threadPool.awaitQuiescence(10, TimeUnit.SECONDS)
+      workerVerifiers foreach (_.stop())
 
-      slaveVerifierExecutor.shutdown()
-      slaveVerifierExecutor.awaitTermination(10, TimeUnit.SECONDS)
+      threadPool.shutdown()
+      threadPool.awaitTermination(10, TimeUnit.SECONDS)
     }
 
-    if (slaveVerifierPool != null) {
-      slaveVerifierPool.close()
+    if (workerVerifierPool != null) {
+      workerVerifierPool.close()
     }
   }
 
-  private object slaveVerifierPoolableObjectFactory extends BasePooledObjectFactory[SlaveVerifier] {
-    def create(): SlaveVerifier = {
-      val slave = new SlaveVerifier(master, master.nextUniqueVerifierId(), master.reporter)
-      slaveVerifiers = slave +: slaveVerifiers
+  private object workerVerifierPoolableObjectFactory extends BasePooledObjectFactory[WorkerVerifier] {
+    def create(): WorkerVerifier = {
+      val worker = new WorkerVerifier(mainVerifier, mainVerifier.nextUniqueVerifierId(), mainVerifier.reporter)
+      workerVerifiers = worker +: workerVerifiers
 
-      slave
+      worker
     }
 
-    def wrap(arg: SlaveVerifier): PooledObject[SlaveVerifier] = new DefaultPooledObject(arg)
+    def wrap(arg: WorkerVerifier): PooledObject[WorkerVerifier] = new DefaultPooledObject(arg)
   }
 
   /* Verification task management */
 
 
-  def queueVerificationTask(task: SlaveVerifier => Seq[VerificationResult])
+  def queueVerificationTask(task: WorkerVerifier => Seq[VerificationResult])
                            : Future[Seq[VerificationResult]] = {
     val thread = Thread.currentThread()
-    if (thread.isInstanceOf[SlaveBorrowingForkJoinWorkerThread]){
-      new SlaveAwareForkJoinTask(task).fork
+    if (thread.isInstanceOf[WorkerBorrowingForkJoinWorkerThread]){
+      new WorkerAwareForkJoinTask(task).fork
     }else{
-      slaveVerifierExecutor.submit(new SlaveAwareForkJoinTask(task))
+      threadPool.submit(new WorkerAwareForkJoinTask(task))
     }
   }
 
   /* Lifetime */
 
   def start(): Unit = {
-    setupSlaveVerifierPool()
+    setupWorkerPool()
   }
 
   def reset(): Unit = {
-    resetSlaveVerifierPool()
+    resetWorkerPool()
   }
 
   def stop(): Unit = {
-    teardownSlaveVerifierPool()
+    teardownWorkerPool()
   }
 
-  class SlaveBorrowingForkJoinThreadFactory extends ForkJoinPool.ForkJoinWorkerThreadFactory {
+  class WorkerBorrowingForkJoinThreadFactory extends ForkJoinPool.ForkJoinWorkerThreadFactory {
     override def newThread(forkJoinPool: ForkJoinPool): ForkJoinWorkerThread = {
-      new SlaveBorrowingForkJoinWorkerThread(forkJoinPool)
+      new WorkerBorrowingForkJoinWorkerThread(forkJoinPool)
     }
   }
 
-  class SlaveBorrowingForkJoinWorkerThread(pool: ForkJoinPool) extends ForkJoinWorkerThread(pool) {
-    // each thread has its own slave verifier that does not change.
-    var slave: SlaveVerifier = null
+  class WorkerBorrowingForkJoinWorkerThread(pool: ForkJoinPool) extends ForkJoinWorkerThread(pool) {
+    // each thread has its own worker verifier that does not change.
+    var worker: WorkerVerifier = null
 
     override def onStart(): Unit = {
-      slave = slaveVerifierPool.borrowObject()
+      worker = workerVerifierPool.borrowObject()
     }
 
     override def onTermination(exception: Throwable): Unit = {
-      if (slave != null) {
-        slaveVerifierPool.returnObject(slave)
+      if (worker != null) {
+        workerVerifierPool.returnObject(worker)
       }
     }
 
   }
 
-  class SlaveAwareForkJoinTask(task: SlaveVerifier => Seq[VerificationResult])
+  class WorkerAwareForkJoinTask(task: WorkerVerifier => Seq[VerificationResult])
     extends RecursiveTask[Seq[VerificationResult]]{
 
     override def compute(): Seq[VerificationResult] = {
-      // get the slave verifier of the current thread
-      val worker = Thread.currentThread().asInstanceOf[SlaveBorrowingForkJoinWorkerThread]
-      val slave = worker.slave
-      task(slave)
+      // get the worker verifier of the current thread
+      val workerThread = Thread.currentThread().asInstanceOf[WorkerBorrowingForkJoinWorkerThread]
+      val workerVerifier = workerThread.worker
+      task(workerVerifier)
     }
   }
 }

src/main/scala/verifier/SlaveVerifier.scala → src/main/scala/verifier/WorkerVerifier.scala

@@ -10,9 +10,9 @@ import viper.silicon.supporters._
 import viper.silver.components.StatefulComponent
 import viper.silver.reporter.Reporter
 
-class SlaveVerifier(master: MasterVerifier,
-                    uniqueId: String,
-                    override val reporter: Reporter)
+class WorkerVerifier(mainVerifier: MainVerifier,
+                     uniqueId: String,
+                     override val reporter: Reporter)
     extends BaseVerifier(Verifier.config, uniqueId)
        with DefaultMethodVerificationUnitProvider
        with DefaultCfgVerificationUnitProvider {
@@ -22,7 +22,7 @@ class SlaveVerifier(master: MasterVerifier,
     cfgSupporter
   )
 
-  def verificationPoolManager: VerificationPoolManager = master.verificationPoolManager
+  def verificationPoolManager: VerificationPoolManager = mainVerifier.verificationPoolManager
 
   /* Lifetime */
 

utils/patches/programmatically-change-logback-pattern.diff

@@ -16,7 +16,7 @@ diff -r 19832d947290 src/main/scala/Silicon.scala
 
 -    setLogLevelsFromConfig()
 -
-     verifier = new DefaultMasterVerifier(config)
+     verifier = new DefaultMainVerifier(config)
      verifier.start()
    }
 @@ -304,9 +304,14 @@