Modeling non-determinism and the MP pattern

gistfile1.txt

The Message Passing pattern (MP pattern) is shown below in the snippet below. P0 and P1 are 2 CPUs executing some code. The pattern has P0 store a message to `buf` and then signal to consumers like P1 that the message is available -- by doing a store to `flag`. Without memory barriers between P0's stores, the stores can appear to be out of order to P1, thus breaking the pattern. The condition "r1 == 0 and r2 == 1" is a failure and show never occur. Only after flag is updated, should we read the buf ("message").

```
        int buf = 0, flag = 0;

        P0()
        {
                WRITE_ONCE(buf, 1);
                WRITE_ONCE(flag, 1);
        }

        P1()
        {
                int r1;
                int r2 = 0;

                r1 = READ_ONCE(flag);
                if (r1)
                        r2 = READ_ONCE(buf);
        }
```

Here is a simple program in PlusCal to model the "Message passing" access pattern and check whether if the failure scenario ever occurs (r1 == 0 and r2 == 1). In PlusCal, we can model the out-of-order stores to buf and flag using the either/or operator. This makes PlusCal evaluate both scenarios of stores during model checking. The technique used for modeling this non-determinism is similar to how it is done in Promela/Spin using an "if block" (Refer to Paul McKenney's perfbook for details on that).

```
EXTENDS Integers, TLC
(*--algorithm mp_pattern
variables
    buf = 0,
    flag = 0;

process Writer = 1
variables
    begin
e0:
       either
e1:        buf := 1;
e2:        flag := 1;
        or
e3:        flag := 1;
e4:        buf := 1;
        end either;
end process;

process Reader = 2
variables
    r1 = 0,
    r2 = 0;  
    begin
e5:     r1 := flag;
e6:     if r1 = 1 then
e7:         r2 := buf;
        end if;
e8:     assert r1 = 0 \/ r2 = 1;
end process;

end algorithm;*)
```

Sure enough, the `assert r1 = 0 \/ r2 = 1;`  fires when the PlusCal program is run through the TLC model checker.

I do find this clunky, I wish I could just do something like:
```
non_deterministic {
        buf := 1;
        flag := 1;
}
```
And then, PlusCal should evaluate both store orders. In fact, if I have more than 2 stores, then it can get crazy pretty quickly without such a construct. I should try to hack the PlusCal sources soon if I get time, to do exactly this. Thankfully it is open source software.

Not perfect, but gets you closer:

while {buf, flag} /= 1 do
  either
    await flag /= 1;
    flag := 1;
  or
   await buf /= 1;
   buf := 1;
 end either;
end while;