P
P copied to clipboard
p-org
`GuaranteedWithDrawProgress` in Tutorial 1 is inaccurate/misdocumented
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).
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?
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.
@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?
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.
