A Separation Logic for Effect Handlers - Archive ouverte HAL Access content directly
Journal Articles Proceedings of the ACM on Programming Languages Year : 2021

A Separation Logic for Effect Handlers

(1) , (1)
1

Abstract

User-defined effects and effect handlers are advertised and advocated as a relatively easy-to-understand and modular approach to delimited control. They offer the ability of suspending and resuming a computation and allow information to be transmitted both ways between the computation, which requests a certain service, and the handler, which provides this service. Yet, a key question remains, to this day, largely unanswered: how does one modularly specify and verify programs in the presence of both user-defined effect handlers and primitive effects, such as heap-allocated mutable state? We answer this question by presenting a Separation Logic with built-in support for effect handlers, both shallow and deep. The specification of a program fragment includes a protocol that describes the effects that the program may perform as well as the replies that it can expect to receive. The logic allows local reasoning via a frame rule and a bind rule. It is based on Iris and inherits all of its advanced features, including support for higher-order functions, user-defined ghost state, and invariants. We illustrate its power via several case studies, including (1) a generic formulation of control inversion, which turns a producer that "pushes" elements towards a consumer into a producer from which one can "pull" elements on demand, and (2) a simple system for cooperative concurrency, where several threads execute concurrently, can spawn new threads, and communicate via promises.
Fichier principal
Vignette du fichier
de-vilhena-pottier-sleh.pdf (722.49 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive

Dates and versions

hal-03049514 , version 1 (10-12-2020)

Identifiers

Cite

Paulo Emílio de Vilhena, François Pottier. A Separation Logic for Effect Handlers. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), ⟨10.1145/3434314⟩. ⟨hal-03049514⟩
61 View
107 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More