Virtualizing continuations (extended version)

Abstract

Effect handlers and multishot continuations are powerful abstractions for managing control flow; together, they offer concise and modular ways to express and handle nondeterminism, randomness, and more. However, implementing multishot continuations in the presence of stack-allocated lexical resources - lexical effect handlers in particular - is challenging, since stack copying invalidates references to these resources.

We present a novel implementation strategy for lexical effect handlers that fully supports multishot continuations. The key idea is to virtualize the stack space used by continuations. Each stack-allocated handler instances is assigned a virtual address, and all effect invocations through these virtual addresses are mediated by an address translation mechanism. A software-based memory management unit in the runtime system performs these translations efficiently, exploiting the lexical scoping discipline of effect handlers.

We capture the essence of our approach via a new operational semantics for lexical effect handlers and prove it correct with respect to the standard semantics. We also implement it in a compiler and runtime system. Compared to prior languages with lexical effect handlers, our implementation increases expressivity by fully supporting multishot continuations - and, as a happy consequence, unlocks significant performance gains by enabling parallel execution of multishot continuations.