Spec does not cover race conditions for call cancelation

[ecorm]

The spec does not cover what happens in the following scenarios:

A) The callee has already returned a YIELD before it receives an INTERRUPT message B) The dealer has already received a YIELD when it receives a CANCEL message C) The dealer has already returned a RESULT when it receives a CANCEL message

In addition, I think it should be stated that a callee is not guaranteed to receive an ERROR.Error := wamp.error.canceled response after sending a CANCEL message. After sending an ERROR it's possible for the callee to receive either:

1. an ERROR.Error := wamp.error.canceled message associated with the cancellation,
2. a RESULT message associated with the original call, or,
3. an ERROR message associated with the original call, not the cancelation

[estan]

I agree with all of this. This is what I think, off hand, would be most intuitive:

• The callee must ignore the INTERRUPT.
• The dealer may send the RESULT, or the CANCEL, at its discretion.
• The dealer must ignore the CANCEL.

And it should then be made clear that this is what callers can rely on, nothing more. And as a result, and just as you mention, it should be made clear that callers are not guaranteed to get wamp.error.canceled after sending a CANCEL.

In general I think it should be made more clear that cancellations are cancellation requests, which may or may not be fulfilled due to the scenarios you describe.

[oberstet]

awesome! I guess I agree with both of you @ecorm and @estan here. we should include above material in the spec (https://github.com/tavendo/WAMP/blob/master/spec/advanced.md#canceling-calls)

one question though:

The dealer may send the RESULT, or the CANCEL, at its discretion.

Probably good idea to leave that open to an implementation, but why exactly again?

[ecorm]

one question though:

The dealer may send the RESULT, or the CANCEL, at its discretion.

Probably good idea to leave that open to an implementation, but why exactly again?

I added labels (A, B, C) to my scenarios in my original post in order to facilitate discussion.

In scenario B, the dealer has already received a YIELD message from the callee. But before it has a chance to send a RESULT message back to the caller, it suddenly receives a CANCEL message from the caller. So the dealer must now ask himself:

i) "Should I forward the YIELD result I just received to the caller and ignore the CANCEL request?", or, ii) "Should I discard the YIELD result and send an ERROR.Error := wamp.error.canceled message back to the caller?"

I agree with @estan that it's reasonable for the dealer to do either i) or ii) in that scenario. If clients are aware that CANCEL messages are merely requests that may or may not be fulfilled (as estan nicely put it), then they should be able to handle behavior (i) or (ii) without any issue.

[ecorm]

I agree with all of this. This is what I think, off hand, would be most intuitive:

• (A) The callee must ignore the INTERRUPT.
• (B) The dealer may send the RESULT, or the CANCEL, at its discretion.
• (C) The dealer must ignore the CANCEL.

I agree with that behavior, @estan.

[KSDaemon]

I think we have mostly described this in #140. Aslo #141 is related

[gammazero]

I agree with @estan. May want to reword B slightly to change CANCEL to ERROR (wamp.error.canceled).

• A) The callee has already returned a YIELD before it receives an INTERRUPT message
  • The callee must ignore the INTERRUPT.
• B) The dealer has already received a YIELD when it receives a CANCEL message
  • The dealer may return the RESULT, or ERROR (wamp.error.canceled), at its discretion.
• C) The dealer has already returned a RESULT when it receives a CANCEL message
  • The dealer must ignore the CANCEL

To state why B is "at dealer's discretion": Dealer implementations will generally handle B by processing whatever message is received first. If both are being concurrently processed by dealer it may be indeterminate which is processed first, so this must be left open "to dealer's discretion".

[oberstet]

My take:

A): The callee might have already deleted the outstanding invocation from its internal map, and hence the INTERRUPT is referring to a non-existing invocation => ERROR

B): The dealer cannot INTERRUPT, since it already received a YIELD, and hence must return a CALL_RESULT, and hence the CANCEL => ERROR

C): The dealer will have already deleted the outstanding call from its internal map, and hence the CANCEL is referring to a non-existing call => ERROR

[gammazero]

@oberstet If the ERROR your are describing above is wamp.error.canceled, then we are in agreement. Is that what you mean, or some other error URI?

[KSDaemon]

Okay! And another one approach: A) The callee MUST ignore INTERRUPT message if it has already sent final YIELD message. B) When dealer that has received final YIELD message from callee that is not yet sent to caller receives a CANCEL message, it MUST drop YIELD message and send ERROR (wamp.error.canceled) message instead. I don't like OR words in SPEC, and think we should specify more explicitly if it is possible. Caller sending CANCEL message is not interested in result, so why we should send it. Router implementations may interpret putting a RESULT message into caller queue as it was allready sent, and it is not possible to remove it from queue. C) When dealer receives a CANCEL message after it sent a final RESULT message it must ignore CANCEL

So my point is mostly the same as Andrews @gammazero. I just wanted to draw your attention, so we did not forget to mention about progressive calls when updating SPEC.

[oberstet]

Oh, yes, progressive call results. good point. so at least me, I really have to go over all of above again. there are quite some cases to consider here. eg while we are on it, we might specify behavior regarding a future progressive calls as well.

I am wondering: a WAMP RPC scenario is like 3 communicating state machines (caller, dealer, callee), with communication links that can have dropouts or delays. Is there a way to systematically analyze the timing corner cases that can occur in the former protocol interactions?

Besides "order of messages", there is the whole other area of "no reply for infinite time ..." scenarios, where timeouts are required for everything expecting a reply. And as soon as we have timeout, then a message that wasn't received in time might still arrive later.

[estan]

@oberstet It reminds me a little of temporal logic, and perhaps CSP that I learned about in logic class back in school, and quickly forgot about :P

But I'm sure there's tooling for (semi-)automatic formal verification of communicating state machines, I just don't know of any off hand. I guess the challenge will be in getting your machines on the form required by such a tool, and expressing the statements you want proved.

[oberstet]

@estan thanks for your thoughts! Interesting .. CSPs .. temporal logic. Clearly, more of a research topic. Anyone wants to aim for PhD in formal WAMP protocol verification? =)