Closed
Description
While running multiple verifier instances in parallel (from a Rust program) I reliably get the following error, which might indicate a data race in the way builtin domains are loaded and type-checked.
java.util.NoSuchElementException: None.get
at scala.None$.get(Option.scala:627)
at scala.None$.get(Option.scala:626)
at viper.silicon.supporters.utils$.loadProgramFromUrl(BuiltinDomainsContributor.scala:198)
at viper.silicon.supporters.BuiltinDomainsContributor.analyze(BuiltinDomainsContributor.scala:59)
at viper.silicon.verifier.DefaultMasterVerifier.$anonfun$analyzeProgramAndEmitPreambleContributions$1(DefaultMasterVerifier.scala:397)
at viper.silicon.verifier.DefaultMasterVerifier.$anonfun$analyzeProgramAndEmitPreambleContributions$1$adapted(DefaultMasterVerifier.scala:396)
at scala.collection.immutable.List.foreach(List.scala:333)
at viper.silicon.verifier.DefaultMasterVerifier.analyzeProgramAndEmitPreambleContributions(DefaultMasterVerifier.scala:396)
at viper.silicon.verifier.DefaultMasterVerifier.verify(DefaultMasterVerifier.scala:177)
at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:245)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:198)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:197)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1130)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:630)
at java.base/java.lang.Thread.run(Thread.java:832)
Metadata
Metadata
Assignees
Labels
No labels