viperproject/silicon

Weird behavior if WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException

Opened this issue · 0 comments

If WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException for some subset of the worker threads,

  • a stack trace is printed but Silicon does not crash completely
  • for some reason onStart is executed for only two workers max (???)
  • sometimes Silicon hangs forever
  • sometimes it still reports results (unclear if all results or some subset)

Immediate question:
Can a crash like this lead to successful verification even though there should be errors, i.e., is this a potential unsoundness, or is it just weird? And does this change is branch parallelization is on?

Also, does the type of exception matter?