(This suspected issue was noticed by @clef-men; he convinced me that this looks credible and we wrote the proposed fix together.)
The Task implementation seems to be slightly wasteful in that, if we understand correctly, it may install its effect handler twice. This occurs in the following scenario:
call Task.run, under which you
create a promise with async
await this promise
when await gives control back, two step handlers are on the stack
Two handlers are on the stack because:
when the current task is paused by await, the continuation k contains the deep handler of the surrounding step call:
let cont v (k, c) = Multi_channel.send c (Work (fun _ -> continue k v))
invoking this Work function will thus reinstate the surrounding deep handler.
when this continuation is received by another worker, step is called again, installing a second handler
let rec worker task_chan =
match Multi_channel.recv task_chan with
| Quit -> Multi_channel.clear_local_state task_chan
| Work f -> step f (); worker task_chan
At this point, if we understand correctly, there are two step handlers on the call stack. Note that this does not grow to an unbounded number of nested handlers: on the next Wait effect, the inner handler either continues immediately (still 2 handlers) or pushes the current continuation to a Pending queue and returns, popping the two handlers. Once this continuation is invoked again under step, we are back to 2 handlers.
Note that in some case the current implementation does need the step call in worker, because the function argument of Work f does not systematically include a handler:
let async pool f =
let pd = get_pool_data pool in
let p = Atomic.make (Pending []) in
Multi_channel.send pd.task_chan (Work (fun _ -> do_task f p));
p
Explanation of our proposed fix:
This PR proposes to fix the issue by enforcing the invariant that the Work function always includes its own handler for Task effects: for the Work functions that use continue and discontinue there is nothing to do, for the Work function of async we call step at this point.
Another approach would be to use a shallow handler, and use step in the same way as currently (around each Work function), but this may be slightly slower -- we would be exactly encoding a deep handler using a shallow handler. (The current code reads like the authors had the shallow-handler semantics in mind.)
Explanation of the suspected issue:
(This suspected issue was noticed by @clef-men; he convinced me that this looks credible and we wrote the proposed fix together.)
The Task implementation seems to be slightly wasteful in that, if we understand correctly, it may install its effect handler twice. This occurs in the following scenario:
asyncawaitthis promiseawaitgives control back, twostephandlers are on the stackTwo handlers are on the stack because:
when the current task is paused by
await, the continuationkcontains the deep handler of the surroundingstepcall:invoking this Work function will thus reinstate the surrounding deep handler.
when this continuation is received by another worker,
stepis called again, installing a second handlerAt this point, if we understand correctly, there are two
stephandlers on the call stack. Note that this does not grow to an unbounded number of nested handlers: on the next Wait effect, the inner handler either continues immediately (still 2 handlers) or pushes the current continuation to a Pending queue and returns, popping the two handlers. Once this continuation is invoked again understep, we are back to 2 handlers.Note that in some case the current implementation does need the
stepcall inworker, because the function argument ofWork fdoes not systematically include a handler:Explanation of our proposed fix:
This PR proposes to fix the issue by enforcing the invariant that the Work function always includes its own handler for Task effects: for the Work functions that use
continueanddiscontinuethere is nothing to do, for the Work function ofasyncwe callstepat this point.Another approach would be to use a shallow handler, and use
stepin the same way as currently (around each Work function), but this may be slightly slower -- we would be exactly encoding a deep handler using a shallow handler. (The current code reads like the authors had the shallow-handler semantics in mind.)Co-authored-by: Clement Allain clement.allain@inria.fr