viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Better Control over Concurrency #24

Closed ArquintL closed 3 years ago

ArquintL commented 3 years ago

This PR adds the possibility to pass an execution context consisting of a thread pool and actor system to ViperCoreServer

ArquintL commented 3 years ago

Copying the following test case to AsyncCoreServerSpec in master branch results in the same issues as on this branch:

private val ver_error_file = "src/test/resources/viper/verification_error.vpr"
private val empty_viper_file = "src/test/resources/viper/empty.vpr"
private val correct_viper_file = "src/test/resources/viper/sum_method.vpr"
private val files = List(empty_viper_file, correct_viper_file, ver_error_file)
private val asts = files.map((new AstGenerator(SilentLogger().get).generateViperAst(_).get))
private def getAstByFileName(file: String): Program =
  (files zip asts collect {
    case (f, ast) if f==file => ast
  }).last
it should s"be able to verify multiple programs with caching disabled and retrieve results" in {
  val jobIds = files.map(file => (file, core.verify(file, silicon_without_caching, getAstByFileName(file))))
  val filesAndMessages = jobIds map { case (f, id) => (f, ViperCoreServerUtils.getMessagesFuture(core, id)) }
  val resultFutures = filesAndMessages map { case (f, fut) => fut.map(msgs => {
    println(s"future completed for $f")
    msgs.last match {
      case _: OverallSuccessMessage => assert(f != ver_error_file)
      case _: OverallFailureMessage => assert(f == ver_error_file)
      case msg => fail(s"unexpected message: $msg")
    }
  })}
  Future.sequence(resultFutures).map(results => assert(results.length == 3))
}
ArquintL commented 3 years ago

@aterga I've merged your latest changes into this branch. Except the obvious addition of the VerificationExecutionContext that provides an actor system and execution context, I've changed AstWorker, VerificationWorker, MessageStreamingTask, and MessageReportingTask to no longer inherit from Thread. I find it more natural that these concepts inherit from Callable[T] and return a result of type T. They provide a FutureTask that can be submitted to the thread pool and still have the artifact future. Also different from your changes is the VerificationWorker that no longer uses type parameter AST but Unit as it does not provide an artifact. Imho these changes make sense to me but if you disagree I'm curious how you'll convince me ;)

In addition, I've migrated all CoreServerTests to their async counterpart. However, you'll see that simultaneously verifying multiple files does not seem to work. I've added corresponding TODOs and restricted the tests to a single file (as this is working). I've tried running it on the master branch and the same issue seems to occur there as well (see my comment above). I think the cause is in Silicon and/or Silver and might even be related to @mschwerhoff's performance issues. I don't know yet whether I'll have time before the end of January to further look into this but would you agree that the next step is to directly reproduce it with Silicon?

Could you please have a look at this PR again?

aterga commented 3 years ago

The summary of your changes sounds good to me.

Also different from your changes is the VerificationWorker that no longer uses type parameter AST but Unit as it does not provide an artifact.

That's fine, I did not attach any special meaning to the VerificationWorker's AST artifact. FYI: Akka also provides Done s.t. one can return e.g. Future[Done] instead of Future[Unit] which, in some cases, makes the intention of the code clearer.

I've tried running it on the master branch and the same issue seems to occur there as well (see my comment above). I think the cause is in Silicon and/or Silver and might even be related to @mschwerhoff's performance issues. I don't know yet whether I'll have time before the end of January to further look into this but would you agree that the next step is to directly reproduce it with Silicon?

Sounds reasonable!

ArquintL commented 3 years ago

An update on the failing test cases:

fpoli commented 3 years ago

I think time will be better spent on debugging AST rewriting and figuring out why it does not terminate after the paper deadline.

If you modify the AST while iterating over its nodes, then this commit changes the overall behavior and might be the cause of the failing tests. PR https://github.com/viperproject/silver/pull/493 just improves the performance and does not change this behavior. (I suggest to add a test case with simultaneous parsing in Silver, if possible.)

fpoli commented 3 years ago

I think time will be better spent on debugging AST rewriting and figuring out why it does not terminate after the paper deadline.

If you modify the AST while iterating over its nodes, then this commit changes the overall behavior and might be the cause of the failing tests. PR viperproject/silver#493 just improves the performance and does not change this behavior. (I suggest to add a test case with simultaneous parsing in Silver, if possible.)

I updated the PR https://github.com/viperproject/silver/pull/493 to restore the old behavior. So, it might fix bugs.