From f2fe1e0dd0a58e0cfb9ce055dc2f88dcfc7d7ce0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 19 Sep 2022 23:02:15 +0200 Subject: [PATCH] Renamed master to main and slave to worker throughout --- src/main/scala/Silicon.scala | 6 +- ...rifier.scala => DefaultMainVerifier.scala} | 8 +- .../verifier/VerificationPoolManager.scala | 122 +++++++++--------- ...aveVerifier.scala => WorkerVerifier.scala} | 8 +- ...ogrammatically-change-logback-pattern.diff | 2 +- 5 files changed, 73 insertions(+), 73 deletions(-) rename src/main/scala/verifier/{DefaultMasterVerifier.scala => DefaultMainVerifier.scala} (98%) rename src/main/scala/verifier/{SlaveVerifier.scala => WorkerVerifier.scala} (80%) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index 60fc38447..2a5867bb2 100644 --- a/src/main/scala/Silicon.scala +++ b/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() } diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala similarity index 98% rename from src/main/scala/verifier/DefaultMasterVerifier.scala rename to src/main/scala/verifier/DefaultMainVerifier.scala index 56de055cd..e38d5e744 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/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 { diff --git a/src/main/scala/verifier/VerificationPoolManager.scala b/src/main/scala/verifier/VerificationPoolManager.scala index 57ee41bc2..f5ca7e5e5 100644 --- a/src/main/scala/verifier/VerificationPoolManager.scala +++ b/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) } } } diff --git a/src/main/scala/verifier/SlaveVerifier.scala b/src/main/scala/verifier/WorkerVerifier.scala similarity index 80% rename from src/main/scala/verifier/SlaveVerifier.scala rename to src/main/scala/verifier/WorkerVerifier.scala index 629e3d42b..a36b4a0af 100644 --- a/src/main/scala/verifier/SlaveVerifier.scala +++ b/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 */ diff --git a/utils/patches/programmatically-change-logback-pattern.diff b/utils/patches/programmatically-change-logback-pattern.diff index 8d1426ae7..bf405fe25 100644 --- a/utils/patches/programmatically-change-logback-pattern.diff +++ b/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 @@