Questions about maintaining solver's context when adding parallelism in silicon

[fanweneddie]

Hi @marcoeilers,

I am interested in the parallelization of branching in silicon, and I am a little confused about the mechanism that you maintain the solver's context before the parallel branch is started.

For example, suppose on the branching point, the current verifier v originally has declarations and some assumptions (i.e., pathConditions) on {t1, t2}, and the new verifier v0 for else branch originally has declarations and some assumptions on {t1, t3}. In this case, v0 will further declare t2 and hold the same assumptions as v.

First of all, I am wondering if extra declarations (e.g., t3 in v0) don't affect further execution. I think they won't because the extra declarations will not be used in further execution.

• The extra declarations of variables out of the current method will not be used. I think all variables in solver are distinct (e.g., x@4@02), so the local variable with the same name (e.g., x) from other methods will not be used in current method. (By the way, there is no global variable in Viper, right?)
• The extra declarations of variables in the same method will not be used, because further execution will not be in the scope that variable (otherwise, if t3 is used in else branch, it should be declared before in v or should be declared later in v0, and both contradict the fact that t3 is in v0 - v).

Second, I am wondering if it is unnecessary to resume the pathConditions of v0 to its original one. I think for v0, if it is later used in branching, its path conditions will be overwritten anyway, so we don't need to resume; If it is later used in verifying other methods in DefaultMainVerifier.verify, then the modified declarations and pathConditions will not be used in the new method (since all variables have distinct name), so it is okay to keep them.

It would be really appreciated if you could help answer or explain them. I am sorry my description is long and tedious, because I haven't found a counterexample, haha.

[marcoeilers]

Hi!

Regarding the first point:
In the Z3 mode we're using it's actually impossible to un-declare variables, so once they have been declared on some verifier, they'll have to stick around.
So you're right, when we switch to some v0 to verify an else-branch, it will usually have some additional declarations like t3 from whatever method or branch it worked on previously, but since all assumptions from those were dropped, there are no assumptions constraining those variables at all. Viper does not have global variables, but even if it did, we would drop all assumptions about them before verifying an else-branch on a new verifier.
Additionally, as you wrote, any fresh variables generated later will always have a different name because there is a unique postfix in each variable that identifies the verifier instance it was originally declared in, and for each verifier, we make sure the names excluding that postfix are always unique. Any assumptions added later might reference those new variables, but never the old ones that shouldn't exist in the current context.
So the additional variables are there but aren't constrained in any way and could thus hold any value and can never affect whether the current SMT problem is satisfiable or not. They might result in some performance overhead since Z3 presumably still has to remember they exist, but I think that overhead is not big, since Z3 doesn't seem to try to assign any values to variables with no constraints (they don't show up in the model).

Regarding the second point, I don't think it's necessary to reset the path conditions of the new verifier v0 afterwards, for the reasons you mentioned, and we don't do that as far as I can see.

[fanweneddie]

Oh, I see. Thank you so much for your quick and detailed answer!

[marcoeilers]

Let me know if I misunderstood anything or you have any further questions. In particular regarding the last point, I don't remember us resetting path conditions of the new verifier and I gave the code a quick look to see if I'm misremembering things, but I could absolutely be wrong about that.