GuaranteedWithDrawProgress in Tutorial 1 is inaccurate/misdocumented

[hwayne]

The liveness property is defined as:

GuaranteedWithDrawProgress checks the liveness (or progress) property that all withdraw requests
submitted by the client are eventually responded.

However, the definition

  hot state PendingReqs {
    on eWithDrawResp do (resp: tWithDrawResp) {
      assert resp.rId in pendingWDReqs,
        format ("unexpected rId: {0} received, expected one of {1}", resp.rId, pendingWDReqs);
      pendingWDReqs -= (resp.rId);
      if(sizeof(pendingWDReqs) == 0) // all requests have been responded
        goto NopendingRequests;
    }

Instead checks a stronger property: that eventually all the requests are responded to. If requests come in at the same rate they are resolved, then all withdraw requests are responded to, but the property will still fail.

More formally, the documentation implies it's ∀message: ◇responded, but the actual property checked is ◇(∀message: responded).

[atomgardner]

Instead checks a stronger property: that eventually all the requests are responded to.

@hwayne: Care to elaborate? I only see: [] \A m. m \in Resps -> m \in Reqs. What am I missing?

[hwayne]

We enter the hot state when we add a new pending request and only leave it when sizeof(pendingWDReqs) == 0. Now consider the following sequence of states for pendingWDReqs:

{}
{1}
{1, 2}
{2}
{2, 3}
{3}
{3, 4}
...

At every point, sizeof(pendingWDReqs) > 0, so we never leave the hot state. However, we're still responding to every request.

[atomgardner]

@hwayne: I see now, with this missing piece of context:

the system satisfies a liveness specification if at the end of the execution the monitor is not in a hot state (line 13).

No idea how you'd even check [](\A m. m\in Req -> <> m\in Resp) in general. The behaviours with nice structure (like the eg above) make proofs possible, but otherwise impossible?

[ankushdesai]

In P, the liveness checking is defined for finite executions and for long running infinite execution it depends on the heuristics. Lets take this to discussion.

[nvartolomei]

Can you please expand on the "heuristics"? I'm trying to model a multi-producer-multi-consumer queue and run a test with 3 producers and 1 consumer. The liveness check always fails. It seems that it doesn't keep up with the producer rate which should be fine. This is exact problem OP mentioned but less artificial.

How should I think about this type of problem? I guess I can make the consumer do more work per "clock-cycle" but how I can gain confidence that this is good enough?

[nvartolomei]

This is what I have come up with on the producer side to "throttle" them and let consumer run ahead. Still waiting for a better answer if available.

PS. Is there a better way to make the machine "do nothing" for one clock-cycle?

state Sleep {
    entry {
        if (2 > choose(10)) {
            goto Produce;
        } else {
            send this, eTick, true;
        }
    }

    on eTick do {
        goto Sleep;
    }
}

state Produce { ... }