Approaching repeated assignment in PlusCal

[Finn Hackett]

Hello,

I'm working on PGo (link: https://github.com/UBC-NSS/pgo), a tool that, among other things, does some macro-like expansion over PlusCal.

I'd like to discuss some tricky edge cases we're running into, namely: specifications which are written as-if multiple assignments happen to the same variable within the same action, in PlusCal. I am aware that PlusCal assignments correspond to TLA+ primed constraints, and therefore that under the PlusCal translation it really makes no sense to actually reassign the same variable in the same action, in any literal sense.

The trouble is that there are situations where code that has that kind of effect needs to be written, and it would be convenient if it could be generated in a way that works, like PlusCal itself, via macro expansion.

Consider some example critical sections, assuming a single-process specification, with a state variable x that is some integer.

section1:
x := x + 1;
x := x + 1;

Clearly, a human would just rewrite the body to say "x := x + 2" and be done.

Mechanically, this can also be handled by inserting a with:

section1:
with (x0 = x + 1) {
  x := x0 + 1;
}

This works for many simpler cases, but becomes troublesome when certain types of control flow become involved:

section2:
if (x = 2) {
  x := x + 1;
}
x := x + 1;

Here, we can't bind any x0 locally that "fixes" the situation, because there is no syntactically general way to bind something inside a branch that is also visible outside that branch. The best we can do syntactically is to perform a little inlining, duplicating any statements after the if:

section2:
if (x = 2) {
  with (x0 = x + 1) {
    x := x0 + 1;
  }
} else {
  x := x + 1;
}

If we want to avoid code duplication, the only other way we can think of is to add a dummy state variable, also called x0 (this is similar to what PGo currently generates):

section2:
if (x = 2) {
  x0 := x + 1;
} else {
  x0 := x;
}
x := x0 + 1;

This has a significant detrimental effect on state space in practice, though, so it is not a very good approach.

My question, then: can anyone think of better (automatable) ways to simulate multiple intra-action assignments to the same variable? Would there be a TLC/toolbox feature that could help with this kind of thing? For instance, in the dummy state variable version, it would make a big difference if we had a way to selectively drop some state variable from the state space, preventing space blow-up.

Any thoughts or comments are appreciated,

A. Finn Hackett

[Srikumar Subramanian]

(Newbie here so I may be wrong)

To me,, the following looks like a specification error -

    section1:
        x := x + 1;
        x := x + 1;

This is (I think) when the mental model of "assignment"" for "state update" gets shaky. "x := x + 1" is really saying "x' = x + 1" in TLA+. So Saying it twice, would be redundant if you want to treat them as being made atomically. So you're really saying "x1' = x + 1 /\ x' = x1' + 1" in TLA+ notation. I suppose then you want to change the mental model in your PlusCal generator ...which I'm not sure is a good idea as it moves away from thinking about it as "specification" versus "program". (I guess more experienced folks ought to comment on that)

However, if you do want to do that atomically, I don't see a way out of introducing more temporary state variables to handle this. You will have to pretty much treat every "assignment" as introducing a new variable, generate update expressions for each of them and finally update the original state. Meaning you need to treat "x := x + 1; x := x + 1; .. <n times>"  as " x1' = x + 1 /\ x2' = x1' + 1 /\ ... <n times> /\ x' = xn' ".

-Srikumar

[Stephan Merz]

I'd approach the problem in two steps: first make sure that all sub-blocks of statements assign to the same (versions of) variables. In your example: transform

section2:
if (x = 2) {
  x := x + 1;
}
x := x + 1;

into

section2:

if (x = 2) {
  x := x + 1;
}

else {

  x := x;

}
x := x + 1;

In a second step, devise an approach to translation that works for such "balanced" input. For example, this could yield

with (x0 = IF x=2 THEN x+1 ELSE x) {

   with (x1 = x0 + 1) {

      x := x1;

   }

}

Clearly, there will be tricky cases such as when there is involved control structure that need careful thinking. Perhaps some techniques used for single static assignment transformations used in compilers could be relevant here.

My 2 cents,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJs285kRCQAH6JRsNGk5%3DtSOd%3D%3DhcxqWELz1czii66CNgYPNZQ%40mail.gmail.com.

[Finn Hackett]

Thanks for the note Hillel. That's interesting, as I had previously skipped that section of the TLA+ book thinking it was about something else.

Apparently I was the only one to receive your comment, so hopefully this pushes it back into the publicly visible responses.

Thanks to the others for your thoughts as well.

-Finn

On Wed, Dec 9, 2020 at 5:45 PM Hillel Wayne <hwa...@gmail.com> wrote:

On 12/9/2020 6:12 PM, Finn Hackett wrote:

My question, then: can anyone think of better (automatable) ways to simulate multiple intra-action assignments to the same variable? Would there be a TLC/toolbox feature that could help with this kind of thing? For instance, in the dummy state variable version, it would make a big difference if we had a way to selectively drop some state variable from the state space, preventing space blow-up.

I believe you can do this by passing a custom VIEW into TLC. The model checker will only consider states distinct if they have different VIEWs. This use case is covered in pages 243-244 of Specifying Systems.

H

[Markus Kuppe]

On 10.12.20 09:30, Finn Hackett wrote:
> I believe you can do this by passing a custom VIEW into TLC. The model
> checker will only consider states distinct if they have differentVIEWs.

> This use case is covered in pages 243-244 of /Specifying Systems./


Another angel on (view) symmetry can be found in
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-30.pdf
page 38ff.

Markus