External parallelization of Silicon

Question

External parallelization of Silicon

pieter-bos opened this issue 2 years ago · 5 comments

Hi! Is it supported, or should it be supported, to run multiple instances of Silicon in parallel, within the same process/JVM? What I tried to do was make multiple instances of viper.silicon.Silicon in different threads, but this seems to break in various ways. As an example, the instances race to set viper.silicon.verifier.Verifier._program, but it seemed there were more kinds of error (I did not investigate very deeply).

Answer 1 · 2022-11-15T13:51:19.000Z

It should work in the current master branch of Silicon, not in the last release. Pieter ***@***.***> schrieb am Di., 15. Nov. 2022, 14:46:

…

Hi! Is it supported, or should it be supported, to run multiple instances of Silicon in parallel, within the same process/JVM? What I tried to do was make multiple instances of viper.silicon.Silicon in different threads, but this seems to break in various ways. As an example, the instances race to set viper.silicon.verifier.Verifier._program, but it seemed there were more kinds of error (I did not investigate very deeply). — Reply to this email directly, view it on GitHub <#660>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALL2EM6QDU2D6EPQKWVYLLWIOH35ANCNFSM6AAAAAASA6VPVM> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

Answer 2 · 2022-11-16T12:58:47.000Z

Cool! That improves things a lot. Still a couple errors I noticed though:

I got this crash (which I can't stably reproduce). It seems logically impossible to me because the match/PartialFunction from GenericTriggerGenerator.scala:176-183 is defended by Strategy.scala:1116. I'll let you know if I get a reproducible example, otherwise maybe you see it immediately anyway.

scala.MatchError: l + k (of class viper.silver.ast.Add)
	at scala.PartialFunction$$anon$1.apply(PartialFunction.scala:344)
	at scala.PartialFunction$$anon$1.apply(PartialFunction.scala:342)
	at viper.silver.ast.utility.GenericTriggerGenerator$$anonfun$$nestedInanonfun$getFunctionAppsContaining$2$1.applyOrElse(GenericTriggerGenerator.scala:176)
	at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
	at viper.silver.ast.utility.rewriter.AddArtificialContext.apply(Strategy.scala:228)
	at viper.silver.ast.utility.rewriter.AddArtificialContext.apply(Strategy.scala:226)
	at viper.silver.ast.utility.rewriter.Rule.execute(Strategy.scala:1117)
	at viper.silver.ast.utility.rewriter.Strategy.rewriteInnermost(Strategy.scala:534)
	at viper.silver.ast.utility.rewriter.Strategy.selectStrat(Strategy.scala:356)
	at viper.silver.ast.utility.rewriter.Strategy.execute(Strategy.scala:371)
	at viper.silver.ast.Node.transform(Ast.scala:126)
        (...)

We use my fork of silicon that includes #622, which makes the symbolic execution logger thread safe up to the internal parallelization of silicon, but contains global state, and is thus not externally parallelizable. I'd be happy to contribute a fix for that, since I've poked it last anyway :)

Answer 3 · 2022-11-16T13:10:57.000Z

Yeah, I found the first issue, there's mutable state in GenericTriggerGenerator that I overlooked. Will fix that later today. Thanks!

Answer 4 · 2022-11-22T09:45:51.000Z

The problem in the trigger generator should be fixed now.

Answer 5 · 2022-11-22T10:02:43.000Z

I don't see further issues in silicon, so afaic this can be closed by #622