Cancellation of Messages

[coot]

Protocol Message Cancellation Design

Egress

1. The egress queue can be a list of lazy ByteString, each one
   corresponding to a single send call (e.g. an encoding of a single message).

2. MuxSDU gets a new field generation :: Word32. It is added to inform the
   remote end when a cancellation happened.

3. When cancelling a message, we'd remove the last enqueued ByteString (especially if
   it was partially consumed/sent), and increment the generation field. When the next MuxSDU is sent, the receiver will need to restart its incremental parser.

Ingress

1. We store the last seen generation (initialised at 0).
2. When reading a MuxSDU from a bearer, we return the bytstring blob together
   with a boolean flag:

   data Restarted =
       -- stream was cancelled, restarted with new message
       Restarted
     | -- stream continues
       Continued

   A boolean flag should be enough, since there could be one partially sent message which is aborted.

Driver

On the driver side, whenever Restarted is received, we return from
runDecodeStep with the received bytes, and restart the incremental decoding, feeding it with the received bytes.

TypedProtocols

We would need a new TypedProtocols API which allows us to cancel previous
message and go back one step.

The current Peer type doesn't allow us to implement Cancel, since we don't
store previous states. Once we Yield/PipelinedYield a message, we move the protocol
forward.

The branch contains a more explicit pipelining scheme,
where at the type level we remember a list of pipelined transitions, e.g.

pattern YieldPipelined
  :: forall ps st q m stm a.
     ()
  => forall st' st''.
     ( StateTokenI st
     , StateTokenI st'
     , StateAgency st ~ ClientAgency
     )
  => Message ps st st'
  -- ^ pipelined message
  -> Client ps Pipelined (q |> Tr st' st'') st'' m stm a
  -- ^ continuation
  -> Client ps Pipelined  q                 st   m stm a

Note: ignore the stm parameter, the branch contains more features than we would need...

When we pipeline Message ps st st', the continuation state is q |> Tr st' st''. From this alone, we cannot restore the state to Client ps Pipelined q st m stm a, but if we also store st in the Tr type constructor, we
could (I have not assessed the consequences of such a change). This would allow us to cancel requests that were pipelined, but not
pipelined requests, but not ordinary ones. Maybe this is enough. A more direct approach could also be possible. However, the challenge is how many previous states we need to remember; tying this to the pipelining depth seems like a reasonable compromise.
Here is how YieldPipelined and CancelledPipelinedYield could look:

pattern YieldPipelined
  :: forall ps st q m stm a.
     ()
  => forall st' st''.
     ( StateTokenI st
     , StateTokenI st'
     , StateAgency st ~ ClientAgency
     )
  => Message ps st st'
  -- ^ pipelined message
  -> Client ps Pipelined (q |> Tr st st' st'') st'' m stm a
  -- ^ continuation
  -> Client ps Pipelined  q                    st   m stm a

pattern CancelPipelinedYield
  :: forall ps st q m stm a
     ()
  => Client ps (Pipelined  q                    st   m stm a -- ^ continuation for a successful cancellation
  -> Client ps (Pipelined (q |> Tr st st' st'') st'' m stm a -- ^ continuation for an unsuccessful cancellation
  -> Client ps (Pipelined (q |> Tr st st' st'') st'' m stm a

[nfrisby]

since there could be one partially sent message which is aborted.

I'm not certain we need to bring in any additional complexity for the sake of cancelling a message that has been partially sent to the mux/bearer. It's seems plausible that we can instead mitigate the associated risks by bounding the size of message that are sent (message size is something both parties are very much aware before anything is even requested in all of our data-intensive mini protocols)

[nfrisby]

For the specific motivating use case I have in mind---ie LeiosFetch---we do not need the cancellation to alter the st state of the mini protocol. A message MsgLeiosBlockTxs would be replaced with an alternative (and nullary) message MsgLeiosBlockTxs_Skipped that causes the exact same st to st' transition as the replaced message. And the (nullary) message MsgCancel (or equivalent) would incur no transition st-to-st---it's entirely optional and we do not need to receive any reply/acknowledgement from it.

[coot]

The only advantage of this design (it could be mixed with the message rewriting you propose, e.g. enqueued message rewriting), is that it allows to cancel a message that is half sent. For a 12MB block this might be useful.

[nfrisby]

The mitigation we discussed the other day was to never send a single atomic request for 12 MB. But instead send, say, 24 requests of 500 kB each. Increasing the request count on that order seems fine, because of pipelining.

Edit: which is a more concrete version of what I wrote here #5347 (comment)

[nfrisby]

As a result of those two observations, I don't feel particularly well-positioned to comment further on this design. If I've understood it correctly so far, it's more general than the only use-case I can afford to give much thought to right now :)