Please note: This PhD defence will take place in DC 3317 and online.

Cong Ma, PhD candidate
David R. Cheriton School of Computer Science

Supervisor: Professor Yizhou Zhang

Effect handlers generalize exception handling to support control-flow patterns including coroutines, cooperative multitasking, and nondeterminism. Recent work advocates for lexically scoped handlers, which restore abstraction safety and enable modular reasoning: a handler is a lexically scoped capability, and an effect can be raised only to a handler whose capability is in scope. However, prior implementations of lexical effect handlers suffer from inefficiencies that could hinder their adoption in practice.

This thesis shows that the static character that makes lexical scoping safe is also what makes it efficient to implement. It develops this insight into three complementary compilation techniques, embodied in our language Lexa; each technique is made precise by a formal model, proven correct, and realized in the Lexa compiler. Direct Lexa identifies each handler with the stack address where it is installed, so a raise jumps directly to its handler, without any search. Zone Lexa extends the address-based strategy to multishot resumptions by virtualizing handler identities through a software memory-management unit. Zero Lexa serves infrequent effects such as exceptions: it avoids the cost of passing down any run-time handler identity, and instead walks the stack using the static handler provenance information when an effect is raised, so effect-free execution pays nothing. A single program can choose among the three techniques per effect, matching each effect’s expected usage.

Together, these techniques demonstrate that lexical effect handlers can be implemented efficiently. Effect handlers can be both safe and fast.

To attend this PhD defence in person, please go to DC 3317. You can also attend virtually on Zoom.