From b3b6d9c54ed3b08ca813965322241c21a99cb1c4 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 5 May 2026 18:20:50 +0200 Subject: [PATCH 01/22] Replace scheduling ActorSystems with ScheduledExecutorService --- .../core/VerificationExecutionContext.scala | 14 +++++++++++++- .../viper/server/frontends/lsp/Receiver.scala | 13 ++++++++----- .../frontends/lsp/file/QuantifierCodeLens.scala | 11 +++++------ .../frontends/lsp/file/Verification.scala | 17 +++++++++-------- 4 files changed, 35 insertions(+), 20 deletions(-) diff --git a/src/main/scala/viper/server/core/VerificationExecutionContext.scala b/src/main/scala/viper/server/core/VerificationExecutionContext.scala index abdc7bce..b7e9b0f7 100644 --- a/src/main/scala/viper/server/core/VerificationExecutionContext.scala +++ b/src/main/scala/viper/server/core/VerificationExecutionContext.scala @@ -6,7 +6,7 @@ package viper.server.core -import java.util.concurrent.{ExecutorService, Executors, ThreadFactory, TimeUnit} +import java.util.concurrent.{ExecutorService, Executors, ScheduledExecutorService, ThreadFactory, TimeUnit} import java.util.{concurrent => java_concurrent} import akka.actor.ActorSystem @@ -17,6 +17,7 @@ import scala.concurrent.{Await, ExecutionContext, ExecutionContextExecutorServic trait VerificationExecutionContext extends ExecutionContext { def executorService: ExecutorService def actorSystem: ActorSystem + def scheduler: ScheduledExecutorService def submit(r: Runnable): java_concurrent.Future[_] /** terminate executor and actor system */ def terminate(timeoutMSec: Long = 1000): Unit @@ -62,6 +63,16 @@ class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_Syste }) override def executorService: ExecutorService = service + private lazy val schedulerService: ScheduledExecutorService = Executors.newSingleThreadScheduledExecutor(new ThreadFactory { + private val mCount = new java.util.concurrent.atomic.AtomicInteger(1) + override def newThread(runnable: Runnable): Thread = { + val t = new Thread(runnable, s"$threadNamePrefix-scheduler-${mCount.getAndIncrement()}") + t.setDaemon(true) + t + } + }) + override def scheduler: ScheduledExecutorService = schedulerService + private lazy val context: ExecutionContextExecutorService = ExecutionContext.fromExecutorService(executorService) override def execute(runnable: Runnable): Unit = context.execute(runnable) @@ -78,6 +89,7 @@ class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_Syste val oldSystem = actorSystem system = None Await.ready(oldSystem.terminate(), FiniteDuration(timeoutMSec, TimeUnit.MILLISECONDS)) + schedulerService.shutdownNow() executorService.shutdown() executorService.awaitTermination(timeoutMSec, TimeUnit.MILLISECONDS) } diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index 810994c0..b2b33dbb 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala @@ -15,11 +15,10 @@ import viper.server.ViperConfig import viper.server.core.VerificationExecutionContext import viper.viperserver.BuildInfo -import scala.concurrent.Future -import scala.concurrent.duration.DurationInt +import scala.concurrent.{Future, Promise} import scala.jdk.CollectionConverters._ import scala.jdk.FutureConverters._ -import scala.language.postfixOps +import java.util.concurrent.TimeUnit trait StandardReceiver { val coordinator: ClientCoordinator @@ -121,8 +120,12 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer { // we instruct the server to stop all verifications but we only wait for 2s for their completion since // the LSP client expects a response within 3s val stopVerifications = coordinator.stopAllRunningVerifications() - val timeout = akka.pattern.after(2 seconds)(Future.unit)(executor.actorSystem) - Future.firstCompletedOf(Seq(stopVerifications, timeout)).asJava.thenApply(_ => null.asInstanceOf[AnyRef]).toCompletableFuture() + val timeoutPromise = Promise[Unit]() + executor.scheduler.schedule(new Runnable { + override def run(): Unit = timeoutPromise.trySuccess(()) + }, 2L, TimeUnit.SECONDS) + Future.firstCompletedOf(Seq(stopVerifications, timeoutPromise.future))(executor) + .asJava.thenApply(_ => null.asInstanceOf[AnyRef]).toCompletableFuture() } override def setTrace(params: SetTraceParams): Unit = { diff --git a/src/main/scala/viper/server/frontends/lsp/file/QuantifierCodeLens.scala b/src/main/scala/viper/server/frontends/lsp/file/QuantifierCodeLens.scala index fd64e02e..125b4494 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/QuantifierCodeLens.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/QuantifierCodeLens.scala @@ -11,14 +11,12 @@ import scala.collection.mutable.HashMap import viper.silver.ast.utility.lsp._ import viper.silver.ast.LineColumnPosition import java.nio.file.Paths -import akka.actor.ActorSystem import scala.collection.mutable.HashSet -import scala.concurrent.duration.Duration import java.util.concurrent.TimeUnit -import scala.concurrent.ExecutionContext +import viper.server.core.VerificationExecutionContext trait QuantifierCodeLens extends ProjectAware { - implicit val ec: ExecutionContext + implicit val ec: VerificationExecutionContext // Quantifier chosen triggers private val quantifierMap: HashMap[RangePosition, ((Int, Int), Int, Int, Int)] = HashMap() @@ -68,7 +66,6 @@ trait QuantifierCodeLens extends ProjectAware { } } - private val system = ActorSystem("codeLensRefresher") private def doRefresh(): Unit = { Locker.synchronized { changed.foreach(uri => getInProject(uri).codeLensContainer.onUpdate()) @@ -87,7 +84,9 @@ trait QuantifierCodeLens extends ProjectAware { if (delta > refreshRate) { doRefresh() } else { - system.scheduler.scheduleOnce(Duration(refreshRate - delta, TimeUnit.MILLISECONDS))(doRefresh()) + ec.scheduler.schedule(new Runnable { + override def run(): Unit = doRefresh() + }, refreshRate - delta, TimeUnit.MILLISECONDS) } } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 4b3bc89b..6b0c5aa4 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -9,9 +9,10 @@ package viper.server.frontends.lsp.file import ch.qos.logback.classic.Logger import viper.server.frontends.lsp import scala.concurrent.Future -import viper.server.core.ViperBackendConfig +import viper.server.core.{ViperBackendConfig, VerificationExecutionContext} import viper.server.vsi.{AstJobId, VerJobId} -import scala.concurrent.ExecutionContext +import scala.concurrent.Promise +import java.util.concurrent.TimeUnit import akka.actor.Props import viper.server.frontends.lsp.VerificationSuccess._ @@ -90,7 +91,7 @@ trait VerificationManager extends ManagesLeaf { .recover(_ => false) } - implicit def ec: ExecutionContext + implicit def ec: VerificationExecutionContext var lastPhase: Option[VerificationPhase.VerificationPhase] = None private var futureAst: Option[Future[Unit]] = None @@ -112,12 +113,12 @@ trait VerificationManager extends ManagesLeaf { future.map(_ => this.synchronized(f)) } - private val system = akka.actor.ActorSystem("delayer") def delay[T](ms: Int)(block: => T): Future[T] = { - import scala.concurrent.duration._ - akka.pattern.after(ms.millis, system.scheduler) { - Future(block) - } + val promise = Promise[T]() + ec.scheduler.schedule(new Runnable { + override def run(): Unit = promise.completeWith(Future(block)) + }, ms.toLong, TimeUnit.MILLISECONDS) + promise.future } //other From 41a3a8357656cc6959ddaa1a81d91486093f4782 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 5 May 2026 18:29:17 +0200 Subject: [PATCH 02/22] Drop SeqActor and Terminator --- .../server/core/ViperCoreServerUtils.scala | 48 +----- src/main/scala/viper/server/vsi/HTTP.scala | 6 +- .../scala/viper/server/vsi/Terminator.scala | 54 ------- .../viper/server/vsi/VerificationServer.scala | 140 +++++++++--------- 4 files changed, 79 insertions(+), 169 deletions(-) delete mode 100644 src/main/scala/viper/server/vsi/Terminator.scala diff --git a/src/main/scala/viper/server/core/ViperCoreServerUtils.scala b/src/main/scala/viper/server/core/ViperCoreServerUtils.scala index e66f577c..3ac64d76 100644 --- a/src/main/scala/viper/server/core/ViperCoreServerUtils.scala +++ b/src/main/scala/viper/server/core/ViperCoreServerUtils.scala @@ -6,67 +6,23 @@ package viper.server.core -import akka.actor.{Actor, Props, Status} -import akka.pattern.ask -import akka.util.Timeout -import ch.qos.logback.classic.Logger import viper.server.vsi.{JobNotFoundException, VerJobId} import viper.silver.reporter.{Message, OverallFailureMessage, OverallSuccessMessage} import viper.silver.verifier.{VerificationResult, Failure => VerificationFailure, Success => VerificationSuccess} -import scala.concurrent.{Future, Promise} -import scala.concurrent.duration._ +import scala.concurrent.Future object ViperCoreServerUtils { - private object SeqActor { - case object Result - def props(jid: VerJobId, logger: Logger): Props = Props(new SeqActor(jid, logger)) - } - - class SeqActor(jid: VerJobId, logger: Logger) extends Actor { - - var messages: List[Message] = List() - private val msgPromise: Promise[List[Message]] = Promise() - - override def receive: PartialFunction[Any, Unit] = { - case m: Message => - logger.trace(s"SeqActor(JID ${jid.id}) received message $m") - messages = messages :+ m - case SeqActor.Result => - sender() ! msgPromise.future // return a future that will be completed as soon as all messages have been received - case Status.Success => - // Success is sent when the stream is completed - logger.trace(s"SeqActor(JID ${jid.id}) has successfully completed receiving messages") - msgPromise.success(messages) - case Status.Failure(cause) => - logger.trace(s"SeqActor(JID ${jid.id}) has failed receiving all messages: $cause") - msgPromise.failure(cause) - } - } - /** Get a Future containing all messages generated by the backend. - * - * This is a utility function and not part of ViperCoreServer. Therefore, an instance of ViperCoreServer as well as - * an instance of an actor system must be provided. * * Deletes the jobHandle on completion. */ def getMessagesFuture(core: ViperCoreServer, jid: VerJobId)(implicit executor: VerificationExecutionContext): Future[List[Message]] = { - import scala.language.postfixOps - - val actor = executor.actorSystem.actorOf(SeqActor.props(jid, core.globalLogger)) - val complete_future = core.streamMessages(jid, actor, include_ast = true).getOrElse(Future.failed(JobNotFoundException)) - complete_future.flatMap(_ => { - implicit val askTimeout: Timeout = Timeout(core.config.actorCommunicationTimeout() milliseconds) - (actor ? SeqActor.Result).mapTo[Future[List[Message]]].flatten - }) + core.collectMessages(jid).getOrElse(Future.failed(JobNotFoundException)) } /** Get a Future containing only verification results. - * - * This is a utility function and not part of ViperCoreServer. Therefore, an instance of ViperCoreServer as well as - * an instance of an actor system must be provided. * * Deletes the jobHandle on completion. */ diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala index 02755567..d9992bb7 100644 --- a/src/main/scala/viper/server/vsi/HTTP.scala +++ b/src/main/scala/viper/server/vsi/HTTP.scala @@ -78,7 +78,6 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp { ast_jobs = new JobPool("AST-pool", active_jobs) ver_jobs = new JobPool("Verification-pool", active_jobs) bindingFuture = Http().newServerAt("localhost", port).bindFlow(setRoutes()) - _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), Terminator.GetNextTerminatorName) bindingFuture.map { serverBinding => val newPort = serverBinding.localAddress.getPort if (port == 0) { @@ -92,6 +91,11 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp { } } + override protected def onExit(): Future[Unit] = { + if (bindingFuture == null) Future.unit + else bindingFuture.flatMap(_.unbind()).map(_ => ()) + } + /** The returned future is completed when the server is stopped. * Afterwards, the execution context can be terminated. * This function cannot be called before calling `start`. */ diff --git a/src/main/scala/viper/server/vsi/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala deleted file mode 100644 index 271296e0..00000000 --- a/src/main/scala/viper/server/vsi/Terminator.scala +++ /dev/null @@ -1,54 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. -// -// Copyright (c) 2011-2020 ETH Zurich. - -package viper.server.vsi - -import akka.actor.{Actor, Props} -import akka.http.scaladsl.Http -import viper.server.core.VerificationExecutionContext - -import java.util.concurrent.atomic.AtomicInteger -import scala.concurrent.Future - -// --- Actor: Terminator --- - - -object Terminator { - case object Exit - case class WatchJobQueue(jid: JobId, handle: JobHandle) - - // Each server start creates a new Terminator actor. Akka does not like non-unique actor names. - // Thus, we increment a counter to ensure unique names for our Terminator actors even though at no point - // two of them should be active. - // Without this counter, the issue of non-unique actor names occurs in testing contexts as, e.g. in Gobra's tests, - // we start a new ViperServer instance for each testcase that needs it. - private val terminatorCounter = new AtomicInteger(0) - def GetNextTerminatorName: String = s"terminator${terminatorCounter.getAndIncrement()}" - - def props[R](ast_jobs: JobPool[AstJobId, AstHandle[R]], - ver_jobs: JobPool[VerJobId, VerHandle], - bindingFuture: Option[Future[Http.ServerBinding]] = None) - (implicit ctx: VerificationExecutionContext): Props - = Props(new Terminator(ast_jobs, ver_jobs, bindingFuture)(ctx)) -} - -class Terminator[R](ast_jobs: JobPool[AstJobId, AstHandle[R]], - ver_jobs: JobPool[VerJobId, VerHandle], - bindingFuture: Option[Future[Http.ServerBinding]]) - (implicit val ctx: VerificationExecutionContext) extends Actor { - - override def receive: PartialFunction[Any, Unit] = { - case Terminator.Exit => - bindingFuture match { - case Some(future) => - future - .flatMap(_.unbind()) // trigger unbinding from the port - case None => - } - // note that the execution context is NOT terminated such that clients - // have better control over when the execution context should be terminated - } -} \ No newline at end of file diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index ec777d93..f9eab83d 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -6,7 +6,7 @@ package viper.server.vsi -import akka.Done +import akka.{Done, NotUsed} import akka.actor.{ActorRef, ActorSystem, PoisonPill, Status} import akka.pattern.ask import akka.stream.scaladsl.{Keep, Sink, Source} @@ -48,7 +48,10 @@ trait VerificationServer extends Post { implicit val system: ActorSystem = executor.actorSystem implicit def askTimeout: Timeout - protected var _termActor: ActorRef = _ + /** Hook invoked from `stop()` after all jobs have been interrupted. Default + * is a no-op. The HTTP frontend overrides this to unbind its server port. + */ + protected def onExit(): Future[Unit] = Future.unit implicit val ast_id_fact: Int => AstJobId = AstJobId.apply implicit val ver_id_fact: Int => VerJobId = VerJobId.apply @@ -186,64 +189,77 @@ trait VerificationServer extends Post { } } - /** Stream all messages generated by the Verification backend to some actor. - * If `include_ast` is set, this will also stream the AST messages. - * - * Deletes the JobHandle on completion. + /** Build the combined Envelope source for a verification job (optionally + * prepending the AST job's messages). Callers attach a sink to consume. */ - protected def streamMessages(jid: VerJobId, clientActor: ActorRef, include_ast: Boolean): Option[Future[Done]] = { + protected def messageEnvelopeSource(jid: VerJobId, include_ast: Boolean): Option[Future[(VerHandle, Source[Envelope, NotUsed])]] = { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } - ver_jobs.lookupJob(jid) match { - case None => - /** Verification job not found */ - None - case Some(handle_future) => - Some(handle_future.flatMap((ver_handle: VerHandle) => { - ver_handle.prev_job_id match { - case _ if !include_ast => - /** The AST for this verification job is already being streamed. */ - Future.successful((None, ver_handle)) - case None => - /** The AST for this verification job wasn't created by this server. */ - Future.successful((None, ver_handle)) - case Some(ast_id) => - /** The AST construction job may have been cleaned up - * (if all of its messages were already consumed) */ - ast_jobs.lookupJob(ast_id) match { - case Some(ast_handle_fut) => - ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle)) - case None => - Future.successful((None, ver_handle)) - } - } - }) flatMap { - case (ast_handle_maybe: Option[AstHandle[Option[AST]]], ver_handle: VerHandle) => - val ver_source = ver_handle match { - case VerHandle(null, null, null, _) => - /** There were no messages produced during verification. */ - Source.empty[Envelope] - case _ => - Source.fromPublisher(ver_handle.publisher) - } - val combined_source = ast_handle_maybe match { + ver_jobs.lookupJob(jid).map(handle_future => + handle_future.flatMap((ver_handle: VerHandle) => { + ver_handle.prev_job_id match { + case _ if !include_ast => + Future.successful((None, ver_handle)) + case None => + Future.successful((None, ver_handle)) + case Some(ast_id) => + ast_jobs.lookupJob(ast_id) match { + case Some(ast_handle_fut) => + ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle)) case None => - /** The AST messages were already consumed. */ - ver_source - case Some(ast_handle) => - ver_source.prepend(Source.fromPublisher(ast_handle.publisher)) + Future.successful((None, ver_handle)) } - val sink = Sink.actorRef(clientActor, Status.Success, Status.Failure) - val resulting_source = combined_source.map(e => unpack(e)) - resulting_source.runWith(sink) - - // FIXME This assumes that someone will actually complete the verification job queue. - // FIXME Could we guarantee that the client won't forget to do this? - ver_handle.queue.watchCompletion() - }) + } + }).map { + case (ast_handle_maybe: Option[AstHandle[Option[AST]]], ver_handle: VerHandle) => + val ver_source = ver_handle match { + case VerHandle(null, null, null, _) => + Source.empty[Envelope] + case _ => + Source.fromPublisher(ver_handle.publisher) + } + val combined_source = ast_handle_maybe match { + case None => ver_source + case Some(ast_handle) => ver_source.prepend(Source.fromPublisher(ast_handle.publisher)) + } + (ver_handle, combined_source) + }) + } + + /** Build the Envelope source for an AST job. */ + protected def messageEnvelopeSource(jid: AstJobId): Option[Future[(AstHandle[Option[AST]], Source[Envelope, NotUsed])]] = { + if (!isRunning) { + throw new IllegalStateException("Instance of VerificationServer already stopped") } + + ast_jobs.lookupJob(jid).map(_.map(ast_handle => + (ast_handle, Source.fromPublisher(ast_handle.publisher)))) + } + + /** Stream all messages generated by the Verification backend to some actor. + * If `include_ast` is set, this will also stream the AST messages. + * + * Deletes the JobHandle on completion. + */ + protected def streamMessages(jid: VerJobId, clientActor: ActorRef, include_ast: Boolean): Option[Future[Done]] = { + messageEnvelopeSource(jid, include_ast).map(_.flatMap { case (ver_handle, combined_source) => + val sink = Sink.actorRef(clientActor, Status.Success, Status.Failure) + combined_source.map(e => unpack(e)).runWith(sink) + // FIXME This assumes that someone will actually complete the verification job queue. + // FIXME Could we guarantee that the client won't forget to do this? + ver_handle.queue.watchCompletion() + }) + } + + /** Collect all messages generated by a verification job (including AST + * messages) into a list. Returns None if the job is unknown. + */ + def collectMessages(jid: VerJobId): Option[Future[List[A]]] = { + messageEnvelopeSource(jid, include_ast = true).map(_.flatMap { case (_, combined_source) => + combined_source.map(e => unpack(e)).runFold(List.empty[A])(_ :+ _) + }) } /** Stream all messages generated by the AST backend to some actor. @@ -251,18 +267,9 @@ trait VerificationServer extends Post { * Deletes the JobHandle on completion. */ protected def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = { - if (!isRunning) { - throw new IllegalStateException("Instance of VerificationServer already stopped") - } - - ast_jobs.lookupJob(jid).map(ast_handle_fut => { - ast_handle_fut.map(ast_handle => (Source.fromPublisher(ast_handle.publisher), ast_handle)).flatMap { - case (ast_handle_maybe, ast_handle) => { - val ast_source = ast_handle_maybe.map(e => unpack(e)) - ast_source.runWith(Sink.actorRef(clientActor, Status.Success, Status.Failure)) - ast_handle.queue.watchCompletion() - } - } + messageEnvelopeSource(jid).map(_.flatMap { case (ast_handle, ast_source) => + ast_source.map(e => unpack(e)).runWith(Sink.actorRef(clientActor, Status.Success, Status.Failure)) + ast_handle.queue.watchCompletion() }) } @@ -278,13 +285,11 @@ trait VerificationServer extends Post { } isRunning = false getInterruptFutureList().transform(r => { - _termActor ! Terminator.Exit + onExit() r match { case Success(_) => println(s"shutting down...") case Failure(_) => println(s"forcibly shutting down...") } - // delete termActor since we no longer need it. Otherwise, start() cannot be called - _termActor = null r }) } @@ -312,7 +317,6 @@ trait DefaultVerificationServerStart extends VerificationServer { override def start(active_jobs: Int): Future[Done] = { ast_jobs = new JobPool("VSI-AST-pool", active_jobs) ver_jobs = new JobPool("VSI-Verification-pool", active_jobs) - _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs), Terminator.GetNextTerminatorName) isRunning = true Future.successful(Done) } From 76fb75be7ae89beb49b4ae127fd3478e1206ebb8 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 09:47:52 +0200 Subject: [PATCH 03/22] Replace RelayActor with RelayHandler --- .../frontends/lsp/ViperServerService.scala | 43 +++- .../frontends/lsp/file/RelayActor.scala | 225 +++++++++--------- .../frontends/lsp/file/Verification.scala | 7 +- .../viper/server/core/CoreServerSpec.scala | 8 +- 4 files changed, 146 insertions(+), 137 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 858d23f1..5b9bf661 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -7,12 +7,13 @@ package viper.server.frontends.lsp import scala.language.postfixOps -import akka.actor.{PoisonPill, Props} +import akka.actor.PoisonPill import akka.pattern.ask import akka.util.Timeout import ch.qos.logback.classic.Logger import viper.server.ViperConfig import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, ViperCoreServer} +import viper.server.frontends.lsp.file.RelayHandler import viper.server.utility.ReformatterAstGenerator import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile} import viper.server.utility.Helpers.validateViperFile @@ -23,6 +24,7 @@ import viper.silver.ast.utility.FileLoader import scala.concurrent.Future import scala.concurrent.duration._ +import scala.util.{Failure, Success} class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext) extends ViperCoreServer(config)(executor) with DefaultVerificationServerStart { @@ -70,28 +72,43 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve } } - def startStreaming(jid: VerJobId, relayActor_props: Props, localLogger: Option[Logger] = None): Option[Future[Unit]] = { + def startStreaming(jid: VerJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { val logger = combineLoggers(localLogger) logger.debug("Sending verification request to ViperServer...") - val relay_actor = system.actorOf(relayActor_props) - streamMessages(jid, relay_actor, include_ast = true).map(_.map(_ => ())) + runStreamWithHandler(jid, handler, include_ast = true) } - def startStreamingAst(jid: AstJobId, relayActor_props: Props, localLogger: Option[Logger] = None): Option[Future[Unit]] = { + def startStreamingAst(jid: AstJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { val logger = combineLoggers(localLogger) - val relay_actor = system.actorOf(relayActor_props) - logger.debug(s"Sending ast construct request to ViperServer... (${relay_actor.toString()})") - streamMessages(jid, relay_actor).map(_.map(_ => ())) + logger.debug(s"Sending ast construct request to ViperServer...") + messageEnvelopeSource(jid).map(_.flatMap { case (ast_handle, ast_source) => + val done = ast_source.map(e => unpack(e)).runForeach(handler.handleMessage) + done.onComplete { + case Success(_) => handler.onStreamSuccess() + case Failure(e) => handler.onStreamFailure(e) + } + ast_handle.queue.watchCompletion().map(_ => ()) + }) } - def startStreamingVer(jid: VerJobId, relayActor_props: Props, localLogger: Option[Logger] = None): Option[Future[Unit]] = { + def startStreamingVer(jid: VerJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { val logger = combineLoggers(localLogger) - val relay_actor = system.actorOf(relayActor_props) - logger.debug(s"Sending verification request to ViperServer... (${relay_actor.toString()})") - streamMessages(jid, relay_actor, include_ast = false).map(_.map(_ => { + logger.debug(s"Sending verification request to ViperServer...") + runStreamWithHandler(jid, handler, include_ast = false).map(_.map(r => { logger.debug("Done verification request to ViperServer...") - () + r })) } + private def runStreamWithHandler(jid: VerJobId, handler: RelayHandler, include_ast: Boolean): Option[Future[Unit]] = { + messageEnvelopeSource(jid, include_ast).map(_.flatMap { case (ver_handle, combined_source) => + val done = combined_source.map(e => unpack(e)).runForeach(handler.handleMessage) + done.onComplete { + case Success(_) => handler.onStreamSuccess() + case Failure(e) => handler.onStreamFailure(e) + } + ver_handle.queue.watchCompletion().map(_ => ()) + }) + } + def stopVerification(jid: VerJobId, localLogger: Option[Logger] = None): Future[Boolean] = { val logger = combineLoggers(localLogger) ver_jobs.lookupJob(jid) match { diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index f88ca68c..daa7eda7 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -6,7 +6,6 @@ package viper.server.frontends.lsp.file -import akka.actor.{Actor, PoisonPill, Props, Status} import viper.server.frontends.lsp import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ @@ -17,7 +16,7 @@ import viper.server.frontends.lsp.file.ProgressCoordinator import viper.silver.parser._ trait MessageHandler extends ProjectManager with VerificationManager with QuantifierCodeLens with QuantifierInlayHints with SignatureHelp { - override def props(backendClassName: Option[String]): Props = RelayActor.props(this, backendClassName) + override def newRelayHandler(backendClassName: Option[String]): RelayHandler = new RelayHandler(this, backendClassName) var progress: ProgressCoordinator = null @@ -84,13 +83,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti } } -object RelayActor { - def props(task: MessageHandler, backendClassName: Option[String]): Props = Props(new RelayActor(task, backendClassName)) - - case class GetReportedErrors() -} - -class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends Actor { +class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { val coordinator = task.coordinator /** @@ -98,7 +91,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends * `ErrorMessage`). Storing the position along with the error fixes the issue that two errors with offending nodes * at different position just get dropped. */ - var reportedErrors: Set[(AbstractError, Option[ast.Position])] = Set.empty + private var reportedErrors: Set[(AbstractError, Option[ast.Position])] = Set.empty /** helper function to add an error to `reportedErrors` */ private def markErrorAsReported(err: AbstractError): Unit = err match { case err: ErrorMessage => reportedErrors = reportedErrors + ((err, Some(err.offendingNode.pos))) @@ -112,112 +105,114 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case _ => reportedErrors.contains((err, None)) } - override def receive: PartialFunction[Any, Unit] = { - case m if task.is_aborting => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ignoring message because we are aborting: $m") + def getReportedErrors: Seq[AbstractError] = reportedErrors.toSeq.map(_._1) - case PProgramReport(typeckSuccess, pProgram) => - // New project - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] got new pProgram for ${task.filename}") - val files = pProgram.imports.flatMap(_.resolved).map(_.toUri().toString()).toSet - task.setupProject(files) - val parseSuccess = pProgram.errors.isEmpty - val phase = if (typeckSuccess) VerificationPhase.TypeckEnd - else if (parseSuccess) VerificationPhase.ParseEnd - else VerificationPhase.ParseStart - if (typeckSuccess || task.lastPhase.forall(_.order <= phase.order)) { - task.resetContainers(true) - task.lastPhase = Some(phase) - - val beginnerMode = coordinator.server.config.beginnerMode() - task.addCodeLens(true)(HasCodeLens(pProgram)) - task.addDocumentSymbol(true)(HasDocumentSymbol(pProgram).toSeq) - task.addHoverHint(true)(HasHoverHints(pProgram)) - task.addGotoDefinition(true)(HasGotoDefinitions(pProgram)) - task.addFindReferences(true)(HasReferenceTos(pProgram)) - task.addFoldingRange(true)(HasFoldingRanges(pProgram)) - task.addInlayHint(true)(HasInlayHints(pProgram, beginnerMode)) - task.addSemanticHighlight(true)(HasSemanticHighlights(pProgram)) - task.addSignatureHelp(true)(HasSignatureHelps(pProgram)) - task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram)) - task.addCompletionProposal(true)(HasCompletionProposals(pProgram)) - } - case StatisticsReport(m, f, p, _, _) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") - task.progress = new ProgressCoordinator(coordinator, p, f, m) - val params = lsp.StateChangeParams(VerificationRunning.id, progress = 0, filename = task.filename) - coordinator.sendStateChangeNotification(params, Some(task)) - case AstConstructionFailureMessage(_, res) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] AstConstructionFailureMessage") - markErrorsAsReported(res.errors) - task.processErrors(backendClassName, res.errors, Some("Constructing the AST has failed:")) - case ExceptionReport(e) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ExceptionReport (${e.toString()}, ${e.getStackTrace().toString()})") - task.processErrors(backendClassName, Seq(AbortedExceptionally(e))) - case InvalidArgumentsReport(_, errors) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] InvalidArgumentsReport") - markErrorsAsReported(errors) - task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) - case EntitySuccessMessage(_, concerning, _, _) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntitySuccessMessage") - if (task.progress == null) { - coordinator.logger.debug("The backend must send a VerificationStart message before the ...Verified message.") - } else { - val output = lsp.BackendOutput(lsp.BackendOutputType.FunctionVerified, name = concerning.name) - task.progress.updateProgress(output) - val progressPercentage = task.progress.toPercent - val params = lsp.StateChangeParams(VerificationRunning.id, progress = progressPercentage, filename = task.filename) + def handleMessage(m: Message): Unit = { + if (task.is_aborting) { + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ignoring message because we are aborting: $m") + return + } + m match { + case PProgramReport(typeckSuccess, pProgram) => + // New project + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] got new pProgram for ${task.filename}") + val files = pProgram.imports.flatMap(_.resolved).map(_.toUri().toString()).toSet + task.setupProject(files) + val parseSuccess = pProgram.errors.isEmpty + val phase = if (typeckSuccess) VerificationPhase.TypeckEnd + else if (parseSuccess) VerificationPhase.ParseEnd + else VerificationPhase.ParseStart + if (typeckSuccess || task.lastPhase.forall(_.order <= phase.order)) { + task.resetContainers(true) + task.lastPhase = Some(phase) + + val beginnerMode = coordinator.server.config.beginnerMode() + task.addCodeLens(true)(HasCodeLens(pProgram)) + task.addDocumentSymbol(true)(HasDocumentSymbol(pProgram).toSeq) + task.addHoverHint(true)(HasHoverHints(pProgram)) + task.addGotoDefinition(true)(HasGotoDefinitions(pProgram)) + task.addFindReferences(true)(HasReferenceTos(pProgram)) + task.addFoldingRange(true)(HasFoldingRanges(pProgram)) + task.addInlayHint(true)(HasInlayHints(pProgram, beginnerMode)) + task.addSemanticHighlight(true)(HasSemanticHighlights(pProgram)) + task.addSignatureHelp(true)(HasSignatureHelps(pProgram)) + task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram)) + task.addCompletionProposal(true)(HasCompletionProposals(pProgram)) + } + case StatisticsReport(m, f, p, _, _) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") + task.progress = new ProgressCoordinator(coordinator, p, f, m) + val params = lsp.StateChangeParams(VerificationRunning.id, progress = 0, filename = task.filename) coordinator.sendStateChangeNotification(params, Some(task)) - } - case EntityFailureMessage(_, _, _, res, _) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntityFailureMessage") - markErrorsAsReported(res.errors) - task.processErrors(backendClassName, res.errors) - case OverallSuccessMessage(_, verificationTime) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallSuccessMessage") - task.state = VerificationReporting - task.timeMs = verificationTime - // the completion handler is not yet invoked (but as part of Status.Success) - case OverallFailureMessage(_, verificationTime, failure) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallFailureMessage") - task.state = VerificationReporting - task.timeMs = verificationTime - // we filter `failure.errors` such that only new errors are reported - // this is important since Silicon provides errors as part of EntityFailureMessages and the OverallFailureMessage - // where else Carbon does not produce EntityFailureMessages (except for cached members in which case - // ViperServer produces EntitySuccessMessage and EntityFailureMessages) - val newErrors = failure.errors.filterNot(hasAlreadyBeenReported) - markErrorsAsReported(newErrors) - task.processErrors(backendClassName, newErrors) - case WarningsDuringParsing(warnings) => - markErrorsAsReported(warnings) - task.processErrors(backendClassName, warnings) - case WarningsDuringTypechecking(warnings) => - markErrorsAsReported(warnings) - task.processErrors(backendClassName, warnings) - case WarningsDuringVerification(warnings) => - markErrorsAsReported(warnings) - task.processErrors(backendClassName, warnings) - // the completion handler is not yet invoked (but as part of Status.Success) - case QuantifierChosenTriggersMessage(qexp, triggers, oldTriggers) => - coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierChosenTriggersMessage") - task.handleQuantifierChosenTriggers(qexp, triggers, oldTriggers) - case QuantifierInstantiationsMessage(quantifier, instantiations, magGen, maxCost) => - coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierInstantiationsMessage") - task.handleQuantifierInstantiations(quantifier, instantiations, magGen, maxCost) - case m: Message => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] Message") - coordinator.client.map{_.notifyUnhandledViperServerMessage(lsp.UnhandledViperServerMessageTypeParams(m.name, m.toString, lsp.LogLevel.Info.id))} - case Status.Success => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] Status.Success") - // Success is sent when the stream is completed - if (backendClassName.isDefined) task.completionHandler(0) - self ! PoisonPill - case Status.Failure(cause) => - coordinator.logger.info(s"[receive@${task.filename}/${backendClassName.isDefined}] Streaming messages has failed in RelayActor with cause $cause") - if (backendClassName.isDefined) task.completionHandler(-1) // no success - self ! PoisonPill - case RelayActor.GetReportedErrors() => sender() ! reportedErrors.toSeq.map(_._1) - case e: Throwable => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] RelayActor received throwable: $e") + case AstConstructionFailureMessage(_, res) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] AstConstructionFailureMessage") + markErrorsAsReported(res.errors) + task.processErrors(backendClassName, res.errors, Some("Constructing the AST has failed:")) + case ExceptionReport(e) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ExceptionReport (${e.toString()}, ${e.getStackTrace().toString()})") + task.processErrors(backendClassName, Seq(AbortedExceptionally(e))) + case InvalidArgumentsReport(_, errors) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] InvalidArgumentsReport") + markErrorsAsReported(errors) + task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) + case EntitySuccessMessage(_, concerning, _, _) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntitySuccessMessage") + if (task.progress == null) { + coordinator.logger.debug("The backend must send a VerificationStart message before the ...Verified message.") + } else { + val output = lsp.BackendOutput(lsp.BackendOutputType.FunctionVerified, name = concerning.name) + task.progress.updateProgress(output) + val progressPercentage = task.progress.toPercent + val params = lsp.StateChangeParams(VerificationRunning.id, progress = progressPercentage, filename = task.filename) + coordinator.sendStateChangeNotification(params, Some(task)) + } + case EntityFailureMessage(_, _, _, res, _) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntityFailureMessage") + markErrorsAsReported(res.errors) + task.processErrors(backendClassName, res.errors) + case OverallSuccessMessage(_, verificationTime) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallSuccessMessage") + task.state = VerificationReporting + task.timeMs = verificationTime + case OverallFailureMessage(_, verificationTime, failure) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallFailureMessage") + task.state = VerificationReporting + task.timeMs = verificationTime + // we filter `failure.errors` such that only new errors are reported + // this is important since Silicon provides errors as part of EntityFailureMessages and the OverallFailureMessage + // where else Carbon does not produce EntityFailureMessages (except for cached members in which case + // ViperServer produces EntitySuccessMessage and EntityFailureMessages) + val newErrors = failure.errors.filterNot(hasAlreadyBeenReported) + markErrorsAsReported(newErrors) + task.processErrors(backendClassName, newErrors) + case WarningsDuringParsing(warnings) => + markErrorsAsReported(warnings) + task.processErrors(backendClassName, warnings) + case WarningsDuringTypechecking(warnings) => + markErrorsAsReported(warnings) + task.processErrors(backendClassName, warnings) + case WarningsDuringVerification(warnings) => + markErrorsAsReported(warnings) + task.processErrors(backendClassName, warnings) + case QuantifierChosenTriggersMessage(qexp, triggers, oldTriggers) => + coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierChosenTriggersMessage") + task.handleQuantifierChosenTriggers(qexp, triggers, oldTriggers) + case QuantifierInstantiationsMessage(quantifier, instantiations, magGen, maxCost) => + coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierInstantiationsMessage") + task.handleQuantifierInstantiations(quantifier, instantiations, magGen, maxCost) + case other => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] Message") + coordinator.client.map{_.notifyUnhandledViperServerMessage(lsp.UnhandledViperServerMessageTypeParams(other.name, other.toString, lsp.LogLevel.Info.id))} + } + } + + def onStreamSuccess(): Unit = { + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] stream success") + if (backendClassName.isDefined) task.completionHandler(0) + } + + def onStreamFailure(cause: Throwable): Unit = { + coordinator.logger.info(s"[receive@${task.filename}/${backendClassName.isDefined}] stream failed: $cause") + if (backendClassName.isDefined) task.completionHandler(-1) } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 6b0c5aa4..ba5badcc 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -13,7 +13,6 @@ import viper.server.core.{ViperBackendConfig, VerificationExecutionContext} import viper.server.vsi.{AstJobId, VerJobId} import scala.concurrent.Promise import java.util.concurrent.TimeUnit -import akka.actor.Props import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ @@ -244,7 +243,7 @@ trait VerificationManager extends ManagesLeaf { errorCount = 0 diagnosticCount = 0 handler.waitOn(verJob) - val receiver = props(Some(backendClassName)) + val receiver = newRelayHandler(Some(backendClassName)) futureVer = coordinator.server.startStreamingVer(verJob, receiver, Some(coordinator.localLogger)) true } else { @@ -266,7 +265,7 @@ trait VerificationManager extends ManagesLeaf { if (astJob.id >= 0) { this.resetDiagnostics(true) // Execute all handles - val newFut = coordinator.server.startStreamingAst(astJob, props(None), Some(coordinator.localLogger)) + val newFut = coordinator.server.startStreamingAst(astJob, newRelayHandler(None), Some(coordinator.localLogger)) futureAst = newFut handler.waitOn(astJob) Some(astJob) @@ -275,7 +274,7 @@ trait VerificationManager extends ManagesLeaf { } } - def props(backendClassName: Option[String]): Props + def newRelayHandler(backendClassName: Option[String]): RelayHandler def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index f1adc668..5563db4d 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -31,7 +31,6 @@ import scala.concurrent.duration._ import scala.concurrent.{Await, Future, Promise} import scala.util.{Failure, Success} import scala.language.postfixOps -import viper.server.frontends.lsp.file.RelayActor /** * Although the withServer fixture deals with futures, AnyWordSpec as been purposely chosen over AsyncFlatSpec: @@ -406,10 +405,9 @@ class CoreServerSpec extends AnyWordSpec with Matchers { coordinator.setClient(new MockClient()) val fileManager = FileManager(Paths.get(file).toAbsolutePath.toUri.toString, coordinator, None) val jid = verifyCarbonWithCaching(core, file) - val relayActorRef = context.actorSystem.actorOf(fileManager.props(Some("carbon"))) - implicit val askTimeout: Timeout = Timeout(5000 milliseconds) - core.streamMessages(jid, relayActorRef, include_ast = true).getOrElse(Future.failed(JobNotFoundException)) - .flatMap(_ => (relayActorRef ? RelayActor.GetReportedErrors()).mapTo[Seq[AbstractError]]) + val handler = fileManager.newRelayHandler(Some("carbon")) + core.startStreaming(jid, handler).getOrElse(Future.failed(JobNotFoundException)) + .map(_ => handler.getReportedErrors) .map(actualErrors => { val lineNrsOfActualVerificationErrors = actualErrors .map(_.pos match { From 1336cb85e9c070cf6f4a2ee30809c2f7cbc33d39 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 10:06:29 +0200 Subject: [PATCH 04/22] Drop QueueActor --- .../server/vsi/MessageStreamingTask.scala | 59 +++++++------------ .../scala/viper/server/vsi/Protocol.scala | 6 -- .../scala/viper/server/vsi/QueueActor.scala | 29 --------- .../viper/server/vsi/VerificationServer.scala | 9 +-- 4 files changed, 21 insertions(+), 82 deletions(-) delete mode 100644 src/main/scala/viper/server/vsi/QueueActor.scala diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala index 2cd43518..352e29d6 100644 --- a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala +++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala @@ -7,15 +7,11 @@ package viper.server.vsi import java.util.concurrent.{Callable, FutureTask} -import scala.language.postfixOps -import akka.actor.ActorRef -import akka.pattern.ask -import akka.stream.QueueOfferResult -import akka.util.Timeout +import akka.stream.scaladsl.SourceQueueWithComplete import ch.qos.logback.classic.Logger -import scala.concurrent.{Await, Future, Promise} import scala.concurrent.duration._ +import scala.concurrent.{Await, Future, Promise} import scala.util.Try @@ -23,12 +19,9 @@ import scala.util.Try /** This class is a generic wrapper for a any sort of task a VerificationServer might * work on. * - * It has the following properties: - * - implements callable and provides an artifact future that completes when the task terminates - * - provides a reference to a queue actor. - * - * The first serves the purpose of running the task concurrently. The second allows to - * communicate from the verification process to the server. + * Implements Callable and provides an artifact future that completes when the task + * terminates. Holds a reference to a SourceQueue used to push backend messages to + * downstream consumers. * */ abstract class MessageStreamingTask[T] extends Callable[T] with Post { @@ -38,52 +31,40 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { override def done(): Unit = artifactPromise.complete(Try(get())) } - private var q_actor: ActorRef = _ + private var queue: SourceQueueWithComplete[Envelope] = _ private var hasEnded: Boolean = false - final def setQueueActor(actor: ActorRef): Unit = { - if (q_actor != null) { - throw new IllegalStateException("cannot set queue actor - a queue actor has already been set") + final def setQueue(q: SourceQueueWithComplete[Envelope]): Unit = { + if (queue != null) { + throw new IllegalStateException("cannot set queue - a queue has already been set") } - - q_actor = actor + queue = q } - /** Sends massage to the attached actor. - * - * The actor receiving this message offers it to a queue. This offering returns a Future, - * which will eventually indicate whether or not the offer was successful. This method is - * blocking, as it waits for the successful completion of such an offer. - * */ + /** Offers `msg` to the downstream queue, blocking until the offer resolves. + * With the default backpressure overflow strategy, this naturally throttles the + * verification thread when consumers are slow. + */ protected def enqueueMessage(msg: Envelope, logger: Logger): Unit = { if (hasEnded) { throw new IllegalStateException("cannot enqueue message - message streaming task's end has already been registered") } logger.trace(s"enqueueMessage: $msg") - implicit val askTimeout: Timeout = Timeout(5000 milliseconds) - // answer is a future that will resolve with the actor's response to the BackendReport request - val answer = (q_actor ? TaskProtocol.BackendReport(msg)).mapTo[Future[QueueOfferResult]] - // currentOffer is the future that the actor will send in its response (assuming that no timeout occurred requesting it from the actor) - // currentOffer will resolve when the message is dequeued from the queue - val currentOffer = answer.flatten try { - // note that an exception is thrown if the currentOffer future fails, e.g. because the askTimeout occurred - Await.result(currentOffer, Duration.Inf) + Await.result(queue.offer(msg), Duration.Inf) } catch { case ex: Exception => logger.error(s"exception in enqueueMessage occurred: $ex") - // rethrow exception: throw ex } } - /** Notify the queue actor that the task has come to an end - * - * The actor receiving this message will close the queue. + /** Closes the downstream queue, signalling the end of the message stream. * - * @param success indicates whether or not the task has ended as successfully. - * */ + * @param success retained for API compatibility; queue completion is the same + * regardless of success/failure outcome. + */ protected def registerTaskEnd(success: Boolean, logger: Logger): Unit = { if (hasEnded) { throw new IllegalStateException("cannot register task end - message streaming task's end has already been registered") @@ -91,6 +72,6 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { hasEnded = true logger.trace(s"registerTaskEnd: $success") - q_actor ! TaskProtocol.FinalBackendReport(success) + queue.complete() } } diff --git a/src/main/scala/viper/server/vsi/Protocol.scala b/src/main/scala/viper/server/vsi/Protocol.scala index f0bcece0..1b412084 100644 --- a/src/main/scala/viper/server/vsi/Protocol.scala +++ b/src/main/scala/viper/server/vsi/Protocol.scala @@ -11,12 +11,6 @@ import org.reactivestreams.Publisher import spray.json.{DefaultJsonProtocol, RootJsonFormat} import viper.server.core.VerificationExecutionContext -// Protocol to communicate with QueueActor -object TaskProtocol { - case class BackendReport(msg: Envelope) - case class FinalBackendReport(success: Boolean) -} - object VerificationProtocol { sealed trait StartProcessRequest[T] { diff --git a/src/main/scala/viper/server/vsi/QueueActor.scala b/src/main/scala/viper/server/vsi/QueueActor.scala deleted file mode 100644 index be9dd6a5..00000000 --- a/src/main/scala/viper/server/vsi/QueueActor.scala +++ /dev/null @@ -1,29 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. -// -// Copyright (c) 2011-2020 ETH Zurich. - -package viper.server.vsi - -import akka.actor.{Actor, PoisonPill, Props} -import akka.stream.scaladsl.SourceQueueWithComplete - -// --- Actor: MessageActor --- - -object QueueActor { - def props(queue: SourceQueueWithComplete[Envelope]): Props = Props(new QueueActor(queue)) -} - -class QueueActor(queue: SourceQueueWithComplete[Envelope]) extends Actor { - - override def receive: PartialFunction[Any, Unit] = { - case TaskProtocol.BackendReport(msg) => - val offer_status = queue.offer(msg) - sender() ! offer_status - case TaskProtocol.FinalBackendReport(_) => - queue.complete() - self ! PoisonPill - case _ => - } -} diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index f9eab83d..389de107 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -105,14 +105,7 @@ trait VerificationServer extends Post { val (queue, publisher) = Source.queue[Envelope](10000, OverflowStrategy.backpressure) .toMat(Sink.asPublisher(false))(Keep.both).run() - /** This actor will be responsible for managing ONE queue, - * whereas the JobActor can manage multiple tasks, all of which are related to some pipeline, - * e.g. [Text] ---> [AST] ---> [VerificationResult] - * '--- Task I ----' | - * '---------- Task II ----------' - **/ - val message_actor = system.actorOf(QueueActor.props(queue), s"${pool.tag}--message_actor--${new_jid.id}") - task.setQueueActor(message_actor) + task.setQueue(queue) val job_actor = system.actorOf(JobActor.props(new_jid), s"${pool.tag}_job_actor_${new_jid}") From 5002b89911ab82230daafea6dff83e9804e7c2c2 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 10:18:30 +0200 Subject: [PATCH 05/22] Replace JobActor with JobExecution --- .../frontends/lsp/ViperServerService.scala | 28 ++----- src/main/scala/viper/server/vsi/HTTP.scala | 13 +-- .../scala/viper/server/vsi/JobActor.scala | 81 +++---------------- src/main/scala/viper/server/vsi/JobPool.scala | 7 +- .../scala/viper/server/vsi/Protocol.scala | 35 -------- .../viper/server/vsi/VerificationServer.scala | 56 +++++-------- 6 files changed, 46 insertions(+), 174 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 5b9bf661..8e2521de 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -6,10 +6,6 @@ package viper.server.frontends.lsp -import scala.language.postfixOps -import akka.actor.PoisonPill -import akka.pattern.ask -import akka.util.Timeout import ch.qos.logback.classic.Logger import viper.server.ViperConfig import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, ViperCoreServer} @@ -17,13 +13,11 @@ import viper.server.frontends.lsp.file.RelayHandler import viper.server.utility.ReformatterAstGenerator import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile} import viper.server.utility.Helpers.validateViperFile -import viper.server.vsi.VerificationProtocol.{StopAstConstruction, StopVerification} import viper.server.vsi.{AstJobId, DefaultVerificationServerStart, VerHandle, VerJobId} import viper.silver.parser.ReformatPrettyPrinter import viper.silver.ast.utility.FileLoader import scala.concurrent.Future -import scala.concurrent.duration._ import scala.util.{Failure, Success} class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext) @@ -133,17 +127,12 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve private def stopOnlyVerification(handle: VerHandle, combinedLogger: Logger): Future[Boolean] = { handle match { - // If AST construction failed, a verification handle will be returned where the actor field is null. + // If AST construction failed, a verification handle will be returned where the execution field is null. case VerHandle(null, _, _, _) => Future.successful(false) - case _ => { - implicit val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds) - val interrupt: Future[String] = (handle.job_actor ? StopVerification).mapTo[String] - handle.job_actor ! PoisonPill // the actor played its part. - interrupt.map(msg => { - combinedLogger.info(msg) - true - }) - } + case _ => + val interrupted = handle.execution.cancel() + combinedLogger.info(formatInterruptResult(VerJobId(-1), interrupted)) + Future.successful(true) } } @@ -151,9 +140,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve def discardAstJobLookup(jid: AstJobId): Unit = { ast_jobs.lookupJob(jid).map({job => ast_jobs.discardJob(jid) - job.map(astHandle => astHandle.queue.watchCompletion().onComplete(_ => { - astHandle.job_actor ! PoisonPill - })) + job }) } @@ -168,8 +155,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve ast_jobs.lookupJob(jid) match { case Some(handle_future) => handle_future.map { handle => - handle.job_actor ! StopAstConstruction - handle.job_actor ! PoisonPill // the actor played its part. + handle.execution.cancel() combinedLogger.info(s"ast construction stopped for job #$jid") true } diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala index d9992bb7..2ae276a6 100644 --- a/src/main/scala/viper/server/vsi/HTTP.scala +++ b/src/main/scala/viper/server/vsi/HTTP.scala @@ -7,19 +7,14 @@ package viper.server.vsi import akka.{Done, NotUsed} -import akka.actor.PoisonPill import akka.http.scaladsl.Http import akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport._ import akka.http.scaladsl.marshalling.ToResponseMarshallable import akka.http.scaladsl.server.Directives._ import akka.http.scaladsl.server.Route -import akka.pattern.ask import akka.stream.scaladsl.Source -import akka.util.Timeout -import viper.server.vsi.VerificationProtocol.StopVerification import scala.concurrent.{Future, Promise} -import scala.concurrent.duration._ import scala.util.{Failure, Success, Try} /** This trait contains the bear essentials required for an HTTP server. @@ -226,12 +221,8 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp { case Some(handle_future) => onComplete(handle_future) { case Success(handle) => - implicit val askTimeout: Timeout = Timeout(5000 milliseconds) - val interrupt_done: Future[String] = (handle.job_actor ? StopVerification).mapTo[String] - onSuccess(interrupt_done) { msg => - handle.job_actor ! PoisonPill // the actor played its part. - complete(discardJobConfirmation(id, msg)) - } + val msg = formatInterruptResult(ver_id, handle.execution.cancel()) + complete(discardJobConfirmation(id, msg)) case Failure(_) => complete(discardJobRejection(id)) } diff --git a/src/main/scala/viper/server/vsi/JobActor.scala b/src/main/scala/viper/server/vsi/JobActor.scala index c42a62ea..832156ed 100644 --- a/src/main/scala/viper/server/vsi/JobActor.scala +++ b/src/main/scala/viper/server/vsi/JobActor.scala @@ -6,79 +6,24 @@ package viper.server.vsi -import java.util.concurrent.FutureTask +import java.util.concurrent.{Executor, FutureTask} -import akka.actor.{Actor, Props} +/** Owns the FutureTask of a single AST construction or verification job and + * exposes synchronous start/cancel operations. Replaces the prior actor-based + * lifecycle wrapper. + */ +final class JobExecution[T](task: FutureTask[T]) { + def start(executor: Executor): Unit = executor.execute(task) - -// --- Actor: JobActor --- - -object JobActor { - def props[T](id: JobId): Props = Props(new JobActor[T](id)) -} - -class JobActor[T](private val id: JobId) extends Actor { - - import VerificationProtocol._ - - private var _astConstructionTask: FutureTask[T] = _ - private var _verificationTask: FutureTask[T] = _ - - private def interrupt(task: FutureTask[T]): Boolean = { - if (task != null && !task.isDone) { - task.cancel(true) - return true - } - false - } - - private def resetTask(task: FutureTask[T]): Unit = { + /** Returns true iff this call actually interrupted a still-running task. */ + def cancel(): Boolean = { if (task != null && !task.isDone) { task.cancel(true) + true + } else { + false } } - private def resetAstConstructionTask(): Unit = { - resetTask(_astConstructionTask) - _astConstructionTask = null - } - - private def resetVerificationTask(): Unit = { - resetTask(_verificationTask) - _verificationTask = null - } - - override def receive: PartialFunction[Any, Unit] = { - case req: StartProcessRequest[T] => - req match { - case _: ConstructAst[T] => - //println(">>> JobActor received request ConstructAst") - resetAstConstructionTask() - _astConstructionTask = req.task.futureTask - req.executor.execute(_astConstructionTask) - sender() ! AstHandle(self, req.queue, req.publisher, req.task.artifact) - - case ver_req: Verify[T] => - //println(">>> JobActor received request Verify") - resetVerificationTask() - _verificationTask = ver_req.task.futureTask - req.executor.execute(_verificationTask) - sender() ! VerHandle(self, ver_req.queue, ver_req.publisher, ver_req.prev_job_id) - } - case req: StopProcessRequest => - val did_I_interrupt = req match { - case StopAstConstruction => - interrupt(_astConstructionTask) - case StopVerification => - interrupt(_verificationTask) - } - if (did_I_interrupt) { - sender() ! s"$id has been successfully interrupted." - } else { - // FIXME: Saying this is a potential vulnerability - sender() ! s"$id has already been finalized." - } - case msg => - throw new Exception("JobActor: received unexpected message: " + msg) - } + def isDone: Boolean = task.isDone } diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index fc8ab945..d77f2ca6 100644 --- a/src/main/scala/viper/server/vsi/JobPool.scala +++ b/src/main/scala/viper/server/vsi/JobPool.scala @@ -6,7 +6,6 @@ package viper.server.vsi -import akka.actor.ActorRef import akka.stream.scaladsl.SourceQueueWithComplete import org.reactivestreams.Publisher @@ -30,19 +29,19 @@ case class VerJobId(id: Int) extends JobId { sealed trait JobHandle { def tag: String // identify the kind of job this is - val job_actor: ActorRef + val execution: JobExecution[_] val queue: SourceQueueWithComplete[Envelope] val publisher: Publisher[Envelope] } -case class AstHandle[R](job_actor: ActorRef, +case class AstHandle[R](execution: JobExecution[_], queue: SourceQueueWithComplete[Envelope], publisher: Publisher[Envelope], artifact: Future[R]) extends JobHandle { def tag = "AST" } -case class VerHandle(job_actor: ActorRef, +case class VerHandle(execution: JobExecution[_], queue: SourceQueueWithComplete[Envelope], publisher: Publisher[Envelope], prev_job_id: Option[AstJobId]) extends JobHandle { diff --git a/src/main/scala/viper/server/vsi/Protocol.scala b/src/main/scala/viper/server/vsi/Protocol.scala index 1b412084..83d8e80a 100644 --- a/src/main/scala/viper/server/vsi/Protocol.scala +++ b/src/main/scala/viper/server/vsi/Protocol.scala @@ -6,42 +6,7 @@ package viper.server.vsi -import akka.stream.scaladsl.SourceQueueWithComplete -import org.reactivestreams.Publisher import spray.json.{DefaultJsonProtocol, RootJsonFormat} -import viper.server.core.VerificationExecutionContext - -object VerificationProtocol { - - sealed trait StartProcessRequest[T] { - val task: MessageStreamingTask[T] - val queue: SourceQueueWithComplete[Envelope] - val publisher: Publisher[Envelope] - val executor: VerificationExecutionContext - } - - // Request Job Actor to execute an AST construction task - case class ConstructAst[T](task: MessageStreamingTask[T], - queue: SourceQueueWithComplete[Envelope], - publisher: Publisher[Envelope], - executor: VerificationExecutionContext) extends StartProcessRequest[T] - - // Request Job Actor to execute a verification task - case class Verify[T](task: MessageStreamingTask[T], - queue: SourceQueueWithComplete[Envelope], - publisher: Publisher[Envelope], - prev_job_id: Option[AstJobId], - executor: VerificationExecutionContext) extends StartProcessRequest[T] - - sealed trait StopProcessRequest - - // Request Job Actor to stop its verification task - case object StopAstConstruction extends StopProcessRequest - - // Request Job Actor to stop its verification task - case object StopVerification extends StopProcessRequest -} - object Requests extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol { diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index 389de107..5f240038 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -7,18 +7,15 @@ package viper.server.vsi import akka.{Done, NotUsed} -import akka.actor.{ActorRef, ActorSystem, PoisonPill, Status} -import akka.pattern.ask +import akka.actor.{ActorRef, ActorSystem, Status} import akka.stream.scaladsl.{Keep, Sink, Source} import akka.stream.OverflowStrategy import akka.util.Timeout import viper.server.core.VerificationExecutionContext -import scala.concurrent.duration._ import scala.concurrent.Future import scala.reflect.ClassTag import scala.util.{Failure, Success} -import scala.language.postfixOps abstract class VerificationServerException extends Exception @@ -97,36 +94,27 @@ trait VerificationServer extends Post { Future.successful(VerHandle(null, null, null, prev_job_id_maybe)) } case Some(task) => - /** What we really want here is SourceQueueWithComplete[Envelope] - * Publisher[Envelope] might be needed to create a stream later on, - * but the publisher and the queue are synchronized are should be viewed - * as different representation of the same concept. - */ val (queue, publisher) = Source.queue[Envelope](10000, OverflowStrategy.backpressure) .toMat(Sink.asPublisher(false))(Keep.both).run() task.setQueue(queue) - val job_actor = system.actorOf(JobActor.props(new_jid), s"${pool.tag}_job_actor_${new_jid}") + val execution = new JobExecution(task.futureTask) /** Register cleanup task. */ queue.watchCompletion().onComplete(_ => { if (discardOnCompletion) { - pool.discardJob(new_jid) - /** FIXME: if the job actors are meant to be reused from one phase to another (only partially implemented), - * FIXME: then they should be stopped only after the **last** job is completed in the pipeline. */ - job_actor ! PoisonPill + pool.discardJob(new_jid) } }) - (job_actor ? (new_jid match { + execution.start(executor.executorService) + + val handle: JobHandle = new_jid match { case _: AstJobId => - VerificationProtocol.ConstructAst(task, queue, publisher, executor) + AstHandle(execution, queue, publisher, task.artifact) case _: VerJobId => - VerificationProtocol.Verify(task, queue, publisher, - /** TODO: Use factories for specializing the messages. - * TODO: Clearly, there should be a clean separation between concrete job types - * TODO: (AST Construction, Verification) and generic types (JobHandle). */ + VerHandle(execution, queue, publisher, prev_job_id_maybe match { case Some(prev_job_id: AstJobId) => Some(prev_job_id) @@ -134,10 +122,10 @@ trait VerificationServer extends Post { throw new IllegalArgumentException(s"cannot map ${prev_job_id.toString} to expected type AstJobId") case None => None - }, executor) - })).mapTo[T] + }) + } + Future.successful(handle.asInstanceOf[T]) } - /** TODO avoid hardcoded parameters */ }).recover({ case e: AstConstructionException => @@ -290,19 +278,17 @@ trait VerificationServer extends Post { /** This method interrupts active jobs upon termination of the server. */ protected def getInterruptFutureList(): Future[List[String]] = { - implicit val askTimeout: Timeout = Timeout(1000 milliseconds) val handles = ver_jobs.jobHandles ++ ast_jobs.jobHandles - val interrupt_future_list: List[Future[String]] = handles map { - case (_, handle_future) => - handle_future.flatMap { - case AstHandle(actor, _, _, _) => - (actor ? VerificationProtocol.StopAstConstruction).mapTo[String] - case VerHandle(actor, _, _, _) => - (actor ? VerificationProtocol.StopVerification).mapTo[String] - } - } toList - val overall_interrupt_future: Future[List[String]] = Future.sequence(interrupt_future_list) - overall_interrupt_future + val interrupt_future_list: List[Future[String]] = handles.map { + case (jid, handle_future) => + handle_future.map(handle => formatInterruptResult(jid, handle.execution.cancel())) + }.toList + Future.sequence(interrupt_future_list) + } + + protected def formatInterruptResult(jid: JobId, interrupted: Boolean): String = { + if (interrupted) s"$jid has been successfully interrupted." + else s"$jid has already been finalized." } } From 06754a69d0cf7b276399011184c6aaa24c2af1bf Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 10:47:34 +0200 Subject: [PATCH 06/22] Replace Source.queue with EnvelopeStream over LinkedBlockingQueue --- build.sbt | 9 ++ .../frontends/lsp/ViperServerService.scala | 6 +- .../viper/server/vsi/EnvelopeStream.scala | 88 +++++++++++++++++++ src/main/scala/viper/server/vsi/HTTP.scala | 8 +- src/main/scala/viper/server/vsi/JobPool.scala | 12 +-- .../server/vsi/MessageStreamingTask.scala | 36 ++++---- .../viper/server/vsi/VerificationServer.scala | 30 +++---- 7 files changed, 136 insertions(+), 53 deletions(-) create mode 100644 src/main/scala/viper/server/vsi/EnvelopeStream.scala diff --git a/build.sbt b/build.sbt index e5ed73aa..fc7fc701 100644 --- a/build.sbt +++ b/build.sbt @@ -31,6 +31,15 @@ lazy val server = (project in file(".")) libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test, libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test, libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol + libraryDependencies += "com.lihaoyi" %% "cask" % "0.9.5", // Lightweight HTTP server (replacing Akka HTTP) + libraryDependencies += "com.lihaoyi" %% "upickle" % "4.0.2", // JSON marshalling for cask + // upickle and geny pull conflicting transitive versions across the dependency tree; + // accept the newer ones since they are the consumers' preferred versions. + libraryDependencySchemes += "com.lihaoyi" %% "upickle" % "always", + libraryDependencySchemes += "com.lihaoyi" %% "upickle-core" % "always", + libraryDependencySchemes += "com.lihaoyi" %% "upickle-implicits" % "always", + libraryDependencySchemes += "com.lihaoyi" %% "ujson" % "always", + libraryDependencySchemes += "com.lihaoyi" %% "geny" % "always", silicon / excludeFilter := "logback.xml", /* Ignore Silicon's Logback configuration */ carbon / excludeFilter := "logback.xml", /* Ignore Carbon's Logback configuration */ diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 8e2521de..a018d499 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -80,7 +80,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve case Success(_) => handler.onStreamSuccess() case Failure(e) => handler.onStreamFailure(e) } - ast_handle.queue.watchCompletion().map(_ => ()) + ast_handle.stream.watchCompletion }) } def startStreamingVer(jid: VerJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { @@ -99,7 +99,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve case Success(_) => handler.onStreamSuccess() case Failure(e) => handler.onStreamFailure(e) } - ver_handle.queue.watchCompletion().map(_ => ()) + ver_handle.stream.watchCompletion }) } @@ -128,7 +128,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve private def stopOnlyVerification(handle: VerHandle, combinedLogger: Logger): Future[Boolean] = { handle match { // If AST construction failed, a verification handle will be returned where the execution field is null. - case VerHandle(null, _, _, _) => Future.successful(false) + case VerHandle(null, _, _) => Future.successful(false) case _ => val interrupted = handle.execution.cancel() combinedLogger.info(formatInterruptResult(VerJobId(-1), interrupted)) diff --git a/src/main/scala/viper/server/vsi/EnvelopeStream.scala b/src/main/scala/viper/server/vsi/EnvelopeStream.scala new file mode 100644 index 00000000..ddcb4162 --- /dev/null +++ b/src/main/scala/viper/server/vsi/EnvelopeStream.scala @@ -0,0 +1,88 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2020 ETH Zurich. + +package viper.server.vsi + +import java.util.concurrent.LinkedBlockingQueue +import scala.concurrent.{Future, Promise} + +/** Single-producer/single-consumer message stream backed by a bounded + * `LinkedBlockingQueue`. Replaces the previous `Source.queue` plumbing — + * `offer` blocks the producer when the queue is full (natural backpressure) + * and `iterator` blocks the consumer when the queue is empty. + * + * `complete` enqueues a sentinel so the iterator terminates cleanly even if + * the consumer is currently waiting on `take`. + */ +final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { + import EnvelopeStream._ + + private val queue = new LinkedBlockingQueue[Item](capacity) + private val completionPromise: Promise[Unit] = Promise() + @volatile private var completed: Boolean = false + + /** Block until `e` can be enqueued. Throws if the stream is already complete. */ + def offer(e: Envelope): Unit = { + if (completed) { + throw new IllegalStateException("EnvelopeStream is already complete") + } + queue.put(Msg(e)) + } + + /** Mark the stream complete. Idempotent. */ + def complete(): Unit = this.synchronized { + if (!completed) { + completed = true + queue.put(Done) + completionPromise.trySuccess(()) + } + } + + /** Future that resolves when `complete` is called. */ + def watchCompletion: Future[Unit] = completionPromise.future + + /** Single-shot iterator over the stream. Blocks on `hasNext`/`next` until + * envelopes are available. Returns false from `hasNext` once the + * completion sentinel is observed. + */ + def iterator: Iterator[Envelope] = new Iterator[Envelope] { + private var nextItem: Envelope = _ + private var atEnd: Boolean = false + private var hasFetched: Boolean = false + + override def hasNext: Boolean = { + if (atEnd) return false + if (hasFetched) return true + queue.take() match { + case Msg(e) => + nextItem = e + hasFetched = true + true + case Done => + atEnd = true + // Re-enqueue the sentinel in case anything else is also draining. + queue.put(Done) + false + } + } + + override def next(): Envelope = { + if (!hasNext) throw new NoSuchElementException("EnvelopeStream iterator exhausted") + val r = nextItem + hasFetched = false + nextItem = null.asInstanceOf[Envelope] + r + } + } +} + +object EnvelopeStream { + val DefaultCapacity: Int = 10000 + + private sealed trait Item + private final case class Msg(e: Envelope) extends Item + private case object Done extends Item +} diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala index 2ae276a6..5f13c080 100644 --- a/src/main/scala/viper/server/vsi/HTTP.scala +++ b/src/main/scala/viper/server/vsi/HTTP.scala @@ -150,7 +150,7 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp { case Some(handle_future) => onComplete(handle_future) { case Success(handle) => - val s: Source[Envelope, NotUsed] = Source.fromPublisher(handle.publisher) + val s: Source[Envelope, NotUsed] = Source.fromIterator(() => handle.stream.iterator) complete(unpackMessages(s)) case Failure(error) => // TODO use AST-specific response @@ -190,18 +190,18 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp { })) { case Success((ast_handle_maybe, ver_handle)) => val ver_source = ver_handle match { - case VerHandle(null, null, null, _) => + case VerHandle(null, null, _) => /** There were no messages produced during verification. */ Source.empty[Envelope] case _ => - Source.fromPublisher(ver_handle.publisher) + Source.fromIterator(() => ver_handle.stream.iterator) } val ast_source = ast_handle_maybe match { case None => /** The AST messages were already consumed. */ Source.empty[Envelope] case Some(ast_handle) => - Source.fromPublisher(ast_handle.publisher) + Source.fromIterator(() => ast_handle.stream.iterator) } val resulting_source = ver_source.prepend(ast_source) complete(unpackMessages(resulting_source)) diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index d77f2ca6..2aa85cc3 100644 --- a/src/main/scala/viper/server/vsi/JobPool.scala +++ b/src/main/scala/viper/server/vsi/JobPool.scala @@ -6,9 +6,6 @@ package viper.server.vsi -import akka.stream.scaladsl.SourceQueueWithComplete -import org.reactivestreams.Publisher - import java.util.concurrent.atomic.AtomicInteger import scala.collection.mutable import scala.concurrent.{Future, Promise} @@ -30,20 +27,17 @@ case class VerJobId(id: Int) extends JobId { sealed trait JobHandle { def tag: String // identify the kind of job this is val execution: JobExecution[_] - val queue: SourceQueueWithComplete[Envelope] - val publisher: Publisher[Envelope] + val stream: EnvelopeStream } case class AstHandle[R](execution: JobExecution[_], - queue: SourceQueueWithComplete[Envelope], - publisher: Publisher[Envelope], + stream: EnvelopeStream, artifact: Future[R]) extends JobHandle { def tag = "AST" } case class VerHandle(execution: JobExecution[_], - queue: SourceQueueWithComplete[Envelope], - publisher: Publisher[Envelope], + stream: EnvelopeStream, prev_job_id: Option[AstJobId]) extends JobHandle { def tag = "VER" } diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala index 352e29d6..02c09956 100644 --- a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala +++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala @@ -7,21 +7,18 @@ package viper.server.vsi import java.util.concurrent.{Callable, FutureTask} -import akka.stream.scaladsl.SourceQueueWithComplete import ch.qos.logback.classic.Logger -import scala.concurrent.duration._ -import scala.concurrent.{Await, Future, Promise} +import scala.concurrent.{Future, Promise} import scala.util.Try -/** This class is a generic wrapper for a any sort of task a VerificationServer might - * work on. +/** Generic wrapper for any task a VerificationServer might work on. * - * Implements Callable and provides an artifact future that completes when the task - * terminates. Holds a reference to a SourceQueue used to push backend messages to - * downstream consumers. + * Implements Callable and provides an artifact future that completes when the + * task terminates. Holds a reference to an `EnvelopeStream` used to push + * backend messages to downstream consumers. * */ abstract class MessageStreamingTask[T] extends Callable[T] with Post { @@ -31,19 +28,18 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { override def done(): Unit = artifactPromise.complete(Try(get())) } - private var queue: SourceQueueWithComplete[Envelope] = _ + private var stream: EnvelopeStream = _ private var hasEnded: Boolean = false - final def setQueue(q: SourceQueueWithComplete[Envelope]): Unit = { - if (queue != null) { - throw new IllegalStateException("cannot set queue - a queue has already been set") + final def setStream(s: EnvelopeStream): Unit = { + if (stream != null) { + throw new IllegalStateException("cannot set stream - a stream has already been set") } - queue = q + stream = s } - /** Offers `msg` to the downstream queue, blocking until the offer resolves. - * With the default backpressure overflow strategy, this naturally throttles the - * verification thread when consumers are slow. + /** Offers `msg` to the downstream stream, blocking until queue space is available + * (natural backpressure when consumers are slow). */ protected def enqueueMessage(msg: Envelope, logger: Logger): Unit = { if (hasEnded) { @@ -52,7 +48,7 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { logger.trace(s"enqueueMessage: $msg") try { - Await.result(queue.offer(msg), Duration.Inf) + stream.offer(msg) } catch { case ex: Exception => logger.error(s"exception in enqueueMessage occurred: $ex") @@ -60,9 +56,9 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { } } - /** Closes the downstream queue, signalling the end of the message stream. + /** Closes the downstream stream, signalling the end of the message stream. * - * @param success retained for API compatibility; queue completion is the same + * @param success retained for API compatibility; stream completion is the same * regardless of success/failure outcome. */ protected def registerTaskEnd(success: Boolean, logger: Logger): Unit = { @@ -72,6 +68,6 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { hasEnded = true logger.trace(s"registerTaskEnd: $success") - queue.complete() + stream.complete() } } diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index 5f240038..38ea5a19 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -8,8 +8,7 @@ package viper.server.vsi import akka.{Done, NotUsed} import akka.actor.{ActorRef, ActorSystem, Status} -import akka.stream.scaladsl.{Keep, Sink, Source} -import akka.stream.OverflowStrategy +import akka.stream.scaladsl.{Sink, Source} import akka.util.Timeout import viper.server.core.VerificationExecutionContext @@ -91,18 +90,17 @@ trait VerificationServer extends Post { pool.discardJob(new_jid) new_jid match { case _: VerJobId => - Future.successful(VerHandle(null, null, null, prev_job_id_maybe)) + Future.successful(VerHandle(null, null, prev_job_id_maybe)) } case Some(task) => - val (queue, publisher) = Source.queue[Envelope](10000, OverflowStrategy.backpressure) - .toMat(Sink.asPublisher(false))(Keep.both).run() + val stream = new EnvelopeStream() - task.setQueue(queue) + task.setStream(stream) val execution = new JobExecution(task.futureTask) /** Register cleanup task. */ - queue.watchCompletion().onComplete(_ => { + stream.watchCompletion.onComplete(_ => { if (discardOnCompletion) { pool.discardJob(new_jid) } @@ -112,9 +110,9 @@ trait VerificationServer extends Post { val handle: JobHandle = new_jid match { case _: AstJobId => - AstHandle(execution, queue, publisher, task.artifact) + AstHandle(execution, stream, task.artifact) case _: VerJobId => - VerHandle(execution, queue, publisher, + VerHandle(execution, stream, prev_job_id_maybe match { case Some(prev_job_id: AstJobId) => Some(prev_job_id) @@ -196,14 +194,14 @@ trait VerificationServer extends Post { }).map { case (ast_handle_maybe: Option[AstHandle[Option[AST]]], ver_handle: VerHandle) => val ver_source = ver_handle match { - case VerHandle(null, null, null, _) => + case VerHandle(null, null, _) => Source.empty[Envelope] case _ => - Source.fromPublisher(ver_handle.publisher) + Source.fromIterator(() => ver_handle.stream.iterator) } val combined_source = ast_handle_maybe match { case None => ver_source - case Some(ast_handle) => ver_source.prepend(Source.fromPublisher(ast_handle.publisher)) + case Some(ast_handle) => ver_source.prepend(Source.fromIterator(() => ast_handle.stream.iterator)) } (ver_handle, combined_source) }) @@ -216,7 +214,7 @@ trait VerificationServer extends Post { } ast_jobs.lookupJob(jid).map(_.map(ast_handle => - (ast_handle, Source.fromPublisher(ast_handle.publisher)))) + (ast_handle, Source.fromIterator(() => ast_handle.stream.iterator)))) } /** Stream all messages generated by the Verification backend to some actor. @@ -228,9 +226,7 @@ trait VerificationServer extends Post { messageEnvelopeSource(jid, include_ast).map(_.flatMap { case (ver_handle, combined_source) => val sink = Sink.actorRef(clientActor, Status.Success, Status.Failure) combined_source.map(e => unpack(e)).runWith(sink) - // FIXME This assumes that someone will actually complete the verification job queue. - // FIXME Could we guarantee that the client won't forget to do this? - ver_handle.queue.watchCompletion() + ver_handle.stream.watchCompletion.map(_ => Done) }) } @@ -250,7 +246,7 @@ trait VerificationServer extends Post { protected def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = { messageEnvelopeSource(jid).map(_.flatMap { case (ast_handle, ast_source) => ast_source.map(e => unpack(e)).runWith(Sink.actorRef(clientActor, Status.Success, Status.Failure)) - ast_handle.queue.watchCompletion() + ast_handle.stream.watchCompletion.map(_ => Done) }) } From 084c552006dd618a3dbe14b25aaeee318cfa88c8 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 11:11:33 +0200 Subject: [PATCH 07/22] Replace akka-http server with cask --- build.sbt | 1 + .../frontends/http/ViperHttpServer.scala | 373 ++++++++++++------ .../http/jsonWriters/ViperIDEProtocol.scala | 15 +- src/main/scala/viper/server/vsi/HTTP.scala | 234 ----------- .../scala/viper/server/vsi/Protocol.scala | 2 +- .../server/core/ViperServerHttpSpec.scala | 128 ++---- 6 files changed, 289 insertions(+), 464 deletions(-) delete mode 100644 src/main/scala/viper/server/vsi/HTTP.scala diff --git a/build.sbt b/build.sbt index fc7fc701..23e9e2dd 100644 --- a/build.sbt +++ b/build.sbt @@ -33,6 +33,7 @@ lazy val server = (project in file(".")) libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol libraryDependencies += "com.lihaoyi" %% "cask" % "0.9.5", // Lightweight HTTP server (replacing Akka HTTP) libraryDependencies += "com.lihaoyi" %% "upickle" % "4.0.2", // JSON marshalling for cask + libraryDependencies += "io.spray" %% "spray-json" % "1.3.6", // JSON AST and serialization (existing marshallers) // upickle and geny pull conflicting transitive versions across the dependency tree; // accept the newer ones since they are the consumers' preferred versions. libraryDependencySchemes += "com.lihaoyi" %% "upickle" % "always", diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala index ebe9fec3..b9c626c0 100644 --- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala +++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala @@ -6,189 +6,306 @@ package viper.server.frontends.http -import akka.{Done, NotUsed} -import akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport._ -import akka.http.scaladsl.marshalling.ToResponseMarshallable -import akka.http.scaladsl.server.Directives._ -import akka.http.scaladsl.server.Route -import akka.stream.scaladsl.Source +import java.net.InetSocketAddress +import akka.Done import edu.mit.csail.sdg.alloy4.A4Reporter import edu.mit.csail.sdg.parser.CompUtil import edu.mit.csail.sdg.translator.{A4Options, TranslateAlloyToKodkod} -import spray.json.{DefaultJsonProtocol, RootJsonFormat} +import io.undertow.Undertow +import spray.json._ import viper.server.ViperConfig import viper.server.core.{AstConstructionFailureException, VerificationExecutionContext, ViperBackendConfig, ViperCache, ViperCoreServer} -import viper.server.frontends.http.jsonWriters.ViperIDEProtocol.{AlloyGenerationRequestComplete, AlloyGenerationRequestReject, CacheFlushAccept, CacheFlushReject, JobDiscardAccept, JobDiscardReject, ServerStopConfirmed, VerificationRequestAccept, VerificationRequestReject} +import viper.server.frontends.http.jsonWriters.ViperIDEProtocol._ import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile} -import viper.server.vsi.Requests.CacheResetRequest import viper.server.vsi._ -import viper.silver.reporter.Message -import scala.concurrent.Future -import scala.util.{Failure, Success, Try} +import scala.concurrent.{Future, Promise} +import scala.util.{Failure, Success} class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContext) - extends ViperCoreServer(config)(executor) with VerificationServerHttp { + extends ViperCoreServer(config)(executor) { + + var port: Int = 0 + private var undertow: Undertow = _ + private val stoppedPromise: Promise[Done] = Promise() + + private val routes: ViperCaskRoutes = new ViperCaskRoutes(this) override def start(): Future[Done] = { - port = config.port.toOption.getOrElse(0) // 0 causes HTTP server to automatically select a free port - // we call here `ViperCoreServer.start()` (which internally calls `VerificationServer.start(activeJobs)`) - // Note that `VerificationServer.start(activeJobs)` is overridden in VerificationServerHttp. - super.start().map({ _ => + port = config.port.toOption.getOrElse(0) + super.start().map { _ => println(s"ViperServer online at http://localhost:$port") Done - })(executor) + }(executor) } - def setRoutes(): Route = { - addRoute(routes(), AdditionalViperServerRoute()) + override def start(active_jobs: Int): Future[Done] = { + ast_jobs = new JobPool("AST-pool", active_jobs) + ver_jobs = new JobPool("Verification-pool", active_jobs) + undertow = Undertow.builder() + .addHttpListener(port, "localhost") + .setHandler(routes.defaultHandler) + .build() + undertow.start() + val boundAddr = undertow.getListenerInfo.get(0).getAddress.asInstanceOf[InetSocketAddress] + port = boundAddr.getPort + isRunning = true + Future.successful(Done) } - override def serverStopConfirmation(interrupt: Try[List[String]]): ToResponseMarshallable = { - interrupt match { + override protected def onExit(): Future[Unit] = { + if (undertow != null) { + val u = undertow + undertow = null + Future { + u.stop() + }(executor).map(_ => ())(executor) + } else { + Future.unit + } + } + + /** Future that resolves once the server has been shut down via /exit. */ + def stopped(): Future[Done] = stoppedPromise.future + + /** Triggered by the `/exit` route. Stops jobs, unbinds the listener, then + * completes the `stopped()` future. + */ + private[http] def handleExit(): String = { + val confirmation = scala.util.Try(scala.concurrent.Await.result( + stop(), scala.concurrent.duration.Duration.Inf)) + val msg = confirmation match { case Success(_) => println("shutting down...") - ServerStopConfirmed("shutting down...") + "shutting down..." case Failure(err_msg) => globalLogger.error(s"Interrupting one of the verification threads timed out: $err_msg") println("forcibly shutting down...") - ServerStopConfirmed("forcibly shutting down...") + "forcibly shutting down..." } + stoppedPromise.complete(confirmation.map(_ => Done)) + ServerStopConfirmed(msg).toJson.compactPrint } - override def onVerifyPost(vr: Requests.VerificationRequest): ToResponseMarshallable = { - val arg_list = getArgListFromArgString(vr.arg) + private[http] def handleVerifyPost(arg: String): String = { + val arg_list = getArgListFromArgString(arg) val file: String = arg_list.last val arg_list_partial: List[String] = arg_list.dropRight(1) if (!validateViperFile(file)) { - return VerificationRequestReject("File not found") + return VerificationRequestReject("File not found").toJson.compactPrint } val backend = try { ViperBackendConfig(arg_list_partial) } catch { case _: IllegalArgumentException => - globalLogger.error(s"Invalid arguments: ${vr.arg} " + + globalLogger.error(s"Invalid arguments: $arg " + s"You need to specify the verification backend, e.g., `silicon [args]`") - return VerificationRequestReject("Invalid arguments for backend.") + return VerificationRequestReject("Invalid arguments for backend.").toJson.compactPrint } val ast_id = requestAst(file, backend) val ver_id = verifyWithAstJob(file, ast_id, backend) + VerificationRequestAccept(ast_id, ver_id).toJson.compactPrint + } - VerificationRequestAccept(ast_id, ver_id) + private[http] def streamAst(id: Int): cask.Response[geny.Writable] = { + val ast_id = AstJobId(id) + ast_jobs.lookupJob(ast_id) match { + case Some(handle_future) => + val handle = scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf) + jsonLineResponse(handle.stream.iterator) + case None => + textJsonResponse(VerificationRequestReject(s"The verification job #$id does not exist.").toJson.compactPrint) + } } - override def unpackMessages(s: Source[Envelope, NotUsed]): ToResponseMarshallable = { - import viper.server.frontends.http.jsonWriters.ViperIDEProtocol._ - val src_message: Source[Message, NotUsed] = s.map(e => unpack(e)) - src_message + private[http] def streamVerify(id: Int): cask.Response[geny.Writable] = { + val ver_id = VerJobId(id) + ver_jobs.lookupJob(ver_id) match { + case None => + textJsonResponse(verificationRequestRejectionString(id, JobNotFoundException)) + case Some(handle_future) => + val ver_handle = scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf) + val ast_id = ver_handle.prev_job_id + val ast_iter: Iterator[Envelope] = ast_id.flatMap(id => ast_jobs.lookupJob(id)) match { + case Some(astFut) => + val astHandle = scala.concurrent.Await.result(astFut, scala.concurrent.duration.Duration.Inf) + astHandle.stream.iterator + case None => Iterator.empty + } + val ver_iter: Iterator[Envelope] = ver_handle match { + case VerHandle(null, null, _) => Iterator.empty + case _ => ver_handle.stream.iterator + } + jsonLineResponse(ast_iter ++ ver_iter) + } } - override def verificationRequestRejection(jid: Int, e: Throwable): ToResponseMarshallable = { - e match { - case JobNotFoundException => - globalLogger.error(s"The verification job #$jid does not exist.") - VerificationRequestReject(s"The verification job #$jid does not exist.") - case AstConstructionFailureException => - globalLogger.error(s"The verification job #$jid could not be created since the AST is inconsistent.") - VerificationRequestReject(s"The verification job #$jid could not be created since the AST is inconsistent.") + private[http] def handleDiscard(id: Int): String = { + val ver_id = VerJobId(id) + ver_jobs.lookupJob(ver_id) match { + case Some(handle_future) => + scala.util.Try(scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf)) match { + case Success(handle) => + val msg = formatInterruptResult(ver_id, handle.execution.cancel()) + globalLogger.info(s"The verification job #$id was successfully stopped.") + JobDiscardAccept(msg).toJson.compactPrint + case Failure(_) => + JobDiscardReject(s"The verification job #$id does not exist.").toJson.compactPrint + } case _ => - globalLogger.error(s"The verification job #$jid resulted in a terrible error: $e") - VerificationRequestReject(s"The verification job #$jid resulted in a terrible error: $e") + JobDiscardReject(s"The verification job #$id does not exist.").toJson.compactPrint } } - override def discardJobConfirmation(jid: Int, msg: String): ToResponseMarshallable = { - globalLogger.info(s"The verification job #$jid was successfully stopped.") - JobDiscardAccept(msg) - } - - override def discardJobRejection(jid: Int): ToResponseMarshallable = { - globalLogger.error(s"The verification job #$jid does not exist.") - JobDiscardReject(s"The verification job #$jid does not exist.") - } - - def AdditionalViperServerRoute(): Route = path("cache" / "flush") { - /** - * Send GET request to "/cache/flush". - * - * This will invalidate the entire cache. - * - * Use case: - * - Client decided to re-verify several files from scratch. - */ - get { - flushCache() - complete( CacheFlushAccept(s"The cache has been flushed successfully.") ) - }~ path("cache" / "flush") { - /** - * Send POST request to "/cache/flush". - * - * This will invalidate the cache for the tool and file specified. - * - * Use case: - * - Client decided to re-verify the entire file from scratch. - */ - post { - entity(as[CacheResetRequest]) { - r => - ViperCache.forgetFile(r.backend, r.file) match { - case Some(_) => - globalLogger.info(s"The cache for tool (${r.backend}) for file (${r.file}) has been flushed successfully.") - complete( CacheFlushAccept(s"The cache for tool (${r.backend}) for file (${r.file}) has been flushed successfully.") ) - case None => - globalLogger.error(s"The cache does not exist for tool (${r.backend}) for file (${r.file}).") - complete( CacheFlushReject(s"The cache does not exist for tool (${r.backend}) for file (${r.file}).") ) - } - } + private[http] def handleCacheFlushAll(): String = { + flushCache() + CacheFlushAccept(s"The cache has been flushed successfully.").toJson.compactPrint + } + + private[http] def handleCacheFlushFile(backend: String, file: String): String = { + ViperCache.forgetFile(backend, file) match { + case Some(_) => + globalLogger.info(s"The cache for tool ($backend) for file ($file) has been flushed successfully.") + CacheFlushAccept(s"The cache for tool ($backend) for file ($file) has been flushed successfully.").toJson.compactPrint + case None => + globalLogger.error(s"The cache does not exist for tool ($backend) for file ($file).") + CacheFlushReject(s"The cache does not exist for tool ($backend) for file ($file).").toJson.compactPrint + } + } + + private[http] def handleAlloy(arg: String, solver: String): String = { + try { + val reporter: A4Reporter = new A4Reporter() + val world = CompUtil.parseEverything_fromString(reporter, arg) + + val options: A4Options = new A4Options() + options.solver = A4Options.SatSolver.parse(solver) + options.skolemDepth = 1 + options.noOverflow = true + options.unrolls = -1 + + val commands = world.getAllCommands + if (commands.size() != 1) { + globalLogger.error(s"Expected only one command, but got ${commands.size()}") + return AlloyGenerationRequestReject(s"Expected only one command, but got ${commands.size()}").toJson.compactPrint } - } ~ path("alloy") { - /** - * Send POST request to "/alloy". - * - * This will generate an instance of the given model. - */ - post { - object AlloyRequest extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol { - case class AlloyGenerationRequest(arg: String, solver: String) - implicit val generateStuff: RootJsonFormat[AlloyRequest.AlloyGenerationRequest] = jsonFormat2(AlloyGenerationRequest.apply) - } + val command = commands.get(0) + val solution = TranslateAlloyToKodkod.execute_command(reporter, world.getAllReachableSigs, command, options) + if (solution.satisfiable()) { + globalLogger.info("Model is satisfiable") + AlloyGenerationRequestComplete(solution).toJson.compactPrint + } else { + globalLogger.info(s"Model could not be satisfied.") + AlloyGenerationRequestReject(s"Model could not be satisfied.").toJson.compactPrint + } + } catch { + case e: Throwable => + globalLogger.error(s"An exception occurred during model-generation:\n${e.toString}") + AlloyGenerationRequestReject(s"An exception occurred during model-generation:\n${e.toString}").toJson.compactPrint + } + } - entity(as[AlloyRequest.AlloyGenerationRequest]) { r => - try { - val reporter: A4Reporter = new A4Reporter() - - val world = CompUtil.parseEverything_fromString(reporter, r.arg) - - val options: A4Options = new A4Options() - options.solver = A4Options.SatSolver.parse(r.solver) - options.skolemDepth = 1 - options.noOverflow = true - options.unrolls = -1 - - val commands = world.getAllCommands - if (commands.size() != 1) { - globalLogger.error(s"Expected only one command, but got ${commands.size()}") - complete( AlloyGenerationRequestReject(s"Expected only one command, but got ${commands.size()}") ) - } - val command = commands.get(0) - val solution = TranslateAlloyToKodkod.execute_command(reporter, world.getAllReachableSigs, command, options) - if (solution.satisfiable()) { - globalLogger.info("Model is satisfiable") - complete( AlloyGenerationRequestComplete(solution) ) - } else { - globalLogger.info(s"Model could not be satisfied.") - complete( AlloyGenerationRequestReject(s"Model could not be satisfied.") ) - } - } catch { - case e: Throwable => - globalLogger.error(s"An exception occurred during model-generation:\n${e.toString}") - complete( AlloyGenerationRequestReject(s"An exception occurred during model-generation:\n${e.toString}") ) + private def verificationRequestRejectionString(jid: Int, e: Throwable): String = e match { + case JobNotFoundException => + globalLogger.error(s"The verification job #$jid does not exist.") + VerificationRequestReject(s"The verification job #$jid does not exist.").toJson.compactPrint + case AstConstructionFailureException => + globalLogger.error(s"The verification job #$jid could not be created since the AST is inconsistent.") + VerificationRequestReject(s"The verification job #$jid could not be created since the AST is inconsistent.").toJson.compactPrint + case _ => + globalLogger.error(s"The verification job #$jid resulted in a terrible error: $e") + VerificationRequestReject(s"The verification job #$jid resulted in a terrible error: $e").toJson.compactPrint + } + + private def jsonLineResponse(envelopes: Iterator[Envelope]): cask.Response[geny.Writable] = { + val writable = new geny.Writable { + override def writeBytesTo(out: java.io.OutputStream): Unit = { + val pw = new java.io.PrintWriter(new java.io.OutputStreamWriter(out, "UTF-8")) + try { + var first = true + for (env <- envelopes) { + if (!first) pw.print('\n') + else first = false + pw.print(unpack(env).toJson.compactPrint) + pw.flush() } + } finally { + pw.flush() } } + override def httpContentType: Option[String] = Some("application/json") + } + cask.Response(data = writable, statusCode = 200, headers = Seq("Content-Type" -> "application/json")) + } + + private def textJsonResponse(body: String): cask.Response[geny.Writable] = { + val writable = new geny.Writable { + override def writeBytesTo(out: java.io.OutputStream): Unit = { + out.write(body.getBytes("UTF-8")) + } + override def httpContentType: Option[String] = Some("application/json") + } + cask.Response(data = writable, statusCode = 200, headers = Seq("Content-Type" -> "application/json")) + } +} + +/** cask routes for the HTTP frontend. Annotations are evaluated by cask macros + * which require this be a concrete class with `initialize()` called. + */ +class ViperCaskRoutes(server: ViperHttpServer) extends cask.MainRoutes { + override def host: String = "localhost" + override def port: Int = server.port + + @cask.get("/exit") + def exit(): cask.Response[geny.Writable] = jsonString(server.handleExit()) + + @cask.post("/verify") + def verify(req: cask.Request): cask.Response[geny.Writable] = { + val body = req.text().parseJson.asJsObject + val arg = body.fields("arg").asInstanceOf[JsString].value + jsonString(server.handleVerifyPost(arg)) + } + + @cask.get("/ast/:id") + def ast(id: Int): cask.Response[geny.Writable] = server.streamAst(id) + + @cask.get("/verify/:id") + def verifyResult(id: Int): cask.Response[geny.Writable] = server.streamVerify(id) + + @cask.get("/discard/:id") + def discard(id: Int): cask.Response[geny.Writable] = jsonString(server.handleDiscard(id)) + + @cask.get("/cache/flush") + def cacheFlushAll(): cask.Response[geny.Writable] = jsonString(server.handleCacheFlushAll()) + + @cask.post("/cache/flush") + def cacheFlushFile(req: cask.Request): cask.Response[geny.Writable] = { + val body = req.text().parseJson.asJsObject + val backend = body.fields("backend").asInstanceOf[JsString].value + val file = body.fields("file").asInstanceOf[JsString].value + jsonString(server.handleCacheFlushFile(backend, file)) + } + + @cask.post("/alloy") + def alloy(req: cask.Request): cask.Response[geny.Writable] = { + val body = req.text().parseJson.asJsObject + val arg = body.fields("arg").asInstanceOf[JsString].value + val solver = body.fields("solver").asInstanceOf[JsString].value + jsonString(server.handleAlloy(arg, solver)) + } + + private def jsonString(body: String): cask.Response[geny.Writable] = { + val writable = new geny.Writable { + override def writeBytesTo(out: java.io.OutputStream): Unit = { + out.write(body.getBytes("UTF-8")) + } + override def httpContentType: Option[String] = Some("application/json") } + cask.Response(data = writable, statusCode = 200, headers = Seq("Content-Type" -> "application/json")) } + + initialize() } diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala index 74b7791a..295312b6 100644 --- a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala +++ b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala @@ -6,10 +6,6 @@ package viper.server.frontends.http.jsonWriters -import akka.NotUsed -import akka.http.scaladsl.common.{EntityStreamingSupport, JsonEntityStreamingSupport} -import akka.stream.scaladsl.Flow -import akka.util.ByteString import edu.mit.csail.sdg.translator.A4Solution import spray.json.DefaultJsonProtocol import viper.server.vsi.{AstJobId, VerJobId} @@ -20,7 +16,7 @@ import viper.silver.ast._ import viper.silver.reporter._ import viper.silver.verifier.{ValueEntry, _} -object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol { +object ViperIDEProtocol extends DefaultJsonProtocol { import spray.json._ @@ -498,13 +494,4 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs })) }) - implicit val jsonStreamingSupport: JsonEntityStreamingSupport = { - val start = ByteString("") - val between = ByteString("\n") - val end = ByteString("") - - val compactArrayRendering: Flow[ByteString, ByteString, NotUsed] = Flow[ByteString].intersperse(start, between, end) - // Method withFramingRendererFlow: Java DSL overrides Scala DSL. Who knows why? Use .asJava as a workaround. - EntityStreamingSupport.json().withFramingRendererFlow( compactArrayRendering.asJava ) - } } diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala deleted file mode 100644 index 5f13c080..00000000 --- a/src/main/scala/viper/server/vsi/HTTP.scala +++ /dev/null @@ -1,234 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. -// -// Copyright (c) 2011-2020 ETH Zurich. - -package viper.server.vsi - -import akka.{Done, NotUsed} -import akka.http.scaladsl.Http -import akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport._ -import akka.http.scaladsl.marshalling.ToResponseMarshallable -import akka.http.scaladsl.server.Directives._ -import akka.http.scaladsl.server.Route -import akka.stream.scaladsl.Source - -import scala.concurrent.{Future, Promise} -import scala.util.{Failure, Success, Try} - -/** This trait contains the bear essentials required for an HTTP server. - * */ -sealed trait BasicHttp { - - /** Specifies the port through which the clients may access this server instance. - * - * The default port number tells the system to automatically pick an available port - * (depends on the implementation of the underlying socket library) - * */ - var port: Int = _ - - /** Must be implemented to return the routes defined for this server. - * */ - def routes(): Route -} - -/** This trait provides the functionality to add additional routes to an HTTP Server. - * */ -sealed trait CustomizableHttp extends BasicHttp { - - /** This method merges two given routes into one. - * */ - def addRoute(existingRoute: Route, newRoute: Route): Route = { - existingRoute ~ newRoute - } -} - -/** This trait extends a VerificationServer by providing common HTTP functionality. - * - * Examples for such functionality are: - * - * - Stopping a VerifiationServer. - * - Submitting verification requests. - * - Requesting results for verification requests. - * - * The VerificationServer-specific functionality will need to be implemented for each individual - * server. In particular, this means providing a protocol that returns the VerificationServer's - * responses as type [[ToResponseMarshallable]]. - * */ -trait VerificationServerHttp extends VerificationServer with CustomizableHttp { - import scala.language.postfixOps - - def setRoutes(): Route - - private val stoppedPromise: Promise[Done] = Promise() - var bindingFuture: Future[Http.ServerBinding] = _ - - /** - * The returned future completes as soon as the server has been started. Before completion, `port` will be set - * to the port number selected by the HTTP server. - * The returned future does NOT indicate when the server has stopped. Use the future returned by `stopped` instead. - */ - override def start(active_jobs: Int): Future[Done] = { - ast_jobs = new JobPool("AST-pool", active_jobs) - ver_jobs = new JobPool("Verification-pool", active_jobs) - bindingFuture = Http().newServerAt("localhost", port).bindFlow(setRoutes()) - bindingFuture.map { serverBinding => - val newPort = serverBinding.localAddress.getPort - if (port == 0) { - assert(newPort != 0, s"HTTP server should have selected a non-zero port but did not") - } else { - assert(port == newPort, s"HTTP server has selected a different port although a non-zero port has been specified") - } - port = newPort - isRunning = true - Done - } - } - - override protected def onExit(): Future[Unit] = { - if (bindingFuture == null) Future.unit - else bindingFuture.flatMap(_.unbind()).map(_ => ()) - } - - /** The returned future is completed when the server is stopped. - * Afterwards, the execution context can be terminated. - * This function cannot be called before calling `start`. */ - def stopped(): Future[Done] = { - stoppedPromise.future - } - - /** Implement VerificationServer- specific handling of server shutdown. - * (Response should depend on interruption state.) - * */ - def serverStopConfirmation(interruption_future: Try[List[String]]): ToResponseMarshallable - - /** Implement VerificationServer- specific handling of VerificationRequests. - * */ - def onVerifyPost(vr: Requests.VerificationRequest): ToResponseMarshallable - - /** Implement VerificationServer- specific handling of a request for streaming results. - * */ - def unpackMessages(s: Source[Envelope, NotUsed]): ToResponseMarshallable - - /** Implement VerificationServer- specific handling of a failed request for streaming results. - * */ - def verificationRequestRejection(jid: Int, e: Throwable): ToResponseMarshallable - - /** Implement VerificationServer- specific handling of a successful request for discarding a job. - * */ - def discardJobConfirmation(jid: Int, msg: String): ToResponseMarshallable - - /** Implement VerificationServer- specific handling of a failed request for for discarding a job. - * */ - def discardJobRejection(jid: Int): ToResponseMarshallable - - override final def routes(): Route = { - /** Send GET request to "/exit". - */ - path("exit") { - get { - // note that `stop` internally uses the `_termActor` that unbinds the server's port and terminates the execution context - onComplete(stop()) { err: Try[List[String]] => - stoppedPromise.complete(err.map(_ => Done)) - complete( serverStopConfirmation(err) ) - } - } - } - } ~ path("verify") { - /** Send POST request to "/verify". - */ - post { - entity(as[Requests.VerificationRequest]) { r => - complete(onVerifyPost(r)) - } - } - } ~ path("ast" / IntNumber) { id => - val ast_id = AstJobId(id) - get { - ast_jobs.lookupJob(ast_id) match { - case Some(handle_future) => - onComplete(handle_future) { - case Success(handle) => - val s: Source[Envelope, NotUsed] = Source.fromIterator(() => handle.stream.iterator) - complete(unpackMessages(s)) - case Failure(error) => - // TODO use AST-specific response - complete(verificationRequestRejection(id, error)) - } - case None => - // TODO use AST-specific response - complete(verificationRequestRejection(id, JobNotFoundException)) - } - } - } ~ path("verify" / IntNumber) { id => - /** Send GET request to "/verify/" where is a non-negative integer. - * must be an ID of an existing verification job. - */ - val ver_id = VerJobId(id) - get { - ver_jobs.lookupJob(ver_id) match { - case None => - /** Verification job with this ID is not found. */ - complete(verificationRequestRejection(id, JobNotFoundException)) - - case Some(handle_future) => - /** Combine the future AST and the future verification results. */ - onComplete(handle_future.flatMap((ver_handle: VerHandle) => { - /** If there exists a verification job, there should have existed - * (or should still exist) a corresponding AST construction job. */ - val ast_id: AstJobId = ver_handle.prev_job_id.get - - /** The AST construction job may have been cleaned up - * (if all of its messages were already consumed) */ - ast_jobs.lookupJob(ast_id) match { - case Some(ast_handle_fut) => - ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle)) - case None => - Future.successful((None, ver_handle)) - } - })) { - case Success((ast_handle_maybe, ver_handle)) => - val ver_source = ver_handle match { - case VerHandle(null, null, _) => - /** There were no messages produced during verification. */ - Source.empty[Envelope] - case _ => - Source.fromIterator(() => ver_handle.stream.iterator) - } - val ast_source = ast_handle_maybe match { - case None => - /** The AST messages were already consumed. */ - Source.empty[Envelope] - case Some(ast_handle) => - Source.fromIterator(() => ast_handle.stream.iterator) - } - val resulting_source = ver_source.prepend(ast_source) - complete(unpackMessages(resulting_source)) - - case Failure(error) => - complete(verificationRequestRejection(id, error)) - } - } - } - } ~ path("discard" / IntNumber) { id => - /** Send GET request to "/discard/" where is a non-negative integer. - * must be an ID of an existing verification job. - */ - val ver_id = VerJobId(id) - get { - ver_jobs.lookupJob(ver_id) match { - case Some(handle_future) => - onComplete(handle_future) { - case Success(handle) => - val msg = formatInterruptResult(ver_id, handle.execution.cancel()) - complete(discardJobConfirmation(id, msg)) - case Failure(_) => - complete(discardJobRejection(id)) - } - case _ => - complete(discardJobRejection(id)) - } - } - } -} \ No newline at end of file diff --git a/src/main/scala/viper/server/vsi/Protocol.scala b/src/main/scala/viper/server/vsi/Protocol.scala index 83d8e80a..bace727d 100644 --- a/src/main/scala/viper/server/vsi/Protocol.scala +++ b/src/main/scala/viper/server/vsi/Protocol.scala @@ -8,7 +8,7 @@ package viper.server.vsi import spray.json.{DefaultJsonProtocol, RootJsonFormat} -object Requests extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol { +object Requests extends DefaultJsonProtocol { case class VerificationRequest(arg: String) implicit val VerificationRequest_format: RootJsonFormat[VerificationRequest] = jsonFormat1(VerificationRequest.apply) diff --git a/src/test/scala/viper/server/core/ViperServerHttpSpec.scala b/src/test/scala/viper/server/core/ViperServerHttpSpec.scala index e3a16fb7..8d709cd0 100644 --- a/src/test/scala/viper/server/core/ViperServerHttpSpec.scala +++ b/src/test/scala/viper/server/core/ViperServerHttpSpec.scala @@ -6,148 +6,102 @@ package viper.server.core // // Copyright (c) 2011-2020 ETH Zurich. -import java.io.File -import java.nio.file.Paths - -import akka.http.scaladsl.common.{EntityStreamingSupport, JsonEntityStreamingSupport} -import akka.http.scaladsl.model.{StatusCodes, _} -import akka.http.scaladsl.testkit.{RouteTestTimeout, ScalatestRouteTest} -import akka.testkit.TestDuration import org.scalatest.wordspec.AnyWordSpec import org.scalatest.matchers.should.Matchers import org.scalatest.concurrent.TimeLimits import org.scalatest.time.{Seconds, Span} import viper.server.frontends.http.ViperHttpServer import viper.server.ViperConfig -import viper.server.vsi.Requests._ import scala.concurrent.Await import scala.concurrent.duration._ -class ViperServerHttpSpec extends AnyWordSpec with Matchers with ScalatestRouteTest with TimeLimits { - - import scala.language.postfixOps - implicit val jsonStreamingSupport: JsonEntityStreamingSupport = EntityStreamingSupport.json() - implicit val requestTimeput: RouteTestTimeout = RouteTestTimeout(10.second dilated) +class ViperServerHttpSpec extends AnyWordSpec with Matchers with TimeLimits { private val verificationContext: VerificationExecutionContext = new DefaultVerificationExecutionContext() private val viperServerHttp = { val config = new ViperConfig(IndexedSeq()) new ViperHttpServer(config)(verificationContext) - // note that the server is not yet started but is just initialized - // the first test case will then actually start it - } - - private val _routesUnderTest = viperServerHttp.routes() - - def printRequestResponsePair(req: String, res: String): Unit = { - println(s">>> ViperServer test request `$req` response in the following response: $res") } - // FIXME this does not work with SBT for some reason - def getResourcePath(vpr_file: String): String = { - val cross_platform_path = new File(vpr_file) getPath - val resource = getClass.getResource(cross_platform_path) - val fname = if (resource != null) { - val file = Paths.get(resource.toURI) - file.toString - } else { - // simulate absent file - val temp_file = File.createTempFile("ViperServer_testing", ".vpr") - val absent_fname = temp_file.getPath - temp_file.delete() - absent_fname - } - "\"" + fname + "\"" - } + // Started lazily on first test to set the bound port. + private def baseUrl: String = s"http://localhost:${viperServerHttp.port}" private val verifiableFile = "src/test/resources/viper/let.vpr" private val nonExistingFile = "2165e0fbd4b980436557b5a6f1a41f68.vpr" private val emptyFile = "src/test/resources/viper/empty.vpr" private val tool = "silicon" - private val testSimpleViperCode_cmd = s"$tool --disableCaching ${verifiableFile}" - private val testEmptyFile_cmd = s"$tool --disableCaching ${emptyFile}" + private val testSimpleViperCode_cmd = s"$tool --disableCaching $verifiableFile" + private val testEmptyFile_cmd = s"$tool --disableCaching $emptyFile" private val testEmptyFileWithCaching_cmd = s"$tool $emptyFile" - private val testNonExistingFile_cmd = s"$tool --disableCaching ${nonExistingFile}" + private val testNonExistingFile_cmd = s"$tool --disableCaching $nonExistingFile" + + private def postVerify(cmd: String): String = { + val body = s"""{"arg":${jsonString(cmd)}}""" + requests.post(s"$baseUrl/verify", data = body, headers = Map("Content-Type" -> "application/json")).text() + } + + private def jsonString(s: String): String = { + val sb = new StringBuilder("\"") + s.foreach { + case '"' => sb.append("\\\"") + case '\\' => sb.append("\\\\") + case '\n' => sb.append("\\n") + case '\r' => sb.append("\\r") + case '\t' => sb.append("\\t") + case c => sb.append(c) + } + sb.append("\"").toString + } "ViperServer" should { "eventually start" in { failAfter(Span(10, Seconds)) { val started = viperServerHttp.start() - // wait until server has been started: Await.result(started, Duration.Inf) } } s"start a verification process using `$tool` over a small Viper program" in { - Post("/verify", VerificationRequest(testSimpleViperCode_cmd)) ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"POST, /verify, $testSimpleViperCode_cmd", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should not include ("""File not found""") - } + val resp = postVerify(testSimpleViperCode_cmd) + resp should not include "File not found" } "respond with the result for process #0" in { - Get("/verify/0") ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"GET, /verify/0", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""") - } + val resp = requests.get(s"$baseUrl/verify/0").text() + resp should include(s""""kind":"overall","status":"success","verifier":"$tool"""") } s"start another verification process using `$tool` on an empty file" in { - Post("/verify", VerificationRequest(testEmptyFile_cmd)) ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"POST, /verify, $testEmptyFile_cmd", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should not include ("""File not found""") - } + val resp = postVerify(testEmptyFile_cmd) + resp should not include "File not found" } "respond with the result for process #1" in { - Get("/verify/1") ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"GET, /verify/1", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""") - } + val resp = requests.get(s"$baseUrl/verify/1").text() + resp should include(s""""kind":"overall","status":"success","verifier":"$tool"""") } s"start another verification process with caching enabled using `$tool` on an empty file (Issue #111)" in { - Post("/verify", VerificationRequest(testEmptyFileWithCaching_cmd)) ~> _routesUnderTest ~> check { - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should not include ("""File not found""") - } + val resp = postVerify(testEmptyFileWithCaching_cmd) + resp should not include "File not found" } "respond with the result for process #2 that should not contain an exception report (Issue #111)" in { - Get("/verify/2") ~> _routesUnderTest ~> check { - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""") - responseAs[String] should not include(s""""msg_type":"exception_report"""") - } + val resp = requests.get(s"$baseUrl/verify/2").text() + resp should include(s""""kind":"overall","status":"success","verifier":"$tool"""") + resp should not include """"msg_type":"exception_report"""" } s"start another verification process using `$tool` on an non-existent file" in { - Post("/verify", VerificationRequest(testNonExistingFile_cmd)) ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"POST, /verify, $testEmptyFile_cmd", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - responseAs[String] should include (s"not found") - } + val resp = postVerify(testNonExistingFile_cmd) + resp should include("not found") } "stop all running executions and terminate self" in { - Get("/exit") ~> _routesUnderTest ~> check { - //printRequestResponsePair(s"GET, /exit", responseAs[String]) - status should ===(StatusCodes.OK) - contentType should ===(ContentTypes.`application/json`) - } + val resp = requests.get(s"$baseUrl/exit").text() + resp should include("shutting down") } "should eventually stop" in { From 1f23b69997467bbe0717159a9c923bba8d7d3b90 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 6 May 2026 11:27:51 +0200 Subject: [PATCH 08/22] Drop remaining akka deps and dead config --- build.sbt | 12 +- src/main/resources/application.conf | 77 ---------- src/main/scala/viper/server/ViperConfig.scala | 9 -- .../core/VerificationExecutionContext.scala | 51 ++----- .../viper/server/core/ViperCoreServer.scala | 20 +-- .../frontends/http/ViperHttpServer.scala | 15 +- .../server/frontends/http/ViperRequests.scala | 25 ---- .../frontends/lsp/ViperServerService.scala | 36 +++-- .../viper/server/vsi/VerificationServer.scala | 138 ++++++------------ .../server/core/AstGenerationTests.scala | 3 +- .../viper/server/core/CoreServerSpec.scala | 69 ++------- .../viper/server/core/ReformatterTest.scala | 3 +- 12 files changed, 105 insertions(+), 353 deletions(-) delete mode 100644 src/main/resources/application.conf delete mode 100644 src/main/scala/viper/server/frontends/http/ViperRequests.scala diff --git a/build.sbt b/build.sbt index 23e9e2dd..e42581cf 100644 --- a/build.sbt +++ b/build.sbt @@ -25,17 +25,11 @@ lazy val server = (project in file(".")) fork := true, libraryDependencies += "net.liftweb" %% "lift-json" % "3.5.0", - libraryDependencies += "com.typesafe.akka" %% "akka-actor" % "2.6.10", - libraryDependencies += "com.typesafe.akka" %% "akka-http-spray-json" % "10.2.1", - libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.6.10", - libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test, - libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test, libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol - libraryDependencies += "com.lihaoyi" %% "cask" % "0.9.5", // Lightweight HTTP server (replacing Akka HTTP) - libraryDependencies += "com.lihaoyi" %% "upickle" % "4.0.2", // JSON marshalling for cask + libraryDependencies += "com.lihaoyi" %% "cask" % "0.9.5", // Lightweight HTTP server (replaces Akka HTTP) libraryDependencies += "io.spray" %% "spray-json" % "1.3.6", // JSON AST and serialization (existing marshallers) - // upickle and geny pull conflicting transitive versions across the dependency tree; - // accept the newer ones since they are the consumers' preferred versions. + // upickle is pulled transitively by cask. Silver depends on an older + // upickle so allow the newer version (cask's) to win. libraryDependencySchemes += "com.lihaoyi" %% "upickle" % "always", libraryDependencySchemes += "com.lihaoyi" %% "upickle-core" % "always", libraryDependencySchemes += "com.lihaoyi" %% "upickle-implicits" % "always", diff --git a/src/main/resources/application.conf b/src/main/resources/application.conf deleted file mode 100644 index 15f31809..00000000 --- a/src/main/resources/application.conf +++ /dev/null @@ -1,77 +0,0 @@ -# This Source Code Form is subject to the terms of the Mozilla Public -# License, v. 2.0. If a copy of the MPL was not distributed with this -# file, You can obtain one at http://mozilla.org/MPL/2.0/. -# -# Copyright (c) 2011-2020 ETH Zurich. - -akka { - - # loglevel = "DEBUG" - - stream { - materializer { - # Cleanup leaked publishers and subscribers when they are not used within a given - # deadline - subscription-timeout { - # when the subscription timeout is reached one of the following strategies on - # the "stale" publisher: - # cancel - cancel it (via `onError` or subscribing to the publisher and - # `cancel()`ing the subscription right away - # warn - log a warning statement about the stale element (then drop the - # reference to it) - # noop - do nothing (not recommended) - mode = warn - - # time after which a subscriber / publisher is considered stale and eligible - # for cancelation (see `akka.stream.subscription-timeout.mode`) - timeout = 5s # 5s is the default - - # in the ViperServer case, this setting is relevant e.g. for streaming the messages - # that are in the queue. In particular, the queue would get completed (when the mode is set - # to `cancel`, which is Akka's default) if the messages do not get streamed within the - # timeout. Trying to enqueue any message into the queue after the timeout has been triggered - # results in exceptions. LA 15.5.2022: I've observed this for input files whose parsing takes - # longer than the configured timeout and using viper_client that only starts streaming messages - # after 10s (also more than the configured timeout). - } - } - } - - http { - - server { - # The default value of the `Server` header to produce if no - # explicit `Server`-header was included in a response. - # If this value is the empty string and no header was included in - # the request, no `Server` header will be rendered at all. - server-header = akka-http/${akka.http.version} - - # "PREVIEW" features that are not yet fully production ready. - # These flags can can change or be removed between patch releases. - preview { - # ONLY WORKS WITH `bindAndHandleAsync` (currently) - # - # If this setting is enabled AND the akka-http2-support is found - # on the classpath the usual Http().bind... method calls will bind - # using HTTP/2. Please note that you must configure HTTPS while doing so. - enable-http2 = off - } - - # The time after which an idle connection will be automatically closed. - # Set to `infinite` to completely disable idle connection timeouts. - idle-timeout = infinite - - # Defines the default time period within which the application has to - # produce an HttpResponse for any given HttpRequest it received. - # The timeout begins to run when the *end* of the request has been - # received, so even potentially long uploads can have a short timeout. - # Set to `infinite` to completely disable request timeout checking. - # - # If this setting is not `infinite` the HTTP server layer attaches a - # `Timeout-Access` header to the request, which enables programmatic - # customization of the timeout period and timeout response for each - # request individually. - request-timeout = 5 s - } - } -} \ No newline at end of file diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala index 37a23162..6b6b0ceb 100644 --- a/src/main/scala/viper/server/ViperConfig.scala +++ b/src/main/scala/viper/server/ViperConfig.scala @@ -119,15 +119,6 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) { noshort = false, hidden = false) - val actorCommunicationTimeout: ScallopOption[Int] = opt[Int]("actorCommunicationTimeout", 'a', - descr = ("Specifies the maximal amount of time that actors will wait when communicating requesting messages from other actors." - + s"The number is of unit milliseconds and must be positive integer." - + "If the option is omitted, a default timeout of 5000 milliseconds will be set."), - default = Some(5000), - noshort = false, - hidden = true - ) - val maximumActiveJobs: ScallopOption[Int] = opt[Int]("maximumActiveJobs", 'm', descr = ("Specifies the maximal amount of jobs that may run concurrently." + s"The number must be positive integer." diff --git a/src/main/scala/viper/server/core/VerificationExecutionContext.scala b/src/main/scala/viper/server/core/VerificationExecutionContext.scala index b7e9b0f7..90c7016b 100644 --- a/src/main/scala/viper/server/core/VerificationExecutionContext.scala +++ b/src/main/scala/viper/server/core/VerificationExecutionContext.scala @@ -9,43 +9,34 @@ package viper.server.core import java.util.concurrent.{ExecutorService, Executors, ScheduledExecutorService, ThreadFactory, TimeUnit} import java.util.{concurrent => java_concurrent} -import akka.actor.ActorSystem - -import scala.concurrent.duration.FiniteDuration -import scala.concurrent.{Await, ExecutionContext, ExecutionContextExecutorService, Future} +import scala.concurrent.{ExecutionContext, ExecutionContextExecutorService, Future} trait VerificationExecutionContext extends ExecutionContext { def executorService: ExecutorService - def actorSystem: ActorSystem def scheduler: ScheduledExecutorService def submit(r: Runnable): java_concurrent.Future[_] - /** terminate executor and actor system */ + /** Terminate executor and scheduler. */ def terminate(timeoutMSec: Long = 1000): Unit - /** restart actor system */ + /** Restart (no-op now that the actor system is gone; retained for API + * compatibility with prior consumers). + */ def restart(): Future[Unit] } object DefaultVerificationExecutionContext { - // at least 3 threads seem to be needed if the actor system is also using the same thread pool. Otherwise, if the actor - // system is started using its own (default) executor, a different number of thread might be sufficient. - // actor system with the default executor like `ActorSystem(actorSystemName)`) - /** minimum number of threads needed for the thread pool in the DefaultVerificationExecutionContext */ + /** Minimum number of threads needed for the thread pool. */ val minNumberOfThreads: Int = 3 } /** - * This class provides a default verification execution context based on a fixed thread pool. The actor system is - * not using that thread pool but is using akka's default executor. (There have been issues starting the (default) - * akka logger in the unit tests because of some blocking behavior of the thread pool when sharing the same thread - * pool.) - * The thread pool uses as many threads as there are processors available (but at least 2). Each started thread - * gets a stack of 128MB. - * The purpose of a verification execution context is that it can be passed to ViperServer and ViperServer will - * use the provided verification execution context whenever an actor or any task requiring a separate thread is - * executed. + * Default verification execution context backed by a fixed thread pool. + * + * The pool uses as many threads as there are processors available (but at + * least 2). Each started thread gets a stack of 128MB. A separate + * single-threaded daemon `ScheduledExecutorService` handles delayed + * callbacks (used to be Akka schedulers). */ -class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_System", - threadNamePrefix: String = "thread", +class DefaultVerificationExecutionContext(threadNamePrefix: String = "thread", threadPoolSize: Option[Int] = None) extends VerificationExecutionContext { protected lazy val nThreads: Int = threadPoolSize.getOrElse( Math.max(DefaultVerificationExecutionContext.minNumberOfThreads, Runtime.getRuntime.availableProcessors())) @@ -79,28 +70,14 @@ class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_Syste override def reportFailure(cause: Throwable): Unit = context.reportFailure(cause) - private var system: Option[ActorSystem] = Some(ActorSystem(actorSystemName)) - override def actorSystem: ActorSystem = system.getOrElse(throw new IllegalStateException(s"actor system has been terminated")) - override def submit(r: Runnable): java_concurrent.Future[_] = context.submit(r) @throws(classOf[InterruptedException]) override def terminate(timeoutMSec: Long = 1000): Unit = { - val oldSystem = actorSystem - system = None - Await.ready(oldSystem.terminate(), FiniteDuration(timeoutMSec, TimeUnit.MILLISECONDS)) schedulerService.shutdownNow() executorService.shutdown() executorService.awaitTermination(timeoutMSec, TimeUnit.MILLISECONDS) } - override def restart(): Future[Unit] = { - // the executor service stays untouched, i.e. only the actor system is restarted - val oldSystem = actorSystem - system = None - oldSystem.terminate().map(_ => { - // set new actor system: - system = Some(ActorSystem(actorSystemName)) - })(this) - } + override def restart(): Future[Unit] = Future.unit } diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala index 0f4508fc..dba4cb31 100644 --- a/src/main/scala/viper/server/core/ViperCoreServer.scala +++ b/src/main/scala/viper/server/core/ViperCoreServer.scala @@ -6,9 +6,6 @@ package viper.server.core -import akka.Done -import akka.actor.ActorRef -import akka.util.Timeout import ch.qos.logback.classic.Logger import viper.server.ViperConfig import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer} @@ -16,9 +13,7 @@ import viper.silver.ast.Program import viper.silver.ast.utility.FileLoader import viper.silver.logger.ViperLogger -import scala.concurrent.duration._ import scala.concurrent.Future -import scala.language.postfixOps abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: VerificationExecutionContext) extends VerificationServer with ViperPost { @@ -26,8 +21,6 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V // --- VCS : Configuration --- - override lazy val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds) - /** global logger that should be used for the server's entire lifetime. Log messages are reported to the global logger as well as local one (if they exist) */ val globalLogger: Logger = getGlobalLogger(config) @@ -51,11 +44,11 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V * This function must be called before any other. Calling any other function before this one * will result in an IllegalStateException. */ - def start(): Future[Done] = { + def start(): Future[Unit] = { ViperCache.initialize(globalLogger, config.backendSpecificCache(), config.cacheFile.toOption) start(config.maximumActiveJobs()) map { _ => globalLogger.info(s"ViperCoreServer has started.") - Done + () } } @@ -125,15 +118,6 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V ver_id } - override def streamMessages(jid: VerJobId, clientActor: ActorRef, include_ast: Boolean): Option[Future[Done]] = { - globalLogger.info(s"Streaming results for job #${jid.id}.") - super.streamMessages(jid, clientActor, include_ast) - } - override def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = { - globalLogger.info(s"Streaming results for job #${jid.id}.") - super.streamMessages(jid, clientActor) - } - def flushCache(localLogger: Option[Logger] = None): Boolean = { val logger = combineLoggers(localLogger) if(!isRunning) { diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala index b9c626c0..db64ab02 100644 --- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala +++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala @@ -7,7 +7,6 @@ package viper.server.frontends.http import java.net.InetSocketAddress -import akka.Done import edu.mit.csail.sdg.alloy4.A4Reporter import edu.mit.csail.sdg.parser.CompUtil import edu.mit.csail.sdg.translator.{A4Options, TranslateAlloyToKodkod} @@ -27,19 +26,19 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex var port: Int = 0 private var undertow: Undertow = _ - private val stoppedPromise: Promise[Done] = Promise() + private val stoppedPromise: Promise[Unit] = Promise() private val routes: ViperCaskRoutes = new ViperCaskRoutes(this) - override def start(): Future[Done] = { + override def start(): Future[Unit] = { port = config.port.toOption.getOrElse(0) super.start().map { _ => println(s"ViperServer online at http://localhost:$port") - Done + () }(executor) } - override def start(active_jobs: Int): Future[Done] = { + override def start(active_jobs: Int): Future[Unit] = { ast_jobs = new JobPool("AST-pool", active_jobs) ver_jobs = new JobPool("Verification-pool", active_jobs) undertow = Undertow.builder() @@ -50,7 +49,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex val boundAddr = undertow.getListenerInfo.get(0).getAddress.asInstanceOf[InetSocketAddress] port = boundAddr.getPort isRunning = true - Future.successful(Done) + Future.unit } override protected def onExit(): Future[Unit] = { @@ -66,7 +65,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex } /** Future that resolves once the server has been shut down via /exit. */ - def stopped(): Future[Done] = stoppedPromise.future + def stopped(): Future[Unit] = stoppedPromise.future /** Triggered by the `/exit` route. Stops jobs, unbinds the listener, then * completes the `stopped()` future. @@ -83,7 +82,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex println("forcibly shutting down...") "forcibly shutting down..." } - stoppedPromise.complete(confirmation.map(_ => Done)) + stoppedPromise.complete(confirmation.map(_ => ())) ServerStopConfirmed(msg).toJson.compactPrint } diff --git a/src/main/scala/viper/server/frontends/http/ViperRequests.scala b/src/main/scala/viper/server/frontends/http/ViperRequests.scala deleted file mode 100644 index 1825ac52..00000000 --- a/src/main/scala/viper/server/frontends/http/ViperRequests.scala +++ /dev/null @@ -1,25 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. -// -// Copyright (c) 2011-2020 ETH Zurich. - -package viper.server.frontends.http - -import spray.json.{DefaultJsonProtocol, RootJsonFormat} - -object ViperRequests extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol { - - // Legacy verification request format. - // TODO: use JSon for submitting verification requests. - case class VerificationRequest(arg: String) - implicit val VerificationRequest_format: RootJsonFormat[VerificationRequest] = jsonFormat1(VerificationRequest.apply) - - case class CacheResetRequest(backend: String, file: String) - implicit val CacheResetRequest_format: RootJsonFormat[CacheResetRequest] = jsonFormat2(CacheResetRequest.apply) - - // Other requests go below this line. - case class AlloyGenerationRequest(arg: String, solver: String) - - implicit val generateStuff = jsonFormat2(AlloyGenerationRequest.apply) -} diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index a018d499..7c2e3fea 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -18,7 +18,6 @@ import viper.silver.parser.ReformatPrettyPrinter import viper.silver.ast.utility.FileLoader import scala.concurrent.Future -import scala.util.{Failure, Success} class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext) extends ViperCoreServer(config)(executor) with DefaultVerificationServerStart { @@ -74,13 +73,8 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve def startStreamingAst(jid: AstJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { val logger = combineLoggers(localLogger) logger.debug(s"Sending ast construct request to ViperServer...") - messageEnvelopeSource(jid).map(_.flatMap { case (ast_handle, ast_source) => - val done = ast_source.map(e => unpack(e)).runForeach(handler.handleMessage) - done.onComplete { - case Success(_) => handler.onStreamSuccess() - case Failure(e) => handler.onStreamFailure(e) - } - ast_handle.stream.watchCompletion + messageEnvelopes(jid).map(_.flatMap { case (_, iter) => + drainIteratorTo(iter, handler) }) } def startStreamingVer(jid: VerJobId, handler: RelayHandler, localLogger: Option[Logger] = None): Option[Future[Unit]] = { @@ -93,16 +87,28 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve } private def runStreamWithHandler(jid: VerJobId, handler: RelayHandler, include_ast: Boolean): Option[Future[Unit]] = { - messageEnvelopeSource(jid, include_ast).map(_.flatMap { case (ver_handle, combined_source) => - val done = combined_source.map(e => unpack(e)).runForeach(handler.handleMessage) - done.onComplete { - case Success(_) => handler.onStreamSuccess() - case Failure(e) => handler.onStreamFailure(e) - } - ver_handle.stream.watchCompletion + messageEnvelopes(jid, include_ast).map(_.flatMap { case (_, iter) => + drainIteratorTo(iter, handler) }) } + /** Drains `iter` on the executor's thread pool, dispatching messages to + * `handler`. The returned future completes when the iterator is exhausted + * or fails, after the corresponding terminal handler callback has run. + */ + private def drainIteratorTo(iter: Iterator[viper.server.vsi.Envelope], handler: RelayHandler): Future[Unit] = { + Future { + try { + for (env <- iter) handler.handleMessage(unpack(env)) + handler.onStreamSuccess() + } catch { + case e: Throwable => + handler.onStreamFailure(e) + throw e + } + }(executor) + } + def stopVerification(jid: VerJobId, localLogger: Option[Logger] = None): Future[Boolean] = { val logger = combineLoggers(localLogger) ver_jobs.lookupJob(jid) match { diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index 38ea5a19..2ccb4630 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -6,10 +6,6 @@ package viper.server.vsi -import akka.{Done, NotUsed} -import akka.actor.{ActorRef, ActorSystem, Status} -import akka.stream.scaladsl.{Sink, Source} -import akka.util.Timeout import viper.server.core.VerificationExecutionContext import scala.concurrent.Future @@ -21,28 +17,17 @@ abstract class VerificationServerException extends Exception case object JobNotFoundException extends VerificationServerException abstract class AstConstructionException extends VerificationServerException -/** This trait provides state and process management functionality for verification servers. +/** State and process management for verification servers. * - * The server runs on Akka's actor system. This means that the entire server's state - * and process management are run by actors. The 3 actors in charge are: - * - * 1) Job Actor - * 2) Queue Actor - * 3) Terminator Actor - * - * The first two actors manage individual verification processes. I.e., on - * initializeVerificationProcess() and instance of each actor is created. The JobActor launches - * the actual VerificationTask, while the QueueActor acts as a middleman for communication - * between a VerificationTask's backend and the server. The Terminator Actor is in charge of - * terminating both individual processes and the server. + * Each booked job owns a `JobExecution` (cancellable Future-task wrapper) and an + * `EnvelopeStream` over which the backend streams messages back to consumers. + * Two pools (AST construction, verification) are managed in parallel. */ trait VerificationServer extends Post { type AST implicit val executor: VerificationExecutionContext - implicit val system: ActorSystem = executor.actorSystem - implicit def askTimeout: Timeout /** Hook invoked from `stop()` after all jobs have been interrupted. Default * is a no-op. The HTTP frontend overrides this to unbind its server port. @@ -59,13 +44,12 @@ trait VerificationServer extends Post { /** Configures an instance of VerificationServer. * - * This function must be called before any other. Calling any other function before this one - * will result in an IllegalStateException. - * The returned future resolves when the server has been started. - * - * Note that a default implementation is provided in DefaultVerificationServerStart + * Calling any other function before this one will result in an + * IllegalStateException. The returned future resolves when the server has + * been started. A default implementation is provided in + * `DefaultVerificationServerStart`. */ - def start(active_jobs: Int): Future[Done] + def start(active_jobs: Int): Future[Unit] protected def initializeProcess[S <: JobId, T <: JobHandle : ClassTag] (pool: JobPool[S, T], @@ -79,14 +63,12 @@ trait VerificationServer extends Post { require(pool.newJobsAllowed) - /** Ask the pool to book a new job using the above function - * to construct Future[JobHandle] and Promise[AST] later on. */ pool.bookNewJob((new_jid: S) => task_maybe_fut.flatMap((task_maybe: Option[MessageStreamingTask[_]]) => { task_maybe match { case None => - /** If there's no task, that means their prerequisite tasks haven't produced usable artifacts. - * The sole purpose of this task is hence to hold the identifier of its predecessor. - * We should remove this task from the job pool. */ + /** No task means a prerequisite produced no usable artifact; the placeholder + * just holds the predecessor's id and is removed from the pool. + */ pool.discardJob(new_jid) new_jid match { case _: VerJobId => @@ -94,12 +76,10 @@ trait VerificationServer extends Post { } case Some(task) => val stream = new EnvelopeStream() - task.setStream(stream) val execution = new JobExecution(task.futureTask) - /** Register cleanup task. */ stream.watchCompletion.onComplete(_ => { if (discardOnCompletion) { pool.discardJob(new_jid) @@ -127,8 +107,7 @@ trait VerificationServer extends Post { }).recover({ case e: AstConstructionException => - // If the AST construction phase failed, remove the verification job handle - // from the corresponding pool. + // If the AST construction phase failed, drop the verification job handle. val msg = s"AST construction job ${prev_job_id_maybe.get} resulted in a failure: $e" println(msg) pool.discardJob(new_jid) @@ -151,10 +130,7 @@ trait VerificationServer extends Post { ast_jobs.discardJob(jid) } - /** This method starts a verification process. - * - * As such, it accepts an instance of a VerificationTask, which it will pass to the JobActor. - */ + /** Starts a verification process. */ protected def initializeVerificationProcess(task_maybe_fut: Future[Option[MessageStreamingTask[Unit]]], ast_job_id_maybe: Option[AstJobId]): VerJobId = { if (!isRunning) { @@ -168,10 +144,10 @@ trait VerificationServer extends Post { } } - /** Build the combined Envelope source for a verification job (optionally - * prepending the AST job's messages). Callers attach a sink to consume. + /** Combined envelope iterator for a verification job, optionally prepending + * the AST job's messages. Caller iterates synchronously to drain. */ - protected def messageEnvelopeSource(jid: VerJobId, include_ast: Boolean): Option[Future[(VerHandle, Source[Envelope, NotUsed])]] = { + protected def messageEnvelopes(jid: VerJobId, include_ast: Boolean): Option[Future[(VerHandle, Iterator[Envelope])]] = { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } @@ -180,82 +156,55 @@ trait VerificationServer extends Post { handle_future.flatMap((ver_handle: VerHandle) => { ver_handle.prev_job_id match { case _ if !include_ast => - Future.successful((None, ver_handle)) + Future.successful((None: Option[AstHandle[Option[AST]]], ver_handle)) case None => - Future.successful((None, ver_handle)) + Future.successful((None: Option[AstHandle[Option[AST]]], ver_handle)) case Some(ast_id) => ast_jobs.lookupJob(ast_id) match { case Some(ast_handle_fut) => - ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle)) + ast_handle_fut.map(ast_handle => (Some(ast_handle): Option[AstHandle[Option[AST]]], ver_handle)) case None => - Future.successful((None, ver_handle)) + Future.successful((None: Option[AstHandle[Option[AST]]], ver_handle)) } } }).map { - case (ast_handle_maybe: Option[AstHandle[Option[AST]]], ver_handle: VerHandle) => - val ver_source = ver_handle match { - case VerHandle(null, null, _) => - Source.empty[Envelope] - case _ => - Source.fromIterator(() => ver_handle.stream.iterator) + case (ast_handle_maybe, ver_handle) => + val ver_iter: Iterator[Envelope] = ver_handle match { + case VerHandle(null, null, _) => Iterator.empty + case _ => ver_handle.stream.iterator } - val combined_source = ast_handle_maybe match { - case None => ver_source - case Some(ast_handle) => ver_source.prepend(Source.fromIterator(() => ast_handle.stream.iterator)) + val combined: Iterator[Envelope] = ast_handle_maybe match { + case None => ver_iter + case Some(ast_handle) => ast_handle.stream.iterator ++ ver_iter } - (ver_handle, combined_source) + (ver_handle, combined) }) } - /** Build the Envelope source for an AST job. */ - protected def messageEnvelopeSource(jid: AstJobId): Option[Future[(AstHandle[Option[AST]], Source[Envelope, NotUsed])]] = { + /** Envelope iterator for an AST job. */ + protected def messageEnvelopes(jid: AstJobId): Option[Future[(AstHandle[Option[AST]], Iterator[Envelope])]] = { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } ast_jobs.lookupJob(jid).map(_.map(ast_handle => - (ast_handle, Source.fromIterator(() => ast_handle.stream.iterator)))) + (ast_handle, ast_handle.stream.iterator))) } - /** Stream all messages generated by the Verification backend to some actor. - * If `include_ast` is set, this will also stream the AST messages. - * - * Deletes the JobHandle on completion. - */ - protected def streamMessages(jid: VerJobId, clientActor: ActorRef, include_ast: Boolean): Option[Future[Done]] = { - messageEnvelopeSource(jid, include_ast).map(_.flatMap { case (ver_handle, combined_source) => - val sink = Sink.actorRef(clientActor, Status.Success, Status.Failure) - combined_source.map(e => unpack(e)).runWith(sink) - ver_handle.stream.watchCompletion.map(_ => Done) - }) - } - - /** Collect all messages generated by a verification job (including AST - * messages) into a list. Returns None if the job is unknown. - */ + /** Collect all messages from a verification job (including AST messages) into a list. */ def collectMessages(jid: VerJobId): Option[Future[List[A]]] = { - messageEnvelopeSource(jid, include_ast = true).map(_.flatMap { case (_, combined_source) => - combined_source.map(e => unpack(e)).runFold(List.empty[A])(_ :+ _) - }) - } - - /** Stream all messages generated by the AST backend to some actor. - * - * Deletes the JobHandle on completion. - */ - protected def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = { - messageEnvelopeSource(jid).map(_.flatMap { case (ast_handle, ast_source) => - ast_source.map(e => unpack(e)).runWith(Sink.actorRef(clientActor, Status.Success, Status.Failure)) - ast_handle.stream.watchCompletion.map(_ => Done) + messageEnvelopes(jid, include_ast = true).map(_.flatMap { case (_, iter) => + Future { + iter.map(e => unpack(e)).toList + }(executor) }) } /** Stops an instance of VerificationServer from running. - * The actor system and executor do not get terminated and are the responsibility of the caller * - * As such it should be the last method called. Calling any other function after stop will - * result in an IllegalStateException. - * */ + * Should be the last method called. Calling any other function after `stop` + * will result in an IllegalStateException. + */ def stop(): Future[List[String]] = { if(!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") @@ -271,8 +220,7 @@ trait VerificationServer extends Post { }) } - /** This method interrupts active jobs upon termination of the server. - */ + /** Interrupts all active jobs (used during server shutdown). */ protected def getInterruptFutureList(): Future[List[String]] = { val handles = ver_jobs.jobHandles ++ ast_jobs.jobHandles val interrupt_future_list: List[Future[String]] = handles.map { @@ -289,10 +237,10 @@ trait VerificationServer extends Post { } trait DefaultVerificationServerStart extends VerificationServer { - override def start(active_jobs: Int): Future[Done] = { + override def start(active_jobs: Int): Future[Unit] = { ast_jobs = new JobPool("VSI-AST-pool", active_jobs) ver_jobs = new JobPool("VSI-Verification-pool", active_jobs) isRunning = true - Future.successful(Done) + Future.unit } } diff --git a/src/test/scala/viper/server/core/AstGenerationTests.scala b/src/test/scala/viper/server/core/AstGenerationTests.scala index 16998da5..a5da9368 100644 --- a/src/test/scala/viper/server/core/AstGenerationTests.scala +++ b/src/test/scala/viper/server/core/AstGenerationTests.scala @@ -8,7 +8,6 @@ package viper.server.core import java.nio.file.NoSuchFileException -import akka.http.scaladsl.testkit.ScalatestRouteTest import org.scalatest.matchers.should.Matchers import org.scalatest.wordspec.AnyWordSpec import viper.server.utility.ViperAstGenerator @@ -16,7 +15,7 @@ import viper.silver.ast.Program import viper.silver.logger.ViperStdOutLogger -class AstGenerationTests extends AnyWordSpec with Matchers with ScalatestRouteTest { +class AstGenerationTests extends AnyWordSpec with Matchers { private val verifiableFile = "src/test/resources/viper/let.vpr" private val emptyFile = "src/test/resources/viper/empty.vpr" diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index 5563db4d..bb33f323 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -7,9 +7,6 @@ package viper.server.core import java.nio.file.Paths -import akka.actor.{Actor, Props, Status} -import akka.pattern.ask -import akka.util.Timeout import org.eclipse.lsp4j.{MessageActionItem, MessageParams, Position, PublishDiagnosticsParams, Range, ShowMessageRequestParams} import org.scalatest.exceptions.TestFailedException import org.scalatest.matchers.should.Matchers @@ -520,64 +517,24 @@ class CoreServerSpec extends AnyWordSpec with Matchers { verifyMultipleFiles(core, List(fileBeforeModification, fileAfterReorderingDomainFunctions, fileAfterReorderingDomainAxioms), handleResult)(context) }) - object ClientActor { - case object ReportOutcome - def props(): Props = Props(new ClientActor()) - } - - class ClientActor() extends Actor { - - private var outcome: Option[Boolean] = None - private val outcomePromise: Promise[Boolean] = Promise() - - override def receive: PartialFunction[Any, Unit] = { - case m: Message => - m match { - case _: OverallSuccessMessage => outcome = Some(true) - case _: OverallFailureMessage => outcome = Some(false) - case _ => - } - case ClientActor.ReportOutcome => - sender() ! outcomePromise.future - case Status.Success => - // Success is sent when the stream is completed - if (outcome.isEmpty) { - // we should have received an overall message by now - outcomePromise.failure(new RuntimeException("expected to receive an overall verification message but received none so far")) - } else { - outcomePromise.success(outcome.get) - } - case Status.Failure(f) => outcomePromise.failure(f) - } - } - - s"be able to verify multiple programs with caching disabled and retrieve results via `streamMessages()`" in withServer[ViperCoreServer]({ (core, context) => + s"be able to verify multiple programs with caching disabled and retrieve results via `collectMessages()`" in withServer[ViperCoreServer]({ (core, context) => implicit val ctx: VerificationExecutionContext = context - val test_actors = 0 to 2 map (_ => context.actorSystem.actorOf(ClientActor.props())) val jids = files.map(file => verifySiliconWithoutCaching(core, file)) - // stream messages to actors - val jidsWithActors = jids zip test_actors - val streamOptionsWithActors = jidsWithActors map { case (jid, actor) => (core.streamMessages(jid, actor, include_ast = true), actor) } - // stream options should be defined - val streamDones = streamOptionsWithActors map { case (streamOption, actor) => - assert(streamOption.isDefined) - val streamDoneFuture = streamOption.get - // as soon as stream completes, complete it with the actor - streamDoneFuture.map(_ => actor) + val outcomeFutures: Seq[Future[Boolean]] = jids.map { jid => + core.collectMessages(jid).getOrElse(Future.failed(JobNotFoundException)).map { msgs => + val outcomes = msgs.collect { + case _: OverallSuccessMessage => true + case _: OverallFailureMessage => false + } + if (outcomes.isEmpty) { + throw new RuntimeException("expected to receive an overall verification message but received none") + } + outcomes.head + } } - // streamDones futures should eventually be resolved - val allVerificationsFuture = Future.sequence(streamDones) - val outcomesFuture = allVerificationsFuture.flatMap(actors => { - val outcomeFutures = actors.map(actor => { - implicit val askTimeout: Timeout = Timeout(5000 milliseconds) - (actor ? ClientActor.ReportOutcome).mapTo[Future[Boolean]].flatten - }) - Future.sequence(outcomeFutures) - }) - val assertionsFuture = outcomesFuture.map(_.zip(files) map { case (outcome, file) => + val assertionsFuture = Future.sequence(outcomeFutures).map(_.zip(files) map { case (outcome, file) => assert(outcome == (file != ver_error_file)) }) - // map assertionsFuture to a single assertion: assertionsFuture.map(_ => Succeeded) }) diff --git a/src/test/scala/viper/server/core/ReformatterTest.scala b/src/test/scala/viper/server/core/ReformatterTest.scala index c41eefff..5d667694 100644 --- a/src/test/scala/viper/server/core/ReformatterTest.scala +++ b/src/test/scala/viper/server/core/ReformatterTest.scala @@ -6,7 +6,6 @@ package viper.server.core -import akka.http.scaladsl.testkit.ScalatestRouteTest import org.scalatest.Assertion import org.scalatest.matchers.should.Matchers import org.scalatest.wordspec.AnyWordSpec @@ -18,7 +17,7 @@ import viper.silver.parser.ReformatPrettyPrinter import java.nio.file.Path -class ReformatterTest extends AnyWordSpec with Matchers with ScalatestRouteTest { +class ReformatterTest extends AnyWordSpec with Matchers { private val console_logger = ViperStdOutLogger("parsingTest logger", "ALL") "ReformatterAstGenerator" should { From 717458c4a1bac3dbb2428c86a520d5092db83ca4 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 11:53:40 +0200 Subject: [PATCH 09/22] S4: VerificationServer constructor lifecycle --- .../viper/server/core/ViperCoreServer.scala | 25 ++++++------ .../frontends/http/ViperHttpServer.scala | 21 ++++------ .../frontends/lsp/ViperServerService.scala | 9 ++--- .../viper/server/vsi/VerificationServer.scala | 39 ++++++++----------- .../viper/server/core/CoreServerSpec.scala | 4 +- 5 files changed, 42 insertions(+), 56 deletions(-) diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala index dba4cb31..5010e991 100644 --- a/src/main/scala/viper/server/core/ViperCoreServer.scala +++ b/src/main/scala/viper/server/core/ViperCoreServer.scala @@ -8,7 +8,7 @@ package viper.server.core import ch.qos.logback.classic.Logger import viper.server.ViperConfig -import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer} +import viper.server.vsi.{AstHandle, AstJobId, JobPool, VerHandle, VerJobId, VerificationServer} import viper.silver.ast.Program import viper.silver.ast.utility.FileLoader import viper.silver.logger.ViperLogger @@ -39,18 +39,17 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V } } - /** Configures an instance of ViperCoreServer. - * - * This function must be called before any other. Calling any other function before this one - * will result in an IllegalStateException. - */ - def start(): Future[Unit] = { - ViperCache.initialize(globalLogger, config.backendSpecificCache(), config.cacheFile.toOption) - start(config.maximumActiveJobs()) map { _ => - globalLogger.info(s"ViperCoreServer has started.") - () - } - } + override protected val ast_jobs: JobPool[AstJobId, AstHandle[Option[Program]]] = + new JobPool("AST-pool", config.maximumActiveJobs()) + override protected val ver_jobs: JobPool[VerJobId, VerHandle] = + new JobPool("Verification-pool", config.maximumActiveJobs()) + + ViperCache.initialize(globalLogger, config.backendSpecificCache(), config.cacheFile.toOption) + + override def start(): Future[Unit] = super.start().map { _ => + globalLogger.info(s"ViperCoreServer has started.") + () + }(executor) def requestAst(file: String, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, loader: Option[FileLoader] = None): AstJobId = { require(config != null) diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala index db64ab02..1cb53194 100644 --- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala +++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala @@ -33,25 +33,18 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex override def start(): Future[Unit] = { port = config.port.toOption.getOrElse(0) super.start().map { _ => + undertow = Undertow.builder() + .addHttpListener(port, "localhost") + .setHandler(routes.defaultHandler) + .build() + undertow.start() + val boundAddr = undertow.getListenerInfo.get(0).getAddress.asInstanceOf[InetSocketAddress] + port = boundAddr.getPort println(s"ViperServer online at http://localhost:$port") () }(executor) } - override def start(active_jobs: Int): Future[Unit] = { - ast_jobs = new JobPool("AST-pool", active_jobs) - ver_jobs = new JobPool("Verification-pool", active_jobs) - undertow = Undertow.builder() - .addHttpListener(port, "localhost") - .setHandler(routes.defaultHandler) - .build() - undertow.start() - val boundAddr = undertow.getListenerInfo.get(0).getAddress.asInstanceOf[InetSocketAddress] - port = boundAddr.getPort - isRunning = true - Future.unit - } - override protected def onExit(): Future[Unit] = { if (undertow != null) { val u = undertow diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 7c2e3fea..d9b749d5 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -10,17 +10,16 @@ import ch.qos.logback.classic.Logger import viper.server.ViperConfig import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, ViperCoreServer} import viper.server.frontends.lsp.file.RelayHandler -import viper.server.utility.ReformatterAstGenerator -import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile} import viper.server.utility.Helpers.validateViperFile -import viper.server.vsi.{AstJobId, DefaultVerificationServerStart, VerHandle, VerJobId} -import viper.silver.parser.ReformatPrettyPrinter +import viper.server.utility.ReformatterAstGenerator +import viper.server.vsi.{AstJobId, VerHandle, VerJobId} import viper.silver.ast.utility.FileLoader +import viper.silver.parser.ReformatPrettyPrinter import scala.concurrent.Future class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext) - extends ViperCoreServer(config)(executor) with DefaultVerificationServerStart { + extends ViperCoreServer(config)(executor) { def constructAst(file: String, backend: ViperBackendConfig, localLogger: Option[Logger] = None, loader: Option[FileLoader]): AstJobId = { val logger = combineLoggers(localLogger) diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index 2ccb4630..f1903dad 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -6,6 +6,8 @@ package viper.server.vsi +import java.util.concurrent.atomic.AtomicBoolean + import viper.server.core.VerificationExecutionContext import scala.concurrent.Future @@ -22,6 +24,11 @@ abstract class AstConstructionException extends VerificationServerException * Each booked job owns a `JobExecution` (cancellable Future-task wrapper) and an * `EnvelopeStream` over which the backend streams messages back to consumers. * Two pools (AST construction, verification) are managed in parallel. + * + * Pools are constructor-initialised by the implementing class, so an instance + * is ready as soon as it is constructed. `start()` is a hook for subclass + * startup work (e.g. binding an HTTP listener); `stop()` flips the running + * flag idempotently. */ trait VerificationServer extends Post { @@ -37,19 +44,17 @@ trait VerificationServer extends Post { implicit val ast_id_fact: Int => AstJobId = AstJobId.apply implicit val ver_id_fact: Int => VerJobId = VerJobId.apply - protected var ast_jobs: JobPool[AstJobId, AstHandle[Option[AST]]] = _ - protected var ver_jobs: JobPool[VerJobId, VerHandle] = _ + protected val ast_jobs: JobPool[AstJobId, AstHandle[Option[AST]]] + protected val ver_jobs: JobPool[VerJobId, VerHandle] - var isRunning: Boolean = false + private val _running: AtomicBoolean = new AtomicBoolean(true) + def isRunning: Boolean = _running.get() - /** Configures an instance of VerificationServer. - * - * Calling any other function before this one will result in an - * IllegalStateException. The returned future resolves when the server has - * been started. A default implementation is provided in - * `DefaultVerificationServerStart`. + /** Hook for subclasses to perform startup work after construction (e.g. bind + * an HTTP listener). Default is a no-op. Pools and running state are + * already established by the constructor. */ - def start(active_jobs: Int): Future[Unit] + def start(): Future[Unit] = Future.unit protected def initializeProcess[S <: JobId, T <: JobHandle : ClassTag] (pool: JobPool[S, T], @@ -203,13 +208,12 @@ trait VerificationServer extends Post { /** Stops an instance of VerificationServer from running. * * Should be the last method called. Calling any other function after `stop` - * will result in an IllegalStateException. + * will result in an IllegalStateException. Idempotent: a second call throws. */ def stop(): Future[List[String]] = { - if(!isRunning) { + if (!_running.compareAndSet(true, false)) { throw new IllegalStateException("Instance of VerificationServer already stopped") } - isRunning = false getInterruptFutureList().transform(r => { onExit() r match { @@ -235,12 +239,3 @@ trait VerificationServer extends Post { else s"$jid has already been finalized." } } - -trait DefaultVerificationServerStart extends VerificationServer { - override def start(active_jobs: Int): Future[Unit] = { - ast_jobs = new JobPool("VSI-AST-pool", active_jobs) - ver_jobs = new JobPool("VSI-Verification-pool", active_jobs) - isRunning = true - Future.unit - } -} diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index bb33f323..ac3bb2cc 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -16,7 +16,7 @@ import viper.server.ViperConfig import viper.server.frontends.lsp.{ClientCoordinator, GetIdentifierResponse, GetRangeResponse, GetViperFileEndingsResponse, HintMessage, IdeLanguageClient, LogParams, SetupProjectParams, StateChangeParams, UnhandledViperServerMessageTypeParams, VerificationNotStartedParams, ViperServerService} import viper.server.frontends.lsp.file.FileManager import viper.server.utility.ViperAstGenerator -import viper.server.vsi.{DefaultVerificationServerStart, JobNotFoundException, VerJobId} +import viper.server.vsi.{JobNotFoundException, VerJobId} import viper.silver.ast import viper.silver.ast.{AbstractSourcePosition, HasLineColumn, Program} import viper.silver.logger.SilentLogger @@ -96,7 +96,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { } implicit val viperCoreServerFactory: (ViperConfig, VerificationExecutionContext) => ViperCoreServer = - (config, context) => new ViperCoreServer(config)(context) with DefaultVerificationServerStart + (config, context) => new ViperCoreServer(config)(context) {} val viperServerServiceFactory: (ViperConfig, VerificationExecutionContext) => ViperServerService = (config, context) => new ViperServerService(config)(context) From 79be4935606ce0841d46adf11bb125e963387ed8 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 12:06:07 +0200 Subject: [PATCH 10/22] S1: Simplify JobPool to a single map with atomic tryBook --- src/main/scala/viper/server/vsi/JobPool.scala | 66 ++++++++----------- .../viper/server/vsi/VerificationServer.scala | 20 ++---- 2 files changed, 33 insertions(+), 53 deletions(-) diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index 2aa85cc3..279c8998 100644 --- a/src/main/scala/viper/server/vsi/JobPool.scala +++ b/src/main/scala/viper/server/vsi/JobPool.scala @@ -42,52 +42,44 @@ case class VerHandle(execution: JobExecution[_], def tag = "VER" } +/** Bounded registry of active jobs. Single mutex guards all access; the API is + * compound-action-safe (capacity check + insert is one atomic step). + * + * `tryBook` registers the entry *before* invoking the start callback so that + * synchronous `discardJob` calls inside the callback (used to free the slot + * for placeholder/no-op jobs) find a live entry to remove. + */ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS: Int = 3) (implicit val jid_fact: Int => S) { - private val _jobHandles: mutable.Map[S, Promise[T]] = mutable.Map() - private val _jobExecutors: mutable.Map[S, () => Future[T]] = mutable.Map() - private val _jobCache: mutable.Map[S, Future[T]] = mutable.Map() - def jobHandles: Map[S, Future[T]] = _jobHandles.map{ case (id, hand) => (id, hand.future) }.toMap - + private val jobs: mutable.Map[S, Future[T]] = mutable.Map() private val _nextJobId: AtomicInteger = new AtomicInteger(0) - def newJobsAllowed: Boolean = jobHandles.size < MAX_ACTIVE_JOBS - - def bookNewJob(job_executor: S => Future[T]): S = { - require(newJobsAllowed) - - val new_jid: S = jid_fact(_nextJobId.getAndIncrement()) - - _jobHandles(new_jid) = Promise() - _jobExecutors(new_jid) = () => { - if (_jobCache.contains(new_jid)) { - /** This prevents recomputing the same future multiple times. */ - _jobCache(new_jid) - } else { - /** Create Future[JobHandle]. */ - val t_fut = job_executor(new_jid) - - /** Cache the newly created Future[JobHandle] for later reference. */ - _jobCache(new_jid) = t_fut - t_fut - } + def jobHandles: Map[S, Future[T]] = synchronized { jobs.toMap } + + /** Atomically: check capacity, allocate a fresh id, register a placeholder + * Future, then invoke `buildStart` to obtain the real Future and wire it + * into the placeholder. Returns `None` if at capacity. + * + * `synchronized` is reentrant, so `buildStart` may call `discardJob` on + * this pool synchronously without deadlock. + */ + def tryBook(buildStart: S => Future[T]): Option[S] = synchronized { + if (jobs.size >= MAX_ACTIVE_JOBS) None + else { + val jid: S = jid_fact(_nextJobId.getAndIncrement()) + val promise = Promise[T]() + jobs(jid) = promise.future + promise.completeWith(buildStart(jid)) + Some(jid) } - new_jid } - def discardJob(jid: S): Unit = { - _jobHandles -= jid - _jobExecutors -= jid - _jobCache -= jid + def discardJob(jid: S): Unit = synchronized { + jobs -= jid } - def lookupJob(jid: S): Option[Future[T]] = { - _jobHandles.get(jid).map((promise: Promise[T]) => { - /** 1. Execute the job and get the result's future OR get the priorly cached result's future. - * 2. Complete the promise with this future. */ - promise.completeWith(_jobExecutors(jid)()) - promise.future - }) + def lookupJob(jid: S): Option[Future[T]] = synchronized { + jobs.get(jid) } } diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index f1903dad..fbabac60 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -60,15 +60,13 @@ trait VerificationServer extends Post { (pool: JobPool[S, T], task_maybe_fut: Future[Option[MessageStreamingTask[_]]], discardOnCompletion: Boolean, - prev_job_id_maybe: Option[AstJobId] = None): S = { + prev_job_id_maybe: Option[AstJobId] = None): Option[S] = { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } - require(pool.newJobsAllowed) - - pool.bookNewJob((new_jid: S) => task_maybe_fut.flatMap((task_maybe: Option[MessageStreamingTask[_]]) => { + pool.tryBook((new_jid: S) => task_maybe_fut.flatMap((task_maybe: Option[MessageStreamingTask[_]]) => { task_maybe match { case None => /** No task means a prerequisite produced no usable artifact; the placeholder @@ -123,12 +121,7 @@ trait VerificationServer extends Post { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } - - if (ast_jobs.newJobsAllowed) { - initializeProcess(ast_jobs, Future.successful(Some(task)), false) - } else { - AstJobId(-1) // Process Management running at max capacity. - } + initializeProcess(ast_jobs, Future.successful(Some(task)), false).getOrElse(AstJobId(-1)) } protected def discardAstJob(jid: AstJobId): Unit = { @@ -141,12 +134,7 @@ trait VerificationServer extends Post { if (!isRunning) { throw new IllegalStateException("Instance of VerificationServer already stopped") } - - if (ver_jobs.newJobsAllowed) { - initializeProcess(ver_jobs, task_maybe_fut, true, ast_job_id_maybe) - } else { - VerJobId(-1) // Process Management running at max capacity. - } + initializeProcess(ver_jobs, task_maybe_fut, true, ast_job_id_maybe).getOrElse(VerJobId(-1)) } /** Combined envelope iterator for a verification job, optionally prepending From 74f598aff128426bb1ca411c4c9512e36616cd16 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 12:13:44 +0200 Subject: [PATCH 11/22] S2: Make EnvelopeStream offer/complete mutex-safe; task owns its stream --- .../server/core/MessageReportingTask.scala | 3 +- .../viper/server/vsi/EnvelopeStream.scala | 12 +++++-- .../server/vsi/MessageStreamingTask.scala | 31 ++++++------------- .../viper/server/vsi/VerificationServer.scala | 9 ++---- 4 files changed, 24 insertions(+), 31 deletions(-) diff --git a/src/main/scala/viper/server/core/MessageReportingTask.scala b/src/main/scala/viper/server/core/MessageReportingTask.scala index b885160c..e7b35b0e 100644 --- a/src/main/scala/viper/server/core/MessageReportingTask.scala +++ b/src/main/scala/viper/server/core/MessageReportingTask.scala @@ -8,8 +8,7 @@ package viper.server.core import ch.qos.logback.classic.Logger import viper.server.vsi.MessageStreamingTask -import viper.silver.reporter.{Entity, EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter, Time, VerificationResultMessage} -import viper.silver.verifier.{Success, VerificationResult} +import viper.silver.reporter.{EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter} trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost { diff --git a/src/main/scala/viper/server/vsi/EnvelopeStream.scala b/src/main/scala/viper/server/vsi/EnvelopeStream.scala index ddcb4162..4945aa06 100644 --- a/src/main/scala/viper/server/vsi/EnvelopeStream.scala +++ b/src/main/scala/viper/server/vsi/EnvelopeStream.scala @@ -24,8 +24,14 @@ final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { private val completionPromise: Promise[Unit] = Promise() @volatile private var completed: Boolean = false - /** Block until `e` can be enqueued. Throws if the stream is already complete. */ - def offer(e: Envelope): Unit = { + /** Block until `e` can be enqueued. Throws if the stream is already complete. + * + * `synchronized` makes the read of `completed` and the put of `Msg(e)` + * atomic with respect to `complete()`, so a concurrent completion cannot + * insert the `Done` sentinel between this check and put — which would + * strand `e` after end-of-stream. + */ + def offer(e: Envelope): Unit = this.synchronized { if (completed) { throw new IllegalStateException("EnvelopeStream is already complete") } @@ -44,6 +50,8 @@ final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { /** Future that resolves when `complete` is called. */ def watchCompletion: Future[Unit] = completionPromise.future + def isCompleted: Boolean = completed + /** Single-shot iterator over the stream. Blocks on `hasNext`/`next` until * envelopes are available. Returns false from `hasNext` once the * completion sentinel is observed. diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala index 02c09956..0bd0dfa1 100644 --- a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala +++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala @@ -17,8 +17,13 @@ import scala.util.Try /** Generic wrapper for any task a VerificationServer might work on. * * Implements Callable and provides an artifact future that completes when the - * task terminates. Holds a reference to an `EnvelopeStream` used to push - * backend messages to downstream consumers. + * task terminates. Owns the `EnvelopeStream` it pushes backend messages to — + * created at construction so it's a `final val`, removing the prior + * post-construction `setStream` indirection and its visibility concerns. + * + * `enqueueMessage` and `registerTaskEnd` are both expected to be invoked from + * the same producer (the worker thread). The stream's own synchronization + * keeps things safe even if that contract is violated. * */ abstract class MessageStreamingTask[T] extends Callable[T] with Post { @@ -28,24 +33,12 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { override def done(): Unit = artifactPromise.complete(Try(get())) } - private var stream: EnvelopeStream = _ - private var hasEnded: Boolean = false - - final def setStream(s: EnvelopeStream): Unit = { - if (stream != null) { - throw new IllegalStateException("cannot set stream - a stream has already been set") - } - stream = s - } + val stream: EnvelopeStream = new EnvelopeStream() /** Offers `msg` to the downstream stream, blocking until queue space is available * (natural backpressure when consumers are slow). */ protected def enqueueMessage(msg: Envelope, logger: Logger): Unit = { - if (hasEnded) { - throw new IllegalStateException("cannot enqueue message - message streaming task's end has already been registered") - } - logger.trace(s"enqueueMessage: $msg") try { stream.offer(msg) @@ -59,14 +52,10 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { /** Closes the downstream stream, signalling the end of the message stream. * * @param success retained for API compatibility; stream completion is the same - * regardless of success/failure outcome. + * regardless of success/failure outcome. Idempotent (a second + * call is a no-op). */ protected def registerTaskEnd(success: Boolean, logger: Logger): Unit = { - if (hasEnded) { - throw new IllegalStateException("cannot register task end - message streaming task's end has already been registered") - } - - hasEnded = true logger.trace(s"registerTaskEnd: $success") stream.complete() } diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index fbabac60..c272afaf 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -78,12 +78,9 @@ trait VerificationServer extends Post { Future.successful(VerHandle(null, null, prev_job_id_maybe)) } case Some(task) => - val stream = new EnvelopeStream() - task.setStream(stream) - val execution = new JobExecution(task.futureTask) - stream.watchCompletion.onComplete(_ => { + task.stream.watchCompletion.onComplete(_ => { if (discardOnCompletion) { pool.discardJob(new_jid) } @@ -93,9 +90,9 @@ trait VerificationServer extends Post { val handle: JobHandle = new_jid match { case _: AstJobId => - AstHandle(execution, stream, task.artifact) + AstHandle(execution, task.stream, task.artifact) case _: VerJobId => - VerHandle(execution, stream, + VerHandle(execution, task.stream, prev_job_id_maybe match { case Some(prev_job_id: AstJobId) => Some(prev_job_id) From ca821e2d51a904869c9f8ba54122b41dab3add38 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 12:29:17 +0200 Subject: [PATCH 12/22] S3: Per-FileManager monitor serializes RelayHandler + verification mutators --- .../frontends/lsp/file/FileManager.scala | 10 +++++++- .../frontends/lsp/file/RelayActor.scala | 18 ++++++++++--- .../frontends/lsp/file/Verification.scala | 25 +++++++++++-------- 3 files changed, 37 insertions(+), 16 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala index 2b6d7b18..e0687188 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala @@ -44,11 +44,19 @@ trait ManagesLeaf { def getInFuture[T](f: => T): Future[T] } +/** Per-file state, serialized via the instance's intrinsic monitor. + * + * The FileManager's `synchronized` is the per-file mutex. RelayHandler + * methods, lifecycle methods (`close`), and verification mutators + * (`startVerification`, `stop`, …) all acquire it. Reads of multi-field + * snapshot state should also synchronize. The lock is reentrant, so + * methods that call into each other don't deadlock. + */ case class FileManager(root: LeafManager)(implicit executor: VerificationExecutionContext) extends MessageHandler { override val ec: VerificationExecutionContext = executor var isOpen: Boolean = true - def close(): Unit = { + def close(): Unit = synchronized { teardownProject() stopRunningVerification() } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index daa7eda7..b65b7d19 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -83,6 +83,13 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti } } +/** Drains backend messages into the owning `MessageHandler` (FileManager). + * + * All public methods acquire the FileManager's intrinsic monitor (`task`) so + * message handling is serialized with respect to LSP request handlers and the + * other relay (AST vs. verification streams that share the same FileManager). + * This restores the per-file serialization the previous Akka actor provided. + */ class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { val coordinator = task.coordinator @@ -90,6 +97,9 @@ class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { * errors together with the offending node's position (only for errors that have an offending node (i.e. implement * `ErrorMessage`). Storing the position along with the error fixes the issue that two errors with offending nodes * at different position just get dropped. + * + * Accessed only under `task.synchronized` (entered by `handleMessage` / + * `getReportedErrors`). */ private var reportedErrors: Set[(AbstractError, Option[ast.Position])] = Set.empty /** helper function to add an error to `reportedErrors` */ @@ -105,9 +115,9 @@ class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { case _ => reportedErrors.contains((err, None)) } - def getReportedErrors: Seq[AbstractError] = reportedErrors.toSeq.map(_._1) + def getReportedErrors: Seq[AbstractError] = task.synchronized { reportedErrors.toSeq.map(_._1) } - def handleMessage(m: Message): Unit = { + def handleMessage(m: Message): Unit = task.synchronized { if (task.is_aborting) { coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ignoring message because we are aborting: $m") return @@ -206,12 +216,12 @@ class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { } } - def onStreamSuccess(): Unit = { + def onStreamSuccess(): Unit = task.synchronized { coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] stream success") if (backendClassName.isDefined) task.completionHandler(0) } - def onStreamFailure(cause: Throwable): Unit = { + def onStreamFailure(cause: Throwable): Unit = task.synchronized { coordinator.logger.info(s"[receive@${task.filename}/${backendClassName.isDefined}] stream failed: $cause") if (backendClassName.isDefined) task.completionHandler(-1) } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index ba5badcc..f99db7aa 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -79,9 +79,9 @@ object VerificationPhase { } trait VerificationManager extends ManagesLeaf { - def stopRunningVerification(): Future[Boolean] = { + def stopRunningVerification(): Future[Boolean] = synchronized { stop() - .map(_ => { + .map(_ => synchronized { coordinator.logger.trace(s"stopVerification has completed for ${file_uri}") val params = lsp.StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = file_uri) coordinator.sendStateChangeNotification(params, Some(this)) @@ -146,7 +146,7 @@ trait VerificationManager extends ManagesLeaf { var lastCustomArgs: Option[String] = None var lastBackendClassName: Option[String] = None - def prepareVerification(mt: Boolean): Unit = { + def prepareVerification(mt: Boolean): Unit = synchronized { manuallyTriggered = mt is_verifying = true @@ -159,7 +159,7 @@ trait VerificationManager extends ManagesLeaf { internalErrorMessage = "" } - def stop(): Future[Unit] = { + def stop(): Future[Unit] = synchronized { coordinator.logger.trace(s"stop verification of $file_uri") handler.verHandle match { case None => { @@ -170,7 +170,7 @@ trait VerificationManager extends ManagesLeaf { coordinator.logger.info("Aborting running verification.") is_aborting = true val stop = coordinator.server.stopVerification(verJob, Some(coordinator.localLogger)).transform( - _ => { + _ => synchronized { is_verifying = false lastSuccess = Aborted }, @@ -187,7 +187,7 @@ trait VerificationManager extends ManagesLeaf { } /** Run parsing and typechecking but no verification */ - def runParseTypecheck(loader: FileContent): Boolean = { + def runParseTypecheck(loader: FileContent): Boolean = synchronized { coordinator.logger.info(s"construct AST for $filename") if (anyFutureRunning) { coordinator.logger.debug(s"Already running parse/typecheck or verification") @@ -210,13 +210,16 @@ trait VerificationManager extends ManagesLeaf { /** Do full parsing, type checking and verification */ def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = { - lastBackendClassName = Some(backendClassName) - lastCustomArgs = Some(customArgs) + val pendingCancel = synchronized { + lastBackendClassName = Some(backendClassName) + lastCustomArgs = Some(customArgs) + coordinator.logger.info(s"verify $filename ($backendClassName $customArgs)") + if (handler.isVerifying) stop() + futureCancel.getOrElse(Future.unit) + } val backend = ViperBackendConfig(backendClassName, customArgs) - coordinator.logger.info(s"verify $filename ($backendClassName $customArgs)") - if (handler.isVerifying) stop() - futureCancel.getOrElse(Future.unit).map(_ => { + pendingCancel.map(_ => synchronized { lastPhase = None From 808959900600680293a9f50b298b53bcd9c2d007 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 12:54:55 +0200 Subject: [PATCH 13/22] H1+H2: Drop duplicate apache Socket and unused findFreePort --- .../viper/server/utility/apache/LICENSE.txt | 202 ------------------ .../viper/server/utility/apache/NOTICE.txt | 11 - .../viper/server/utility/apache/Socket.scala | 72 ------- .../viper/server/utility/ibm/Socket.scala | 42 ---- 4 files changed, 327 deletions(-) delete mode 100644 src/main/scala/viper/server/utility/apache/LICENSE.txt delete mode 100644 src/main/scala/viper/server/utility/apache/NOTICE.txt delete mode 100644 src/main/scala/viper/server/utility/apache/Socket.scala diff --git a/src/main/scala/viper/server/utility/apache/LICENSE.txt b/src/main/scala/viper/server/utility/apache/LICENSE.txt deleted file mode 100644 index 7a4a3ea2..00000000 --- a/src/main/scala/viper/server/utility/apache/LICENSE.txt +++ /dev/null @@ -1,202 +0,0 @@ - - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. - - END OF TERMS AND CONDITIONS - - APPENDIX: How to apply the Apache License to your work. - - To apply the Apache License to your work, attach the following - boilerplate notice, with the fields enclosed by brackets "[]" - replaced with your own identifying information. (Don't include - the brackets!) The text should be enclosed in the appropriate - comment syntax for the file format. We also recommend that a - file or class name and description of purpose be included on the - same "printed page" as the copyright notice for easier - identification within third-party archives. - - Copyright [yyyy] [name of copyright owner] - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. \ No newline at end of file diff --git a/src/main/scala/viper/server/utility/apache/NOTICE.txt b/src/main/scala/viper/server/utility/apache/NOTICE.txt deleted file mode 100644 index f4f12814..00000000 --- a/src/main/scala/viper/server/utility/apache/NOTICE.txt +++ /dev/null @@ -1,11 +0,0 @@ - ========================================================================= - == NOTICE file corresponding to the section 4 d of == - == the Apache License, Version 2.0, == - == in this case for the Apache Camel distribution. == - ========================================================================= - - This product includes software developed by - The Apache Software Foundation (http://www.apache.org/). - - Please read the different LICENSE files present in the licenses directory of - this distribution. \ No newline at end of file diff --git a/src/main/scala/viper/server/utility/apache/Socket.scala b/src/main/scala/viper/server/utility/apache/Socket.scala deleted file mode 100644 index b3812e69..00000000 --- a/src/main/scala/viper/server/utility/apache/Socket.scala +++ /dev/null @@ -1,72 +0,0 @@ -/** - * Licensed to the Apache Software Foundation (ASF) under one or more - * contributor license agreements. See the NOTICE file distributed with - * this work for additional information regarding copyright ownership. - * The ASF licenses this file to You under the Apache License, Version 2.0 - * (the "License"); you may not use this file except in compliance with - * the License. You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package viper.server.utility.apache - -import java.io.IOException -import java.net.{DatagramSocket, ServerSocket} - -object Socket { - - /** - * The minimum server currentMinPort number. Set at 1100 to avoid returning privileged - * currentMinPort numbers. - * - * Source: http://svn.apache.org/viewvc/camel/trunk/components/camel-test/src/main/java/org/apache/camel/test/AvailablePortFinder.java?view=markup#l39 - */ - val MIN_PORT_NUMBER = 1100 - - /** - * The maximum server currentMinPort number. - */ - val MAX_PORT_NUMBER = 65535 - - /** - * Checks to see if a specific port is available. - * - * Source: http://svn.apache.org/viewvc/camel/trunk/components/camel-test/src/main/java/org/apache/camel/test/AvailablePortFinder.java - * Source: https://stackoverflow.com/questions/434718/sockets-discover-port-availability-using-java - * - * @param port the port to check for availability - */ - def available(port: Int): Boolean = { - if (port < MIN_PORT_NUMBER || port > MAX_PORT_NUMBER) - throw new IllegalArgumentException("Invalid start port: " + port) - var ss: ServerSocket = null - var ds: DatagramSocket = null - try { - ss = new ServerSocket(port) - ss.setReuseAddress(true) - ds = new DatagramSocket(port) - ds.setReuseAddress(true) - return true - } catch { - case _: IOException => - - } finally { - if (ds != null) ds.close() - if (ss != null) try - ss.close() - catch { - case _: IOException => - - /* should not be thrown */ - } - } - false - } -} \ No newline at end of file diff --git a/src/main/scala/viper/server/utility/ibm/Socket.scala b/src/main/scala/viper/server/utility/ibm/Socket.scala index 7ababa13..59d43f5d 100644 --- a/src/main/scala/viper/server/utility/ibm/Socket.scala +++ b/src/main/scala/viper/server/utility/ibm/Socket.scala @@ -32,48 +32,6 @@ object Socket { */ val MAX_PORT_NUMBER = 65535 - /** - * Returns a free port number on localhost. - * - * Heavily inspired from org.eclipse.jdt.launching.SocketUtil (to avoid a dependency to JDT just because of this). - * Slightly improved with close() missing in JDT. And throws exception instead of returning -1. - * - * Source: https://gist.github.com/vorburger/3429822 - * TODO: check license - * - * @return a free port number on localhost - * @throws IllegalStateException if unable to find a free port - */ - def findFreePort: Int = { - var socket: ServerSocket = null - try { - socket = new ServerSocket (0) - socket.setReuseAddress (true) - val port: Int = socket.getLocalPort - try { - socket.close () - } catch { - case _: IOException => - - // Ignore IOException on close() - } - return port - } catch { - case _: IOException => - - } finally { - if (socket != null) { - try { - socket.close () - } catch { - case _: IOException => - - } - } - } - throw new IllegalStateException ("Could not find a free TCP/IP port to start ViperServer on") - } - /** * Checks to see if a specific port is available. * From 5e08befd00d9ff16f057dc777f2d26969ebdc433 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 17:55:36 +0200 Subject: [PATCH 14/22] Add task.settled to sequence cleanup before stream wake-ups --- .../viper/server/vsi/EnvelopeStream.scala | 18 ++++- src/main/scala/viper/server/vsi/JobPool.scala | 46 +++++++++---- .../server/vsi/MessageStreamingTask.scala | 68 ++++++++++++++++++- .../viper/server/vsi/VerificationServer.scala | 14 ++-- 4 files changed, 123 insertions(+), 23 deletions(-) diff --git a/src/main/scala/viper/server/vsi/EnvelopeStream.scala b/src/main/scala/viper/server/vsi/EnvelopeStream.scala index 4945aa06..85a2139c 100644 --- a/src/main/scala/viper/server/vsi/EnvelopeStream.scala +++ b/src/main/scala/viper/server/vsi/EnvelopeStream.scala @@ -16,6 +16,13 @@ import scala.concurrent.{Future, Promise} * * `complete` enqueues a sentinel so the iterator terminates cleanly even if * the consumer is currently waiting on `take`. + * + * Note: cleanup that must be observable to consumers before they wake up + * from the iterator should be registered on the owning task via + * `MessageStreamingTask.onSettled`, not here. The task's finalize + * sequence runs hooks BEFORE calling `complete()`, which gives a single + * canonical "fully settled" signal (`task.settled`) without coupling + * cleanup to the stream itself. */ final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { import EnvelopeStream._ @@ -38,7 +45,10 @@ final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { queue.put(Msg(e)) } - /** Mark the stream complete. Idempotent. */ + /** Mark the stream complete. Idempotent. Wakes any iterator waiting on + * `take` (via the `Done` sentinel) and any subscriber to + * `watchCompletion`. + */ def complete(): Unit = this.synchronized { if (!completed) { completed = true @@ -47,7 +57,11 @@ final class EnvelopeStream(capacity: Int = EnvelopeStream.DefaultCapacity) { } } - /** Future that resolves when `complete` is called. */ + /** Future that resolves when `complete` is called. Note: this resolves as + * soon as the stream itself is closed and may fire concurrently with + * other producer-side cleanup. For "everything is finalized" semantics, + * await `MessageStreamingTask.settled` instead. + */ def watchCompletion: Future[Unit] = completionPromise.future def isCompleted: Boolean = completed diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index 279c8998..b2edc6c7 100644 --- a/src/main/scala/viper/server/vsi/JobPool.scala +++ b/src/main/scala/viper/server/vsi/JobPool.scala @@ -43,43 +43,61 @@ case class VerHandle(execution: JobExecution[_], } /** Bounded registry of active jobs. Single mutex guards all access; the API is - * compound-action-safe (capacity check + insert is one atomic step). + * compound-action-safe. * - * `tryBook` registers the entry *before* invoking the start callback so that - * synchronous `discardJob` calls inside the callback (used to free the slot - * for placeholder/no-op jobs) find a live entry to remove. + * Two maps separate **slot accounting** from **entry visibility**: + * - `active` counts toward `MAX_ACTIVE_JOBS`. Booked jobs land here. + * - `completed` does not. `markCompleted` moves an entry from `active` to + * `completed` so the slot is freed but `lookupJob` still finds it. + * + * `markCompleted` is invoked synchronously from `EnvelopeStream.complete`'s + * sync-hook list, so a consumer awaiting the stream's iterator-drain Future + * is guaranteed to see `active.size` decremented before its continuation + * runs. Without this, the iterator's `take()` could unblock before the + * (async) discard fired, and the next `tryBook` would race-fail. */ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS: Int = 3) (implicit val jid_fact: Int => S) { - private val jobs: mutable.Map[S, Future[T]] = mutable.Map() + private val active: mutable.Map[S, Future[T]] = mutable.Map() + private val completed: mutable.Map[S, Future[T]] = mutable.Map() private val _nextJobId: AtomicInteger = new AtomicInteger(0) - def jobHandles: Map[S, Future[T]] = synchronized { jobs.toMap } + /** Active job handles (used at shutdown to interrupt running work). */ + def jobHandles: Map[S, Future[T]] = synchronized { active.toMap } - /** Atomically: check capacity, allocate a fresh id, register a placeholder - * Future, then invoke `buildStart` to obtain the real Future and wire it - * into the placeholder. Returns `None` if at capacity. + /** Atomically check capacity, allocate a fresh id, register a placeholder + * Future, and start work eagerly via `buildStart`. Returns `None` if at + * capacity. * * `synchronized` is reentrant, so `buildStart` may call `discardJob` on - * this pool synchronously without deadlock. + * this pool synchronously (used by the placeholder/no-task path). */ def tryBook(buildStart: S => Future[T]): Option[S] = synchronized { - if (jobs.size >= MAX_ACTIVE_JOBS) None + if (active.size >= MAX_ACTIVE_JOBS) None else { val jid: S = jid_fact(_nextJobId.getAndIncrement()) val promise = Promise[T]() - jobs(jid) = promise.future + active(jid) = promise.future promise.completeWith(buildStart(jid)) Some(jid) } } + /** Move the entry from `active` to `completed`. Slot freed; `lookupJob` + * still finds the entry until an explicit `discardJob` removes it. + */ + def markCompleted(jid: S): Unit = synchronized { + active.remove(jid).foreach { fut => completed(jid) = fut } + } + + /** Remove the entry from both maps. Used on explicit cancellation/cleanup. */ def discardJob(jid: S): Unit = synchronized { - jobs -= jid + active -= jid + completed -= jid } def lookupJob(jid: S): Option[Future[T]] = synchronized { - jobs.get(jid) + active.get(jid).orElse(completed.get(jid)) } } diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala index 0bd0dfa1..0c423a7f 100644 --- a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala +++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala @@ -9,6 +9,7 @@ package viper.server.vsi import java.util.concurrent.{Callable, FutureTask} import ch.qos.logback.classic.Logger +import scala.collection.mutable import scala.concurrent.{Future, Promise} import scala.util.Try @@ -24,13 +25,59 @@ import scala.util.Try * `enqueueMessage` and `registerTaskEnd` are both expected to be invoked from * the same producer (the worker thread). The stream's own synchronization * keeps things safe even if that contract is violated. + * + * Completion model: `settled` is the canonical "all internal cleanup is + * done" signal. Consumers chaining post-completion logic should await + * `settled` rather than `stream.watchCompletion` or `artifact`, because + * cleanup hooks registered via `onSettled` are guaranteed to have run + * before `settled` resolves AND before the stream's Done sentinel can + * unblock any iterator. This eliminates the multi-signal fanout race + * where a consumer wakes up on one signal while side-effects registered + * on another haven't run yet. * */ abstract class MessageStreamingTask[T] extends Callable[T] with Post { private lazy val artifactPromise = Promise[T]() lazy val artifact: Future[T] = artifactPromise.future + + private val settledPromise = Promise[Unit]() + /** Resolves after the producer has finished and every `onSettled` hook + * has run. Always resolves with `Success(())` — task failures are + * surfaced through `artifact`, not here. + */ + def settled: Future[Unit] = settledPromise.future + + private val cleanupHooks = mutable.ArrayBuffer.empty[() => Unit] + private var finalized = false + + /** Register cleanup to run inside the finalize sequence, BEFORE + * `stream.complete()` and BEFORE `settled` resolves. Hooks run + * synchronously on the producer's thread in registration order. + * + * If the task is already finalized, the hook runs inline. + * + * Hook exceptions are swallowed so a faulty hook cannot block + * subsequent hooks or signaling. + */ + def onSettled(hook: () => Unit): Unit = { + val runNow = this.synchronized { + if (finalized) true + else { cleanupHooks += hook; false } + } + if (runNow) { + try hook() catch { case _: Throwable => /* swallow */ } + } + } + lazy val futureTask: FutureTask[T] = new FutureTask(this) { - override def done(): Unit = artifactPromise.complete(Try(get())) + override def done(): Unit = { + // Backstop: if the task body threw before calling registerTaskEnd, + // we still need the stream to complete and `settled` to resolve so + // consumers don't hang. Idempotent — a normal completion already + // ran finalize and this is a no-op. + finalizeOnce() + artifactPromise.complete(Try(get())) + } } val stream: EnvelopeStream = new EnvelopeStream() @@ -49,6 +96,23 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { } } + /** Run cleanup hooks, complete the stream, then signal `settled`. + * Idempotent. Order matters: hooks run BEFORE `stream.complete()` so + * any iterator waking on the Done sentinel observes post-hook state. + */ + private def finalizeOnce(): Unit = { + val hooks = this.synchronized { + if (finalized) return + finalized = true + val h = cleanupHooks.toList + cleanupHooks.clear() + h + } + hooks.foreach { h => try h() catch { case _: Throwable => /* swallow */ } } + stream.complete() + settledPromise.trySuccess(()) + } + /** Closes the downstream stream, signalling the end of the message stream. * * @param success retained for API compatibility; stream completion is the same @@ -57,6 +121,6 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { */ protected def registerTaskEnd(success: Boolean, logger: Logger): Unit = { logger.trace(s"registerTaskEnd: $success") - stream.complete() + finalizeOnce() } } diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index c272afaf..c615e6d8 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -80,11 +80,15 @@ trait VerificationServer extends Post { case Some(task) => val execution = new JobExecution(task.futureTask) - task.stream.watchCompletion.onComplete(_ => { - if (discardOnCompletion) { - pool.discardJob(new_jid) - } - }) + if (discardOnCompletion) { + // Free the slot as part of the task's finalize sequence: hooks + // registered via `onSettled` run before the stream's Done + // sentinel is enqueued, so any iterator drainer is guaranteed + // to observe `markCompleted` before its `take()` can return. + // The entry stays retrievable via `lookupJob` until an + // explicit `discardJob` removes it. + task.onSettled(() => pool.markCompleted(new_jid)) + } execution.start(executor.executorService) From 3ffbcc9330a8831ab15b13097b04348a8392c86c Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 17:58:26 +0200 Subject: [PATCH 15/22] Per-FileContent monitor serializes buffer reads/writes against LSP threads --- .../frontends/lsp/file/FileContent.scala | 29 ++++++++++++------- .../frontends/lsp/file/ProjectManager.scala | 2 +- 2 files changed, 20 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 15630135..dd81288a 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -14,10 +14,13 @@ import java.nio.file.Path import org.eclipse.lsp4j.Position import viper.server.frontends.lsp.Common +// All public methods that read or mutate `fileContent` synchronize on the +// FileContent instance. The buffer is otherwise not thread-safe and the LSP +// dispatcher can call us from multiple worker threads concurrently. case class FileContent(path: Path) extends DiskLoader { case class FileContentIter(fc: FileContent, delta: Int, var currPos: Option[Position]) extends Iterator[(Char, Position)] { override def hasNext: Boolean = currPos.isDefined - override def next(): (Char, Position) = { + override def next(): (Char, Position) = fc.synchronized { val pos = currPos.get val char = fc.getCharAt(pos) pos.setCharacter(pos.getCharacter + delta) @@ -28,15 +31,17 @@ case class FileContent(path: Path) extends DiskLoader { val fileContent = new ArrayBuffer[String] - def set(newContent: String): Unit = { + def set(newContent: String): Unit = synchronized { fileContent.clear() fileContent.addAll(newContent.split("\n", -1)) } + def text: String = synchronized { fileContent.mkString("\n") } + override def loadContent(path: Path): Try[String] = - if (this.path == path) Success(fileContent.mkString("\n")) else super.loadContent(path) + if (this.path == path) Success(text) else super.loadContent(path) - def handleChange(range: Range, text: String): Unit = { + def handleChange(range: Range, text: String): Unit = synchronized { val startLine = range.getStart.getLine val startStr = fileContent(startLine).slice(0, range.getStart.getCharacter) val endLine = range.getEnd.getLine @@ -46,10 +51,14 @@ case class FileContent(path: Path) extends DiskLoader { fileContent.patchInPlace(startLine, lines, endLine - startLine + 1) } - def iterForward(pos: Position): FileContentIter = FileContentIter(this, 1, normalize(pos)) - def iterBackward(pos: Position): FileContentIter = FileContentIter(this, -1, normalize(pos)) + def iterForward(pos: Position): FileContentIter = synchronized { + FileContentIter(this, 1, normalize(pos)) + } + def iterBackward(pos: Position): FileContentIter = synchronized { + FileContentIter(this, -1, normalize(pos)) + } - def normalize(pos: Position): Option[Position] = { + def normalize(pos: Position): Option[Position] = synchronized { if (pos.getLine < 0 || pos.getLine >= fileContent.length) return None if (pos.getCharacter < 0) { val newPos = new Position(pos.getLine - 1, pos.getCharacter) @@ -70,12 +79,12 @@ case class FileContent(path: Path) extends DiskLoader { return Some(new Position(pos.getLine, pos.getCharacter)) } } - def getCharAt(pos: Position): Char = { + def getCharAt(pos: Position): Char = synchronized { val line = fileContent(pos.getLine) if (pos.getCharacter == line.length) '\n' else line(pos.getCharacter) } - def getIdentAtPos(pos: Position): Option[(String, Range)] = { + def getIdentAtPos(pos: Position): Option[(String, Range)] = synchronized { normalize(pos).flatMap(nPos => { val start = iterBackward(nPos).drop(1).takeWhile { case (c, _) => Common.isIdentChar(c) }.length val startPos = new Position(nPos.getLine, nPos.getCharacter - start) @@ -88,7 +97,7 @@ case class FileContent(path: Path) extends DiskLoader { } }) } - def inComment(pos: Position): Boolean = { + def inComment(pos: Position): Boolean = synchronized { normalize(pos).map(nPos => { var isComment = false var noComment = false diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala index 18d9fc90..e2d6e7e7 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala @@ -65,7 +65,7 @@ trait ProjectManager extends ProjectAware { case Right(li) => li.addRoot(newRoot) } - if (getContents) Some(root.content.fileContent.mkString("\n")) else None + if (getContents) Some(root.content.text) else None } def addToThisProject(uri: String): LeafManager = { From b4da41b6d89ef40fda7d53143db2fd99f2c17be8 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 7 May 2026 18:17:24 +0200 Subject: [PATCH 16/22] S3.1: Per-FileManager monitor serializes ProjectManager mutators --- .../frontends/lsp/file/FileManager.scala | 6 +- .../frontends/lsp/file/ProjectManager.scala | 136 ++++++++++++------ 2 files changed, 97 insertions(+), 45 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala index e0687188..934d9052 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala @@ -56,7 +56,11 @@ case class FileManager(root: LeafManager)(implicit executor: VerificationExecuti override val ec: VerificationExecutionContext = executor var isOpen: Boolean = true - def close(): Unit = synchronized { + def close(): Unit = { + // Both callees manage their own locking. We deliberately do NOT wrap + // them in `synchronized(this)` — `teardownProject` makes cross-instance + // calls and would deadlock against a leaf doing `handleContentChange` + // if we held our monitor across them. teardownProject() stopRunningVerification() } diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala index e2d6e7e7..5d427732 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala @@ -41,7 +41,27 @@ trait ProjectAware extends ManagesLeaf { /** Manages a Viper project consisting of the root file and all imported files. * Note that any Viper file can be either of the two: a root of a project or as - * a leaf in other project(s). See documentation of `ClientCoordinator`. */ + * a leaf in other project(s). See documentation of `ClientCoordinator`. + * + * Concurrency: reads and writes of `project` (and the inner `Map` / + * `LeafInfo`) are guarded by the FileManager's intrinsic monitor (the same + * lock used by `Verification` mutators per S3). Methods that fan out to + * other FileManagers via `coordinator.{addToOther,removeFromOther,handleChangeInLeaf}` + * release the lock before making those cross-instance calls — otherwise + * concurrent root↔leaf interactions (e.g. `setupProject` on a root vs. + * `handleContentChange` on one of its leaves) would deadlock through + * inverted lock acquisition. + * + * The protocol is: + * 1. Read or mutate `project` under `synchronized(this)`. + * 2. Capture any plan that requires cross-instance calls (a list of leaves + * to notify, etc.). + * 3. Release the lock and execute the cross-instance calls. + * 4. If a follow-up local mutation depends on the result, re-acquire the + * lock and double-check before installing. + * + * This protects against torn reads/writes; it does not by itself make + * compound updates atomic across cross-instance call windows. */ trait ProjectManager extends ProjectAware { /** The current project for which this is a root (Left), or the set of project * roots for which this file is a leaf (Right). If this is a leaf, this @@ -50,7 +70,7 @@ trait ProjectManager extends ProjectAware { var project: Either[Map[String, LeafManager], LeafInfo] = Left(Map()) private def getRootOpt: Option[Map[String, LeafManager]] = project.left.toOption - def removeFromOtherProject(toRemove: String): Boolean = { + def removeFromOtherProject(toRemove: String): Boolean = synchronized { val becomeRoot = project.map(li => li.removeRoot(toRemove)).getOrElse(false); if (becomeRoot) { project = Left(Map()) @@ -58,59 +78,79 @@ trait ProjectManager extends ProjectAware { becomeRoot } def addToOtherProject(newRoot: String, getContents: Boolean): Option[String] = { + // teardownProject performs cross-instance calls and manages its own + // locking; do it before we reacquire to install the new leaf state. teardownProject() - project match { - case Left(_) => - project = Right(LeafInfo(newRoot)) - case Right(li) => - li.addRoot(newRoot) + synchronized { + project match { + case Left(_) => + project = Right(LeafInfo(newRoot)) + case Right(li) => + li.addRoot(newRoot) + } } if (getContents) Some(root.content.text) else None } def addToThisProject(uri: String): LeafManager = { - val project = getRootOpt.get - val existing = project.get(uri) - // We need to call this even if `existing` is defined to set ourselves as - // the `lastRoot` in the `LeafInfo` of the leaf. + val existing = synchronized { getRootOpt.get.get(uri) } + // Cross-instance call without holding our lock: the leaf may want its + // own monitor, and one of its callbacks could otherwise deadlock with + // ours. val file = coordinator.addToOtherProject(uri, file_uri, existing.isEmpty) - existing.getOrElse({ - coordinator.logger.error("Creating new LeafManager for " + uri) - val l = LeafManager(uri, file.get, coordinator) - project.put(uri, l) - l - }) + existing.getOrElse { + synchronized { + // Re-read in case `project` was replaced or another thread already + // installed a manager for this uri while we were unlocked. + val pm = getRootOpt.get + pm.get(uri).getOrElse { + coordinator.logger.error("Creating new LeafManager for " + uri) + val l = LeafManager(uri, file.get, coordinator) + pm.put(uri, l) + l + } + } + } } - def teardownProject() = { - removeDiagnostics() - for (p <- projectLeaves; leaf <- p) { - coordinator.removeFromOtherProject(leaf, file_uri) + def teardownProject(): Unit = { + val leaves = synchronized { + removeDiagnostics() + projectLeaves.getOrElse(Set.empty).toList } + leaves.foreach(leaf => coordinator.removeFromOtherProject(leaf, file_uri)) } - def setupProject(imports: Set[String]) = { - val oldProject = getRootOpt.getOrElse(Map()) - val toRemove = oldProject.keySet.diff(imports) - for (p <- toRemove) { - oldProject.remove(p) - coordinator.removeFromOtherProject(p, file_uri) + def setupProject(imports: Set[String]): Unit = { + // Phase 1: under the lock, compute the diff, mutate the inner map, and + // republish `project`. We do NOT make cross-instance calls here. + val toRemove = synchronized { + val oldProject = getRootOpt.getOrElse(Map()) + val tr = oldProject.keySet.diff(imports).toList + tr.foreach(oldProject.remove) + project = Left(oldProject) + tr } - project = Left(oldProject) + // Phase 2: notify removed leaves outside the lock. + toRemove.foreach(coordinator.removeFromOtherProject(_, file_uri)) + // Phase 3: addToThisProject manages its own locking. for (p <- imports) { addToThisProject(p) } - - val setupProject = SetupProjectParams(file_uri, imports.toArray) - coordinator.client.map{_.requestSetupProject(setupProject)} + coordinator.client.map(_.requestSetupProject(SetupProjectParams(file_uri, imports.toArray))) } - def projectRoot: Option[String] = project.toOption.map(_.lastRoot) - def projectLeaves: Option[Set[String]] = getRootOpt.map(_.keySet) - def projectManagers: Option[Iterator[LeafManager]] = getRootOpt.map(p => Iterator(root) ++ p.valuesIterator) - def isRoot: Boolean = project.isLeft + def projectRoot: Option[String] = synchronized { project.toOption.map(_.lastRoot) } + def projectLeaves: Option[Set[String]] = synchronized { getRootOpt.map(_.keySet.toSet) } + def projectManagers: Option[Iterator[LeafManager]] = synchronized { + // Materialize the iterator under the lock so callers iterate a stable + // snapshot rather than a live view of the mutable map. + getRootOpt.map(p => (Iterator(root) ++ p.valuesIterator).toList.iterator) + } + def isRoot: Boolean = synchronized { project.isLeft } - override def getInProjectOpt(uri: String): Option[LeafManager] = + override def getInProjectOpt(uri: String): Option[LeafManager] = synchronized { if (unescape(uri) == unescape(file_uri)) Some(root) else getRootOpt.get.get(uri) + } /** Gets a file in the current project, or adds it if missing. The latter can * happen when, e.g. we get errors in imported files before we get the * `PProgram` itself (to setup the project). @@ -219,20 +259,28 @@ trait ProjectManager extends ProjectAware { * of, so that they can update their local `LeafManager`s for this file */ def handleContentChange(range: Range, text: String): Unit = { root.handleContentChange(range, text) - project.foreach(_.rootsIter.foreach(root => { - coordinator.handleChangeInLeaf(root, file_uri, range, text) - })) + val rootsToNotify = synchronized { + project.toOption.fold(List.empty[String])(_.rootsIter.toList) + } + rootsToNotify.foreach(r => coordinator.handleChangeInLeaf(r, file_uri, range, text)) } /** The `ProjectManager` of one of my leaves received a content change * message, update my local `LeafManager` instance to reflect that. */ def handleChangeInLeaf(leaf: String, range: Range, text: String): Unit = { - project match { - case Left(project) => project.get(leaf) match { - case None => coordinator.logger.error(s"handleChangeInLeaf called on project without leaf (${leaf})") - case Some(v) => v.handleContentChange(range, text) + val target = synchronized { + project match { + case Left(p) => Right(p.get(leaf)) + case Right(_) => Left(()) } - case _ => coordinator.logger.error("handleChangeInLeaf called on non-root") + } + target match { + case Left(_) => + coordinator.logger.error("handleChangeInLeaf called on non-root") + case Right(None) => + coordinator.logger.error(s"handleChangeInLeaf called on project without leaf (${leaf})") + case Right(Some(v)) => + v.handleContentChange(range, text) } } From 1fee141646197d9c708243c6c55cf2faa839c68e Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 09:50:19 +0200 Subject: [PATCH 17/22] B1+C2+B10: Lift logger into MessageStreamingTask; route lifecycle printlns --- .../viper/server/ViperServerRunner.scala | 25 ++++++++++-------- .../server/core/MessageReportingTask.scala | 8 +----- .../viper/server/core/ViperCoreServer.scala | 2 +- .../server/vsi/MessageStreamingTask.scala | 26 +++++++++++++------ .../viper/server/vsi/VerificationServer.scala | 14 +++++++--- 5 files changed, 44 insertions(+), 31 deletions(-) diff --git a/src/main/scala/viper/server/ViperServerRunner.scala b/src/main/scala/viper/server/ViperServerRunner.scala index 4c5ea47c..db79637e 100644 --- a/src/main/scala/viper/server/ViperServerRunner.scala +++ b/src/main/scala/viper/server/ViperServerRunner.scala @@ -23,6 +23,7 @@ object ViperServerRunner { var viperServerHttp: ViperHttpServer = _ def main(args: Array[String]): Unit = { + // Banner emitted before the server (and thus its logger) is constructed. println(s"${BuildInfo.projectName} ${BuildInfo.projectVersionExtended}") val config = new ViperConfig(args.toIndexedSeq) val executor = new DefaultVerificationExecutionContext(threadPoolSize = Some(config.nThreads())) @@ -43,9 +44,9 @@ object ViperServerRunner { viperServerHttp.start() // wait until server has been stopped: Await.ready(viperServerHttp.stopped(), Duration.Inf) - println("HTTP server has been stopped") + viperServerHttp.globalLogger.info("HTTP server has been stopped") executor.terminate() - println("executor service has been shut down") + viperServerHttp.globalLogger.info("executor service has been shut down") // the following `exit` call is required such that the server eventually terminates for `longDuration.vpr` in the // test suite of viper-ide System.exit(0) @@ -55,26 +56,29 @@ object ViperServerRunner { * Run VCS in LSP mode. */ private def runLspServer(config: ViperConfig)(implicit executor: VerificationExecutionContext): Unit = { + var serverOpt: Option[ViperServerService] = None try { val done = startServer(config) .flatMap { case (serverSocket, server) => + serverOpt = Some(server) val url = serverSocket.getInetAddress.getHostAddress val port = serverSocket.getLocalPort val serverUrl = s"$url:$port" announcePort(port) - println(s"going to listen on port $port for LSP") + server.globalLogger.info(s"going to listen on port $port for LSP") processRequests(config, serverSocket, server, serverUrl) } // wait until server is done: Await.result(done, Duration.Inf) - println("all clients have been processed") + serverOpt.foreach(_.globalLogger.info("all clients have been processed")) executor.terminate() - println("executor service has been shut down") + serverOpt.foreach(_.globalLogger.info("executor service has been shut down")) System.exit(0) } catch { case e: IOException => - println(s"IOException occurred: ${e.toString}") + // Logger may not exist yet if startup itself failed; use stderr. + System.err.println(s"IOException occurred: ${e.toString}") System.exit(1) } } @@ -87,9 +91,8 @@ object ViperServerRunner { } private def announcePort(port: Int): Unit = { - // write port number in a predefined format to standard output such that clients can parse it - // do not change this format without adapting clients such as the Viper-IDE client - // regex for parsing: "" + // Machine-parsed contract — must stay on stdout in this exact format. + // Clients (e.g. Viper-IDE) match the regex "". println(s"") } @@ -110,14 +113,14 @@ object ViperServerRunner { * The returned future completes when stream is closed. */ private def handleClient(config: ViperConfig, server: ViperServerService, socket: Socket, serverUrl: String)(implicit executor: VerificationExecutionContext): Future[Unit] = { - println(s"client connected: ${socket.toString}") + server.globalLogger.info(s"client connected: ${socket.toString}") val receiver: CustomReceiver = new CustomReceiver(config, server, serverUrl) val launcher = createLauncher(receiver, socket)(executor) receiver.connect(launcher.getRemoteProxy) // convert Java Future to Scala Future: Future { launcher.startListening().get() - println(s"client disconnected: ${socket.toString}") + server.globalLogger.info(s"client disconnected: ${socket.toString}") receiver.disconnected() socket.close() } diff --git a/src/main/scala/viper/server/core/MessageReportingTask.scala b/src/main/scala/viper/server/core/MessageReportingTask.scala index e7b35b0e..77f875ac 100644 --- a/src/main/scala/viper/server/core/MessageReportingTask.scala +++ b/src/main/scala/viper/server/core/MessageReportingTask.scala @@ -6,21 +6,15 @@ package viper.server.core -import ch.qos.logback.classic.Logger import viper.server.vsi.MessageStreamingTask import viper.silver.reporter.{EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter} trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost { def executor: VerificationExecutionContext - def logger: Logger protected def enqueueMessage(msg: Message): Unit = { - super.enqueueMessage(pack(msg), logger) - } - - protected def registerTaskEnd(success: Boolean): Unit = { - super.registerTaskEnd(success, logger) + super.enqueueMessage(pack(msg)) } // Implementation of the Reporter interface used by the backend. diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala index 5010e991..1f330fc2 100644 --- a/src/main/scala/viper/server/core/ViperCoreServer.scala +++ b/src/main/scala/viper/server/core/ViperCoreServer.scala @@ -27,7 +27,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V /** allows subclasses to return their own global logger */ def getGlobalLogger(config: ViperConfig): Logger = { val logger = ViperLogger("ViperServerLogger", config.getLogFileWithGuarantee, config.logLevel()) - println(s"Writing [level:${config.logLevel()}] logs into " + + logger.get.info(s"Writing [level:${config.logLevel()}] logs into " + s"${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}") logger.get } diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala index 0c423a7f..1fc6689b 100644 --- a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala +++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala @@ -37,6 +37,12 @@ import scala.util.Try * */ abstract class MessageStreamingTask[T] extends Callable[T] with Post { + /** The logger used for trace/error output from the streaming machinery. + * Subclasses must provide this; it is also the canonical logger for + * hook failures and similar diagnostics. + */ + def logger: Logger + private lazy val artifactPromise = Promise[T]() lazy val artifact: Future[T] = artifactPromise.future @@ -56,8 +62,8 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { * * If the task is already finalized, the hook runs inline. * - * Hook exceptions are swallowed so a faulty hook cannot block - * subsequent hooks or signaling. + * Hook exceptions are logged and swallowed so a faulty hook cannot + * block subsequent hooks or signaling. */ def onSettled(hook: () => Unit): Unit = { val runNow = this.synchronized { @@ -65,7 +71,7 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { else { cleanupHooks += hook; false } } if (runNow) { - try hook() catch { case _: Throwable => /* swallow */ } + try hook() catch { case e: Throwable => logger.warn(s"onSettled hook failed: $e") } } } @@ -85,7 +91,7 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { /** Offers `msg` to the downstream stream, blocking until queue space is available * (natural backpressure when consumers are slow). */ - protected def enqueueMessage(msg: Envelope, logger: Logger): Unit = { + protected def enqueueMessage(msg: Envelope): Unit = { logger.trace(s"enqueueMessage: $msg") try { stream.offer(msg) @@ -97,8 +103,10 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { } /** Run cleanup hooks, complete the stream, then signal `settled`. - * Idempotent. Order matters: hooks run BEFORE `stream.complete()` so - * any iterator waking on the Done sentinel observes post-hook state. + * Idempotent. Order matters: hooks run BEFORE `stream.complete()` and + * BEFORE `settledPromise` resolves so any consumer awaiting `settled` + * (or any iterator waking on the Done sentinel) observes post-hook + * state. */ private def finalizeOnce(): Unit = { val hooks = this.synchronized { @@ -108,7 +116,9 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { cleanupHooks.clear() h } - hooks.foreach { h => try h() catch { case _: Throwable => /* swallow */ } } + hooks.foreach { h => + try h() catch { case e: Throwable => logger.warn(s"onSettled hook failed: $e") } + } stream.complete() settledPromise.trySuccess(()) } @@ -119,7 +129,7 @@ abstract class MessageStreamingTask[T] extends Callable[T] with Post { * regardless of success/failure outcome. Idempotent (a second * call is a no-op). */ - protected def registerTaskEnd(success: Boolean, logger: Logger): Unit = { + protected def registerTaskEnd(success: Boolean): Unit = { logger.trace(s"registerTaskEnd: $success") finalizeOnce() } diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index c615e6d8..99ad3708 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -8,6 +8,7 @@ package viper.server.vsi import java.util.concurrent.atomic.AtomicBoolean +import ch.qos.logback.classic.Logger import viper.server.core.VerificationExecutionContext import scala.concurrent.Future @@ -36,6 +37,12 @@ trait VerificationServer extends Post { implicit val executor: VerificationExecutionContext + /** Logger used by lifecycle and error paths in this trait. Implementing + * classes already maintain a server-wide logger; expose it here so the + * trait doesn't fall back to `println` when it needs to report. + */ + def globalLogger: Logger + /** Hook invoked from `stop()` after all jobs have been interrupted. Default * is a no-op. The HTTP frontend overrides this to unbind its server port. */ @@ -112,8 +119,7 @@ trait VerificationServer extends Post { }).recover({ case e: AstConstructionException => // If the AST construction phase failed, drop the verification job handle. - val msg = s"AST construction job ${prev_job_id_maybe.get} resulted in a failure: $e" - println(msg) + globalLogger.error(s"AST construction job ${prev_job_id_maybe.get} resulted in a failure: $e") pool.discardJob(new_jid) }).mapTo[T]) } @@ -206,8 +212,8 @@ trait VerificationServer extends Post { getInterruptFutureList().transform(r => { onExit() r match { - case Success(_) => println(s"shutting down...") - case Failure(_) => println(s"forcibly shutting down...") + case Success(_) => globalLogger.info("shutting down...") + case Failure(e) => globalLogger.warn(s"forcibly shutting down: $e") } r }) From 40de03eab536ff363d2e73ca4cec92a7369566d5 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 09:52:16 +0200 Subject: [PATCH 18/22] B1+B4: HTTP frontend uses globalLogger and bounded await timeouts --- .../frontends/http/ViperHttpServer.scala | 69 +++++++++++++------ 1 file changed, 48 insertions(+), 21 deletions(-) diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala index 1cb53194..5ea957db 100644 --- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala +++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala @@ -18,12 +18,25 @@ import viper.server.frontends.http.jsonWriters.ViperIDEProtocol._ import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile} import viper.server.vsi._ -import scala.concurrent.{Future, Promise} +import scala.concurrent.{Await, Future, Promise, TimeoutException} +import scala.concurrent.duration.{Duration, DurationInt} import scala.util.{Failure, Success} class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContext) extends ViperCoreServer(config)(executor) { + /** Bounded timeout for waiting on internal job handles in HTTP routes. + * Handle futures normally resolve in microseconds (AST) or as fast as + * AST construction (verification). Anything longer means a wedged job + * that should not be allowed to permanently steal an HTTP worker thread. + */ + private val handleAwaitTimeout: Duration = 60.seconds + + /** Bounded timeout for the synchronous shutdown path. Job interrupts + * should resolve well within this window. + */ + private val stopAwaitTimeout: Duration = 30.seconds + var port: Int = 0 private var undertow: Undertow = _ private val stoppedPromise: Promise[Unit] = Promise() @@ -40,7 +53,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex undertow.start() val boundAddr = undertow.getListenerInfo.get(0).getAddress.asInstanceOf[InetSocketAddress] port = boundAddr.getPort - println(s"ViperServer online at http://localhost:$port") + globalLogger.info(s"ViperServer online at http://localhost:$port") () }(executor) } @@ -64,15 +77,14 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex * completes the `stopped()` future. */ private[http] def handleExit(): String = { - val confirmation = scala.util.Try(scala.concurrent.Await.result( - stop(), scala.concurrent.duration.Duration.Inf)) + val confirmation = scala.util.Try(Await.result(stop(), stopAwaitTimeout)) val msg = confirmation match { case Success(_) => - println("shutting down...") + globalLogger.info("shutting down...") "shutting down..." case Failure(err_msg) => globalLogger.error(s"Interrupting one of the verification threads timed out: $err_msg") - println("forcibly shutting down...") + globalLogger.warn("forcibly shutting down...") "forcibly shutting down..." } stoppedPromise.complete(confirmation.map(_ => ())) @@ -106,8 +118,13 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex val ast_id = AstJobId(id) ast_jobs.lookupJob(ast_id) match { case Some(handle_future) => - val handle = scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf) - jsonLineResponse(handle.stream.iterator) + scala.util.Try(Await.result(handle_future, handleAwaitTimeout)) match { + case Success(handle) => jsonLineResponse(handle.stream.iterator) + case Failure(_: TimeoutException) => + textJsonResponse(VerificationRequestReject(s"Timed out waiting for AST job #$id handle.").toJson.compactPrint) + case Failure(e) => + textJsonResponse(VerificationRequestReject(s"AST job #$id failed: $e").toJson.compactPrint) + } case None => textJsonResponse(VerificationRequestReject(s"The verification job #$id does not exist.").toJson.compactPrint) } @@ -119,19 +136,27 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex case None => textJsonResponse(verificationRequestRejectionString(id, JobNotFoundException)) case Some(handle_future) => - val ver_handle = scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf) - val ast_id = ver_handle.prev_job_id - val ast_iter: Iterator[Envelope] = ast_id.flatMap(id => ast_jobs.lookupJob(id)) match { - case Some(astFut) => - val astHandle = scala.concurrent.Await.result(astFut, scala.concurrent.duration.Duration.Inf) - astHandle.stream.iterator - case None => Iterator.empty - } - val ver_iter: Iterator[Envelope] = ver_handle match { - case VerHandle(null, null, _) => Iterator.empty - case _ => ver_handle.stream.iterator + scala.util.Try(Await.result(handle_future, handleAwaitTimeout)) match { + case Failure(_: TimeoutException) => + textJsonResponse(VerificationRequestReject(s"Timed out waiting for verification job #$id handle.").toJson.compactPrint) + case Failure(e) => + textJsonResponse(verificationRequestRejectionString(id, e)) + case Success(ver_handle) => + val ast_id = ver_handle.prev_job_id + val ast_iter: Iterator[Envelope] = ast_id.flatMap(jid => ast_jobs.lookupJob(jid)) match { + case Some(astFut) => + scala.util.Try(Await.result(astFut, handleAwaitTimeout)) match { + case Success(astHandle) => astHandle.stream.iterator + case Failure(_) => Iterator.empty + } + case None => Iterator.empty + } + val ver_iter: Iterator[Envelope] = ver_handle match { + case VerHandle(null, null, _) => Iterator.empty + case _ => ver_handle.stream.iterator + } + jsonLineResponse(ast_iter ++ ver_iter) } - jsonLineResponse(ast_iter ++ ver_iter) } } @@ -139,11 +164,13 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex val ver_id = VerJobId(id) ver_jobs.lookupJob(ver_id) match { case Some(handle_future) => - scala.util.Try(scala.concurrent.Await.result(handle_future, scala.concurrent.duration.Duration.Inf)) match { + scala.util.Try(Await.result(handle_future, handleAwaitTimeout)) match { case Success(handle) => val msg = formatInterruptResult(ver_id, handle.execution.cancel()) globalLogger.info(s"The verification job #$id was successfully stopped.") JobDiscardAccept(msg).toJson.compactPrint + case Failure(_: TimeoutException) => + JobDiscardReject(s"Timed out waiting for verification job #$id handle.").toJson.compactPrint case Failure(_) => JobDiscardReject(s"The verification job #$id does not exist.").toJson.compactPrint } From d272a50249c7f3e468519c47ca397b4982d37c68 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 09:55:43 +0200 Subject: [PATCH 19/22] B3+C5: Drop no-op delay(10); avoid non-local return in Future callback --- .../frontends/lsp/file/Verification.scala | 64 +++++++++---------- 1 file changed, 29 insertions(+), 35 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index f99db7aa..3ad3aeb3 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -11,8 +11,6 @@ import viper.server.frontends.lsp import scala.concurrent.Future import viper.server.core.{ViperBackendConfig, VerificationExecutionContext} import viper.server.vsi.{AstJobId, VerJobId} -import scala.concurrent.Promise -import java.util.concurrent.TimeUnit import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ @@ -106,20 +104,16 @@ trait VerificationManager extends ManagesLeaf { if (neverParsed) { runParseTypecheck(content) } - // Delay the future since `futureAst` returns a future from `watchCompletion` which states: - // "Note that this only means the elements have been passed downstream, not that downstream has successfully processed them." - val future = futureAst.map(_.andThen(delay(10)(_))).getOrElse(Future.successful(())) + // `futureAst` resolves only after `drainIteratorTo` has finished iterating + // the AST stream, which itself happens only after the producer's + // finalize sequence (`MessageStreamingTask.finalizeOnce`) has run all + // `onSettled` hooks and enqueued the Done sentinel. So by the time we + // observe completion here, every backend message has already been + // processed under the per-file monitor. + val future = futureAst.getOrElse(Future.successful(())) future.map(_ => this.synchronized(f)) } - def delay[T](ms: Int)(block: => T): Future[T] = { - val promise = Promise[T]() - ec.scheduler.schedule(new Runnable { - override def run(): Unit = promise.completeWith(Future(block)) - }, ms.toLong, TimeUnit.MILLISECONDS) - promise.future - } - //other var lastSuccess: VerificationSuccess = NA var internalErrorMessage: String = "" @@ -222,37 +216,37 @@ trait VerificationManager extends ManagesLeaf { pendingCancel.map(_ => synchronized { lastPhase = None - - val astJob = handler.astHandle match { + val astJobOpt: Option[AstJobId] = handler.astHandle match { // If an AST job is already running (due file edit or LSP features), reuse it instead of cancelling and rebuilding. case Some(existingAst) => coordinator.logger.info(s"Reusing existing AST job ${existingAst.id} for verification") manuallyTriggered = mt - existingAst + Some(existingAst) // Otherwise, start a new AST job for verification. case None => handler.clearWaitingOn() - startConstructAst(backend, loader, mt) match { - case None => return Future.successful(false) - case Some(ast) => ast - } + startConstructAst(backend, loader, mt) } - val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger)) - if (verJob.id >= 0) { - // Execute all handles - this.resetContainers(false) - this.resetDiagnostics(false) - errorCount = 0 - diagnosticCount = 0 - handler.waitOn(verJob) - val receiver = newRelayHandler(Some(backendClassName)) - futureVer = coordinator.server.startStreamingVer(verJob, receiver, Some(coordinator.localLogger)) - true - } else { - // Ver pool full — free the orphaned AST slot - coordinator.server.discardAstJobLookup(astJob) - false + astJobOpt match { + case None => false + case Some(astJob) => + val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger)) + if (verJob.id >= 0) { + // Execute all handles + this.resetContainers(false) + this.resetDiagnostics(false) + errorCount = 0 + diagnosticCount = 0 + handler.waitOn(verJob) + val receiver = newRelayHandler(Some(backendClassName)) + futureVer = coordinator.server.startStreamingVer(verJob, receiver, Some(coordinator.localLogger)) + true + } else { + // Ver pool full — free the orphaned AST slot + coordinator.server.discardAstJobLookup(astJob) + false + } } }) } From ac5a03a0ab1e6b55822518b91174fd66d9eb8455 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 09:55:49 +0200 Subject: [PATCH 20/22] A4: Drop VerificationExecutionContext.restart() dead API --- .../viper/server/core/VerificationExecutionContext.scala | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/main/scala/viper/server/core/VerificationExecutionContext.scala b/src/main/scala/viper/server/core/VerificationExecutionContext.scala index 90c7016b..fe888773 100644 --- a/src/main/scala/viper/server/core/VerificationExecutionContext.scala +++ b/src/main/scala/viper/server/core/VerificationExecutionContext.scala @@ -9,7 +9,7 @@ package viper.server.core import java.util.concurrent.{ExecutorService, Executors, ScheduledExecutorService, ThreadFactory, TimeUnit} import java.util.{concurrent => java_concurrent} -import scala.concurrent.{ExecutionContext, ExecutionContextExecutorService, Future} +import scala.concurrent.{ExecutionContext, ExecutionContextExecutorService} trait VerificationExecutionContext extends ExecutionContext { def executorService: ExecutorService @@ -17,10 +17,6 @@ trait VerificationExecutionContext extends ExecutionContext { def submit(r: Runnable): java_concurrent.Future[_] /** Terminate executor and scheduler. */ def terminate(timeoutMSec: Long = 1000): Unit - /** Restart (no-op now that the actor system is gone; retained for API - * compatibility with prior consumers). - */ - def restart(): Future[Unit] } object DefaultVerificationExecutionContext { @@ -78,6 +74,4 @@ class DefaultVerificationExecutionContext(threadNamePrefix: String = "thread", executorService.shutdown() executorService.awaitTermination(timeoutMSec, TimeUnit.MILLISECONDS) } - - override def restart(): Future[Unit] = Future.unit } From 84aba1cc704b037cc470d7781041bfd5a2330338 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 10:52:46 +0200 Subject: [PATCH 21/22] AK-12+AK-16: @volatile FileManager.isOpen; simplify JobExecution.cancel --- .../viper/server/frontends/lsp/file/FileManager.scala | 2 +- src/main/scala/viper/server/vsi/JobActor.scala | 9 +-------- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala index 934d9052..492771bc 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala @@ -54,7 +54,7 @@ trait ManagesLeaf { */ case class FileManager(root: LeafManager)(implicit executor: VerificationExecutionContext) extends MessageHandler { override val ec: VerificationExecutionContext = executor - var isOpen: Boolean = true + @volatile var isOpen: Boolean = true def close(): Unit = { // Both callees manage their own locking. We deliberately do NOT wrap diff --git a/src/main/scala/viper/server/vsi/JobActor.scala b/src/main/scala/viper/server/vsi/JobActor.scala index 832156ed..bc44c716 100644 --- a/src/main/scala/viper/server/vsi/JobActor.scala +++ b/src/main/scala/viper/server/vsi/JobActor.scala @@ -16,14 +16,7 @@ final class JobExecution[T](task: FutureTask[T]) { def start(executor: Executor): Unit = executor.execute(task) /** Returns true iff this call actually interrupted a still-running task. */ - def cancel(): Boolean = { - if (task != null && !task.isDone) { - task.cancel(true) - true - } else { - false - } - } + def cancel(): Boolean = task.cancel(true) def isDone: Boolean = task.isDone } From 840a034228a0f81f4fd97714c3cef98dd5edb915 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 8 May 2026 11:09:50 +0200 Subject: [PATCH 22/22] =?UTF-8?q?AB-5=20(partial):=20drop=20residual=20Akk?= =?UTF-8?q?a=20names=20=E2=80=94=20ActorReporter=E2=86=92StreamingReporter?= =?UTF-8?q?,=20RelayActor=E2=86=92RelayHandler,=20ProgressCoordinator?= =?UTF-8?q?=E2=86=92ProgressTracker?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/main/scala/viper/server/core/AstWorker.scala | 2 +- src/main/scala/viper/server/core/MessageReportingTask.scala | 4 ++-- src/main/scala/viper/server/core/VerificationWorker.scala | 6 +++--- .../{ProgressCoordinator.scala => ProgressTracker.scala} | 2 +- .../lsp/file/{RelayActor.scala => RelayHandler.scala} | 6 +++--- src/test/scala/viper/server/core/CoreServerSpec.scala | 2 +- 6 files changed, 11 insertions(+), 11 deletions(-) rename src/main/scala/viper/server/frontends/lsp/file/{ProgressCoordinator.scala => ProgressTracker.scala} (89%) rename src/main/scala/viper/server/frontends/lsp/file/{RelayActor.scala => RelayHandler.scala} (98%) diff --git a/src/main/scala/viper/server/core/AstWorker.scala b/src/main/scala/viper/server/core/AstWorker.scala index e001d517..3eb1c89d 100644 --- a/src/main/scala/viper/server/core/AstWorker.scala +++ b/src/main/scala/viper/server/core/AstWorker.scala @@ -34,7 +34,7 @@ class AstWorker(val file: String, private def constructAst(args: Seq[String]): Option[Program] = { - val reporter = new ActorReporter("AstGenerationReporter") + val reporter = new StreamingReporter("AstGenerationReporter") val astGen = new ViperAstGenerator(logger, reporter, args, disablePlugins = config.disablePlugins()) val ast_option: Option[Program] = try { diff --git a/src/main/scala/viper/server/core/MessageReportingTask.scala b/src/main/scala/viper/server/core/MessageReportingTask.scala index 77f875ac..e0d4a59e 100644 --- a/src/main/scala/viper/server/core/MessageReportingTask.scala +++ b/src/main/scala/viper/server/core/MessageReportingTask.scala @@ -18,11 +18,11 @@ trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost { } // Implementation of the Reporter interface used by the backend. - class ActorReporter(tag: String) extends PluginAwareReporter { + class StreamingReporter(tag: String) extends PluginAwareReporter { val name = s"ViperServer_$tag" def doReport(msg: Message): Unit = { - logger.trace(s"ActorReport received msg $msg") + logger.trace(s"StreamingReporter received msg $msg") msg match { case m: EntityFailureMessage if m.concerning.info.isCached => case m: EntitySuccessMessage if m.concerning.info.isCached => diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index ca84adcf..7d3376f3 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -65,17 +65,17 @@ class VerificationWorker(private val command: List[String], command match { case "silicon" :: args => logger.info("Creating new Silicon verification backend.") - backend = new ViperBackend("silicon", new SiliconFrontend(new ActorReporter("silicon"), logger), programId, program, disablePlugins = config.disablePlugins()) + backend = new ViperBackend("silicon", new SiliconFrontend(new StreamingReporter("silicon"), logger), programId, program, disablePlugins = config.disablePlugins()) backend.execute(args) success = true case "carbon" :: args => logger.info("Creating new Carbon verification backend.") - backend = new ViperBackend("carbon", new CarbonFrontend(new ActorReporter("carbon"), logger), programId, program, disablePlugins = config.disablePlugins()) + backend = new ViperBackend("carbon", new CarbonFrontend(new StreamingReporter("carbon"), logger), programId, program, disablePlugins = config.disablePlugins()) backend.execute(args) success = true case "custom" :: custom :: args => logger.info(s"Creating new verification backend based on class $custom.") - backend = new ViperBackend(custom, resolveCustomBackend(custom, new ActorReporter(custom)).get, programId, program, disablePlugins = config.disablePlugins()) + backend = new ViperBackend(custom, resolveCustomBackend(custom, new StreamingReporter(custom)).get, programId, program, disablePlugins = config.disablePlugins()) backend.execute(args) success = true case args => diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProgressCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/file/ProgressTracker.scala similarity index 89% rename from src/main/scala/viper/server/frontends/lsp/file/ProgressCoordinator.scala rename to src/main/scala/viper/server/frontends/lsp/file/ProgressTracker.scala index e5edc5b5..6c8a42b8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProgressCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProgressTracker.scala @@ -8,7 +8,7 @@ package viper.server.frontends.lsp.file import viper.server.frontends.lsp.{BackendOutput, BackendOutputType, ClientCoordinator} -class ProgressCoordinator(coordinator: ClientCoordinator, val nofPredicates: Int, val nofFunctions: Int, val nofMethods: Int) { +class ProgressTracker(coordinator: ClientCoordinator, val nofPredicates: Int, val nofFunctions: Int, val nofMethods: Int) { var currentFunctions = 0 var currentMethods = 0 diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayHandler.scala similarity index 98% rename from src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala rename to src/main/scala/viper/server/frontends/lsp/file/RelayHandler.scala index b65b7d19..a6578179 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayHandler.scala @@ -12,13 +12,13 @@ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} -import viper.server.frontends.lsp.file.ProgressCoordinator +import viper.server.frontends.lsp.file.ProgressTracker import viper.silver.parser._ trait MessageHandler extends ProjectManager with VerificationManager with QuantifierCodeLens with QuantifierInlayHints with SignatureHelp { override def newRelayHandler(backendClassName: Option[String]): RelayHandler = new RelayHandler(this, backendClassName) - var progress: ProgressCoordinator = null + var progress: ProgressTracker = null private def determineSuccess(code: Int): VerificationSuccess = { if (code != 0) { @@ -151,7 +151,7 @@ class RelayHandler(task: MessageHandler, backendClassName: Option[String]) { } case StatisticsReport(m, f, p, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") - task.progress = new ProgressCoordinator(coordinator, p, f, m) + task.progress = new ProgressTracker(coordinator, p, f, m) val params = lsp.StateChangeParams(VerificationRunning.id, progress = 0, filename = task.filename) coordinator.sendStateChangeNotification(params, Some(task)) case AstConstructionFailureMessage(_, res) => diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index ac3bb2cc..684560dc 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -391,7 +391,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { }) s"verification errors do not get filtered - Viper-IDE Issue #326" in withServer[ViperServerService]({ (core, context) => - // this unit test checks that both errors are correctly collected by the RelayActor + // this unit test checks that both errors are correctly collected by the RelayHandler // The reported errors are equal according to the standard equality on AbstractError even though they occur // on different lines. implicit val ctx: VerificationExecutionContext = context