diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..13109b4 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,12 @@ +version: 2 + +updates: + - package-ecosystem: github-actions + directory: "/" + schedule: + interval: monthly + day: monday + groups: + all: + patterns: + - "*" diff --git a/.github/workflows/license-check.yml b/.github/workflows/license-check.yml index c286d01..09a74de 100644 --- a/.github/workflows/license-check.yml +++ b/.github/workflows/license-check.yml @@ -17,7 +17,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout ViperServer repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Check license headers uses: viperproject/check-license-header@v2 with: diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index 2f6ba78..290b1a6 100644 --- a/.github/workflows/scala.yml +++ b/.github/workflows/scala.yml @@ -55,7 +55,7 @@ jobs: container: viperproject/viperserver:v4_z3_4.8.7 steps: - name: Checkout ViperServer - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: viperserver submodules: recursive @@ -87,7 +87,7 @@ jobs: echo "Silver: commit ${{ env.SILICON_SILVER_REF }}" >> versions.txt # first line overwrites versions.txt in case it already exists, all other append to the file - name: Upload version file - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: versions.txt path: versions.txt @@ -97,7 +97,7 @@ jobs: # note that the cache path is relative to the directory in which sbt is invoked. - name: Cache SBT - uses: actions/cache@v3 + uses: actions/cache@v4 with: path: | viperserver/sbt-cache/.sbtboot @@ -115,7 +115,7 @@ jobs: - name: Upload log files if: ${{ failure() }} - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: TestLogs path: viperserver/logs @@ -129,7 +129,7 @@ jobs: working-directory: viperserver/target/universal/stage/lib - name: Upload ViperServer skinny JARs - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: viperserver-skinny-jars path: viperserver/viperserver-skinny-jars.zip @@ -139,7 +139,7 @@ jobs: working-directory: viperserver - name: Upload ViperServer fat JAR - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: viperserver-fat-jar path: viperserver/target/scala-2.13/viperserver.jar @@ -149,7 +149,7 @@ jobs: working-directory: viperserver - name: Upload ViperServer test fat JAR - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: viperserver-test-fat-jar path: viperserver/target/scala-2.13/viperserver-test.jar @@ -171,20 +171,20 @@ jobs: steps: # we need to checkout the repo to have access to the test files - name: Checkout ViperServer - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: viperserver # we need to checkout the silicon repo to have access to the logback configuration file # as we do not use anything else except the logback config, we simply take the latest master branch (in all configurations) - name: Checkout Silicon - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: viperproject/silicon path: silicon - name: Download ViperServer test fat JAR - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: viperserver-test-fat-jar path: viperserver @@ -244,7 +244,7 @@ jobs: shell: bash - name: Setup Java JDK - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: '11' distribution: 'temurin' @@ -265,7 +265,7 @@ jobs: - name: Upload log files if: ${{ failure() }} - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: TestLogs-${{ runner.os }} path: viperserver/logs @@ -281,19 +281,19 @@ jobs: run: sudo apt-get install curl - name: Download ViperServer skinny JARs - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: viperserver-skinny-jars path: deploy - name: Download ViperServer fat JAR - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: viperserver-fat-jar path: deploy - name: Download version file - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: versions.txt @@ -365,19 +365,19 @@ jobs: runs-on: ubuntu-latest steps: - name: Download ViperServer skinny JARs - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: viperserver-skinny-jars path: deploy - name: Download ViperServer fat JAR - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: viperserver-fat-jar path: deploy - name: Download version file - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: versions.txt diff --git a/.github/workflows/update-submodules.yml b/.github/workflows/update-submodules.yml index 1b56357..fe2886e 100644 --- a/.github/workflows/update-submodules.yml +++ b/.github/workflows/update-submodules.yml @@ -17,7 +17,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Check out the repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: true @@ -54,7 +54,7 @@ jobs: - name: Open a pull request id: pr - uses: peter-evans/create-pull-request@v4 + uses: peter-evans/create-pull-request@v7 if: (env.PREV_SILICON_REF != env.CUR_SILICON_REF) || (env.PREV_CARBON_REF != env.CUR_CARBON_REF) with: # Use viper-admin's token to workaround a restriction of GitHub. diff --git a/carbon b/carbon index 759f3c1..c6807b8 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 759f3c1e80724d5ab6c53fc9cfb989ccc4be1fc6 +Subproject commit c6807b8f0e8b8c16684b91a1d3b9337be559c3ce diff --git a/silicon b/silicon index 46a35ff..16030e9 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 46a35ffb154afc8962a9e3646673bd62ccff33c4 +Subproject commit 16030e9adfbdbad875c68db4c5e4b0c381891f31 diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala index 0d54abd..0275556 100644 --- a/src/main/scala/viper/server/vsi/HTTP.scala +++ b/src/main/scala/viper/server/vsi/HTTP.scala @@ -78,7 +78,7 @@ 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") + _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), Terminator.GetNextTerminatorName) bindingFuture.map { serverBinding => val newPort = serverBinding.localAddress.getPort if (port == 0) { diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index e0b12ad..fc8ab94 100644 --- a/src/main/scala/viper/server/vsi/JobPool.scala +++ b/src/main/scala/viper/server/vsi/JobPool.scala @@ -10,6 +10,7 @@ import akka.actor.ActorRef import akka.stream.scaladsl.SourceQueueWithComplete import org.reactivestreams.Publisher +import java.util.concurrent.atomic.AtomicInteger import scala.collection.mutable import scala.concurrent.{Future, Promise} @@ -56,14 +57,14 @@ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS: 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 var _nextJobId: Int = 0 + 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) + val new_jid: S = jid_fact(_nextJobId.getAndIncrement()) _jobHandles(new_jid) = Promise() _jobExecutors(new_jid) = () => { @@ -79,7 +80,6 @@ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS: t_fut } } - _nextJobId = _nextJobId + 1 new_jid } diff --git a/src/main/scala/viper/server/vsi/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala index c4dd85b..271296e 100644 --- a/src/main/scala/viper/server/vsi/Terminator.scala +++ b/src/main/scala/viper/server/vsi/Terminator.scala @@ -10,6 +10,7 @@ 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 --- @@ -19,6 +20,14 @@ 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) diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala index 21b2957..fb44900 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -319,7 +319,7 @@ 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") + _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs), Terminator.GetNextTerminatorName) isRunning = true Future.successful(Done) }