[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Approaching repeated assignment in PlusCal



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

On 10 Dec 2020, at 01:12, Finn Hackett <fhackett.py@xxxxxxxxx> wrote:

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


--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJs285kRCQAH6JRsNGk5%3DtSOd%3D%3DhcxqWELz1czii66CNgYPNZQ%40mail.gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7AD6BCF6-67D1-4616-BD71-4F75CEB12C82%40gmail.com.