Skip to content

Commit

Permalink
unifies job managers for parsing and type-checking and for the 3 modes
Browse files Browse the repository at this point in the history
  • Loading branch information
@ArquintL
ArquintL committed Jun 29, 2023
1 parent 686b53d commit 046fe54
Show file tree
Hide file tree
Showing 10 changed files with 196 additions and 577 deletions.
8 changes: 4 additions & 4 deletions src/main/scala/viper/gobra/Gobra.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ import viper.gobra.ast.internal.Program
import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
import viper.gobra.backend.BackendVerifier
import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage}
import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult}
import viper.gobra.frontend.Parser.ParseResult
import viper.gobra.frontend.info.{Info, TypeInfo}
import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraConfig}
import viper.gobra.reporting._
Expand Down Expand Up @@ -159,7 +159,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
for {
finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
_ = setLogLevel(finalConfig)
parseResults <- performParsing(finalConfig, pkgInfo)(executor)
parseResults = performParsing(finalConfig, pkgInfo)(executor)
typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults)(executor)
program <- performDesugaring(finalConfig, typeInfo)(executor)
program <- performInternalTransformations(finalConfig, pkgInfo, program)(executor)
Expand Down Expand Up @@ -243,7 +243,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
.setLevel(config.logLevel)
}

private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]] = {
private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Map[AbstractPackage, ParseResult] = {
if (config.shouldParse) {
val startMs = System.currentTimeMillis()
val res = Parser.parse(config, pkgInfo)(executor)
Expand All @@ -253,7 +253,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
}
res
} else {
Left(Vector())
Map.empty
}
}

Expand Down
300 changes: 40 additions & 260 deletions src/main/scala/viper/gobra/frontend/Parser.scala
View file

Large diffs are not rendered by default.

170 changes: 32 additions & 138 deletions src/main/scala/viper/gobra/frontend/TaskManager.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,22 +20,29 @@ object TaskManagerMode extends Enumeration {
val Lazy, Sequential, Parallel = Value
}

