Understanding cancellation (in eio)

Over in the other thread, @kayceesrk wondered if cancellation could be expressed “minimally” by turning

type 'a resumer = 'a -> unit
effect Suspend : ('a resumer -> unit) -> 'a eff

into

type 'a resumer = 'a -> bool

where false is returned when the task was cancelled.

I find it strange with this API that the producer learns whether cancellation happened or not only after trying to resume the suspension with the result. I would expect an API where the producer checks that the suspension is still active first. But I’m not sure which is more correct.

Sometimes there is a race between a producer producing a resource, and a suspended consumer being cancelled. If the producer commits to giving the resource to the suspender, then the suspender must be resumed for the “transactional” guarantees to hold. I guess the following scenarios could happen:

  1. The producer learns that the suspender was cancelled, but “too late” after it committed: it ignores cancellation information and resumes the suspender anyway; or
  2. The producer needs to be careful to not commit until it learns for sure that the suspender will resume. It may need to explicitly keep the resource around for another consumer if it learns that the supended consumer was cancelled.

(Above I have the “simple” cases of cancellation in mind, that I called “suspending on other computations”. In the “low-level case” of asynchronous operation, a symmetric situation arises. If the suspender decides to cancel the asynchronous operation, but cancellation fails because the operation has in fact been committeed, then the computation must continue by resuming the suspension as if cancellation hadn’t happened.)

Note: I believe that with the ('a -> bool) API we don’t have a choice between (1) and (2) anymore, we have to go with (2).

1 Like