Q24: Summary of meeting on 20.10.2020

[sophiaIC]

Here how I remember the meeting -- please correct me.

[sophiaIC]

1. Sylvan pointed out that the definition of "no deadlocks" as in Q22 is too strong. We agreed on that, but also believe that a proof of lack deadlocks using the strong definition is a useful first step.

[sophiaIC]

2. Theo and Luke reported that the invariant (*) which requires that there are no cycle in mute sets (as in Q16) with priority -1, does indeed hold -- by running the model checker tool.
   We also added a further invariant (**) which says:
   (**) prio[c]=1 --> [ queue[c]!=0 \/ !sch[c] ]
   Using a stronger version of (*) and (**) we can prove that there are no deadlocks -- as outlined in Q22.

[sophiaIC]

3. But we then realised that (**) is not presented by Send nor by Acquire.

[sophiaIC]

4. We then changed the definition of Send and Acquire so that it only bumps the priority of the next receiver (Min(CurrMessage(c))). We hope that this change preserves (**).
   But Theo ran the model as we were speaking, and discovered that this breaks even the weaker form of (*).
   Even worse, we worry that in the new protocol the configuration from Q16 may arise; and this configuration is stuck!

[sophiaIC]

At this point we agree to take a break and continue the discussion on GitHub, and talk again in a week's time. Sean told us that the new proposed invariants coincided with invariants he needed for the Pony backpressure algorithm -- this is encouraging.