trait Job[R] {
trait Job[I, R] {
private lazy val precomputationResult: I = sequentialPrecompute()
private var compututationStarted = false
private val promise: Promise[R] = Promise()
def getFuture: Future[R] = promise.future
protected def compute(): R

def call(): R = {
protected def sequentialPrecompute(): I
protected def compute(precomputationResult: I): R

def triggerPrecomputation(): I = {
precomputationResult
}

def execute(): R = {
getFuture.value match {
case Some(Success(res)) => return res // return already computed type-checker result
case Some(Failure(exception)) => Violation.violation(s"Job resulted in exception: $exception")
case _ =>
}
Violation.violation(!compututationStarted, s"Job $this is already on-going")
compututationStarted = true
val res = try {
val res = compute()
try {
val res = compute(precomputationResult)
promise.success(res)
res
} catch {
Expand All @@ -44,160 +51,47 @@ trait Job[R] {
// propagate this exception for the case that `call` is executed synchronously:
throw e
}
res
}
}

trait ParallelJob[R] {
/*
protected def compute(): Future[R]
private var compututationStarted: Option[Future[R]] = None
def call(): Future[R] = {
compututationStarted.getOrElse {
val fut = compute()
compututationStarted = Some(fut)
fut
}
}
*/

private var compututationStarted = false
private val promise: Promise[R] = Promise()
def getFuture: Future[R] = promise.future
protected def compute(): Future[R]

def call(executionContext: GobraExecutionContext): Future[R] = {
getFuture.value match {
case Some(Success(res)) => return Future.successful(res) // return already computed type-checker result
case Some(Failure(exception)) => Violation.violation(s"Job resulted in exception: $exception")
case _ =>
}
Violation.violation(!compututationStarted, s"Job $this is already on-going")
compututationStarted = true
compute()
.map(res => {
promise.success(res)
res
})(executionContext)
}
}

class TaskManager[K, R](mode: TaskManagerMode) {
require(mode != Parallel)

private val jobs: ConcurrentMap[K, Job[R]] = new ConcurrentHashMap()
class TaskManager[K, I, R](mode: TaskManagerMode)(executionContext: GobraExecutionContext) {
private val jobs: ConcurrentMap[K, Job[I, R]] = new ConcurrentHashMap()

/**
* returns true if job has been inserted and thus was previously absent
*/
def addIfAbsent(id: K, job: Job[R], insertOnly: Boolean = false): Unit = {
def addIfAbsent(id: K, job: Job[I, R]): Unit = {
var isAbsent = false
// first insert job, then run it (if necessary)
jobs.computeIfAbsent(id, _ => {
isAbsent = true
job
})
// now run it but only if it's a new job:
if (isAbsent && !insertOnly) {
if (isAbsent) {
job.triggerPrecomputation()
mode match {
case Sequential => job.execute()
case Lazy => // don't do anything as of now
case Sequential => job.call()
case Parallel => Future{ job.execute() }(executionContext)
}
}
}
/*
def getFuture(id: K): Future[R] = {
val job = jobs.get(id)
Violation.violation(job != null, s"Task $id not found")
job.getFuture
}

def getAllFutures: Iterable[(K, Future[R])] =
jobs.asScala.toVector.map { case (key, job) => (key, job.getFuture) }
*/
def getResult(id: K): R = {
val job = jobs.get(id)
Violation.violation(job != null, s"Task $id not found")
getResultFromJob(job)
}
/*
def getAllResults(executionContext: GobraExecutionContext): Iterable[R] = mode match {
case Lazy | Sequential => jobs.values().asScala.map(getResultFromJob)
case Parallel =>
val futs = jobs.values().asScala.map(_.getFuture)
implicit val executor: GobraExecutionContext = executionContext
Await.result(Future.sequence(futs), Duration.Inf)
}
*/
def getAllResults: Iterable[R] =
jobs.values().asScala.map(getResultFromJob)
/*
def getAllResultsWithKeys(executionContext: GobraExecutionContext): Iterable[(K, R)] = mode match {
case Lazy | Sequential => jobs.asScala.toVector.map { case (key, job) => (key, getResultFromJob(job)) }
case Parallel =>
implicit val executor: GobraExecutionContext = executionContext
val futs = jobs.asScala.toVector.map { case (key, job) => job.getFuture.map(res => (key, res)) }
Await.result(Future.sequence(futs), Duration.Inf)
}
*/
def getAllResultsWithKeys: Iterable[(K, R)] =
jobs.asScala.toVector.map { case (key, job) => (key, getResultFromJob(job)) }

private def getResultFromJob(job: Job[R]): R = mode match {
case Lazy => job.call() // we perform the computation now that we need the result
case Sequential =>
// note that we cannot await the future here as type-checking of this package might not have started yet.
// Thus, we use `.call()` that either returns a previously calculated type-checking result or will calculate it.
job.call()
// case Parallel =>
// Await.result(job.getFuture, Duration.Inf)
}
}

class ParallelTaskManager[K, R] {
private val jobs: ConcurrentMap[K, ParallelJob[R]] = new ConcurrentHashMap()

/**
* returns true if job has been inserted and thus was previously absent
*/
def addIfAbsent(id: K, job: ParallelJob[R], insertOnly: Boolean = false)(executionContext: GobraExecutionContext): Future[R] = {
var isAbsent = false
// first insert job, then run it (if necessary)
val res = jobs.computeIfAbsent(id, _ => {
isAbsent = true
job
})
// now run it but only if it's a new job:
if (isAbsent && !insertOnly) {
job.call(executionContext)
mode match {
case Lazy => job.execute() // now we need the job's result
case _ =>
}
// return the future (either of the inserted job or the already existing job with the same id)
res.getFuture
Await.result(job.getFuture, Duration.Inf)
}

def getAllResultsWithKeys(executionContext: GobraExecutionContext): Iterable[(K, R)] = {
implicit val executor: GobraExecutionContext = executionContext
val futs = jobs.asScala.toVector.map { case (key, job) => job.getFuture.map(res => (key, res)) }
Await.result(Future.sequence(futs), Duration.Inf)
}
}

class FutureManager[K, R]() {
private val futures: ConcurrentMap[K, Future[R]] = new ConcurrentHashMap()

def addIfAbsent(id: K, futFn: () => Future[R]): Future[R] = {
// first insert job, then run it (if necessary)
futures.computeIfAbsent(id, _ => futFn())
}

def getFuture(id: K): Future[R] = {
val fut = futures.get(id)
Violation.violation(fut != null, s"Task $id not found")
fut
}

def getAllResults(executionContext: GobraExecutionContext): Iterable[R] = {
def getAllResultsWithKeys: Iterable[(K, R)] = {
implicit val executor: GobraExecutionContext = executionContext
Await.result(Future.sequence(futures.values().asScala), Duration.Inf)
val futs = jobs.asScala.toVector.map { case (key, job) =>
mode match {
case Lazy => job.execute() // now we need the job's result
case _ =>
}
job.getFuture.map(res => (key, res))
}
Await.result(Future.sequence(futs), Duration.Inf)
}
}
Loading

0 comments on commit 046fe54

Please sign in to comment.