Skip to content

Commit

Permalink
Wait for Server Start (#42)
Browse files Browse the repository at this point in the history
* changes server start to return a future and complete only when server has been started

* removes unused import

* implements CR suggestions by Arshavir
  • Loading branch information
ArquintL committed Jul 5, 2021
1 parent 6ad85da commit a9ec059
Show file tree
Hide file tree
Showing 7 changed files with 61 additions and 36 deletions.
8 changes: 5 additions & 3 deletions src/main/scala/viper/server/core/ViperCoreServer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -34,15 +34,17 @@ class ViperCoreServer(val config: ViperConfig)(implicit val executor: Verificati
* This function must be called before any other. Calling any other function before this one
* will result in an IllegalStateException.
* */
def start(): Unit = {
def start(): Future[Done] = {
_logger = ViperLogger("ViperServerLogger", config.getLogFileWithGuarantee, config.logLevel())
println(s"Writing [level:${config.logLevel()}] logs into " +
s"${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}")

ViperCache.initialize(logger.get, config.backendSpecificCache())

super.start(config.maximumActiveJobs())
logger.get.info(s"ViperCoreServer has started.")
super.start(config.maximumActiveJobs()) map { _ =>
logger.get.info(s"ViperCoreServer has started.")
Done
}
}

def requestAst(arg_list: List[String]): AstJobId = {
Expand Down
16 changes: 8 additions & 8 deletions src/main/scala/viper/server/frontends/http/ViperHttpServer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

package viper.server.frontends.http

import akka.NotUsed
import akka.{Done, NotUsed}
import akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport._
import akka.http.scaladsl.marshalling.ToResponseMarshallable
import akka.http.scaladsl.server.Directives._
Expand All @@ -20,28 +20,28 @@ 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.utility.Helpers.{getArgListFromArgString, validateViperFile}
import viper.server.utility.ibm
import viper.server.vsi.Requests.CacheResetRequest
import viper.server.vsi._
import viper.silver.logger.ViperLogger
import viper.silver.reporter.Message

import scala.concurrent.Future
import scala.util.{Failure, Success, Try}

class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContext)
extends ViperCoreServer(config)(executor) with VerificationServerHttp {

override def start(): Unit = {
override def start(): Future[Done] = {
_logger = ViperLogger("ViperServerLogger", config.getLogFileWithGuarantee, config.logLevel())
println(s"Writing [level:${config.logLevel()}] logs into ${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}")

ViperCache.initialize(logger.get, config.backendSpecificCache())

port = config.port.toOption
.flatMap(p => if (p == 0) None else Some(p)) // also search for a free port if the provided one is zero
.getOrElse(ibm.Socket.findFreePort)
super.start(config.maximumActiveJobs())
println(s"ViperServer online at http://localhost:$port")
port = config.port.toOption.getOrElse(0) // 0 causes HTTP server to automatically select a free port
super.start(config.maximumActiveJobs()).map({ _ =>
println(s"ViperServer online at http://localhost:$port")
Done
})(executor)
}

def setRoutes(): Route = {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,12 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve

def setReady(backend: BackendProperties): Unit = {
Coordinator.backend = backend
start()
is_ready = true
val param = BackendReadyParams("Silicon", false, true)
Coordinator.client.notifyBackendReady(param)
Log.info("The backend is ready for verification")
start() map { _ =>
is_ready = true
val param = BackendReadyParams("Silicon", false, true)
Coordinator.client.notifyBackendReady(param)
Log.info("The backend is ready for verification")
}
}

def setStopping(): Unit = {
Expand Down
29 changes: 21 additions & 8 deletions src/main/scala/viper/server/vsi/HTTP.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

package viper.server.vsi

import akka.NotUsed
import akka.{Done, NotUsed}
import akka.actor.PoisonPill
import akka.http.scaladsl.Http
import akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport._
Expand Down Expand Up @@ -65,24 +65,37 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp {

def setRoutes(): Route

private var stoppedPromise: Promise[Unit] = _
private var stoppedPromise: Promise[Done] = _
var bindingFuture: Future[Http.ServerBinding] = _

/** The server has been stopped when `stopped` completes. Afterwards, the execution context can be terminated. */
override def start(active_jobs: Int): Unit = {
/**
* 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)
stoppedPromise = Promise()
bindingFuture = Http().newServerAt("localhost", port).bindFlow(setRoutes())
bindingFuture.map(_.whenTerminationSignalIssued)
_termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), "terminator")
isRunning = true
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
}
}

/** 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[Unit] = {
def stopped(): Future[Done] = {
stoppedPromise.future
}

Expand Down Expand Up @@ -118,7 +131,7 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp {
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(_ => ()))
stoppedPromise.complete(err.map(_ => Done))
complete( serverStopConfirmation(err) )
}
}
Expand Down
4 changes: 3 additions & 1 deletion src/main/scala/viper/server/vsi/VerificationServer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,14 @@ trait VerificationServer extends Post {
*
* 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.
* */
def start(active_jobs: Int): Unit = {
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")
isRunning = true
Future.successful(Done)
}

protected def initializeProcess[S <: JobId, T <: JobHandle : ClassTag]
Expand Down
15 changes: 7 additions & 8 deletions src/test/scala/viper/server/core/CoreServerSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -92,19 +92,18 @@ class CoreServerSpec extends AnyWordSpec with Matchers {
val logFile = Paths.get("logs", s"viperserver_journal_${System.currentTimeMillis()}.log").toFile
logFile.getParentFile.mkdirs
logFile.createNewFile()
val config = new ViperConfig(Array("--logLevel", "TRACE", "--logFile", logFile.getAbsolutePath))
val core = new ViperCoreServer(config)(verificationContext)
core.start()

val config = new ViperConfig(Seq("--logLevel", "TRACE", "--logFile", logFile.getAbsolutePath))
val testName = currentTestName match {
case Some(name) =>
core.logger.get.debug(s"server started for test case '$name'")
name
case Some(name) => name
case None => throw new Exception("no test name")
}
val core = new ViperCoreServer(config)(verificationContext)
val started = core.start().map({ _ =>
core.logger.get.debug(s"server started for test case '$testName'")
})(verificationContext)

// execute testCode
val testFuture = testCode(core, verificationContext)
val testFuture = started.flatMap({_ => testCode(core, verificationContext)})(verificationContext)
// if successful, try to stop core server
// if unsuccessful, stop core server but return error of testFuture
val testWithShutdownFuture = testFuture.transformWith(testRes => {
Expand Down
14 changes: 11 additions & 3 deletions src/test/scala/viper/server/core/ViperServerHttpSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,9 @@ class ViperServerHttpSpec extends AnyWordSpec with Matchers with ScalatestRouteT
private val verificationContext: VerificationExecutionContext = new DefaultVerificationExecutionContext()
private val viperServerHttp = {
val config = new ViperConfig(IndexedSeq())
val server = new ViperHttpServer(config)(verificationContext)
server.start()
server
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()
Expand Down Expand Up @@ -71,6 +71,14 @@ class ViperServerHttpSpec extends AnyWordSpec with Matchers with ScalatestRouteT
private val testNonExistingFile_cmd = s"$tool --disableCaching ${nonExistingFile}"

"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])
Expand Down

0 comments on commit a9ec059

Please sign in to comment.