From 8d5928088d8679648bbeb5b24d428a2dc4cdbe7c Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 5 Mar 2026 17:23:03 +0100 Subject: [PATCH 1/2] some ideas --- .../viper/server/vsi/VerificationServer.scala | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index ec777d9..bbb96ee 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -145,8 +145,6 @@ trait VerificationServer extends Post { }).recover({ case e: AstConstructionException => - // If the AST construction phase failed, remove the verification job handle - // from the corresponding pool. val msg = s"AST construction job ${prev_job_id_maybe.get} resulted in a failure: $e" println(msg) pool.discardJob(new_jid) @@ -239,9 +237,12 @@ trait VerificationServer extends Post { 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() + ver_handle match { + case VerHandle(null, null, null, _) => + Future.successful(Done) + case _ => + ver_handle.queue.watchCompletion() + } }) } } @@ -299,8 +300,13 @@ trait VerificationServer extends Post { handle_future.flatMap { case AstHandle(actor, _, _, _) => (actor ? VerificationProtocol.StopAstConstruction).mapTo[String] + case VerHandle(null, _, _, _) => + Future.successful("Job had no actor.") case VerHandle(actor, _, _, _) => (actor ? VerificationProtocol.StopVerification).mapTo[String] + }.recover { + case _: akka.pattern.AskTimeoutException => + "Job actor already terminated." } } toList val overall_interrupt_future: Future[List[String]] = Future.sequence(interrupt_future_list) From 4c5360f69d9fe57483bac01aa6d42becbd4f2f5d Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Fri, 6 Mar 2026 15:37:14 +0100 Subject: [PATCH 2/2] restored comments --- src/main/scala/viper/server/vsi/VerificationServer.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index bbb96ee..10f4491 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -145,6 +145,8 @@ trait VerificationServer extends Post { }).recover({ case e: AstConstructionException => + // If the AST construction phase failed, remove the verification job handle + // from the corresponding pool. val msg = s"AST construction job ${prev_job_id_maybe.get} resulted in a failure: $e" println(msg) pool.discardJob(new_jid) @@ -237,6 +239,8 @@ trait VerificationServer extends Post { 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 match { case VerHandle(null, null, null, _) => Future.successful(Done)