Using Functional Reactive Programming to Define Safe Actor Systems
Abstract
Functional Reactive Programming (FRP) is a powerful abstraction for building deterministic concurrent systems. However, some programmers prefer a more imperative approach for certain tasks, and that approach is required to implement some imperative algorithms. The Actor Model provides an abstraction for building concurrent systems in a more imperative way without as much of the chaos typical of traditional shared-memory imperative concurrent programming. While the Actor Model offers more structure than other imperative approaches, it still suffers from nondeterminism due to message-ordering and processing times. That makes actor systems hard to reason about, limiting their effectiveness for critical tasks. We formally define an elegant multi-paradigm unification of event-driven FRP constructs and the Actor Model. Our unification enables an intuitive form of declarative programming that can integrate imperative and declarative code within each other. We use reference and object capabilities to tame imperative features: reference capabilities track aliasing and mutability, and object capabilities track I/O. Notably, in our system expressions with deeply immutable input behave deterministically. Additionally, capabilities provide a boundary to allow nondeterministic code to intermingle safely with deterministic code.
Authors
Nick Webster, Marco Servetto, Michael HomerPublished in
Workshop on Formal Techniques for Java-like Programs (FTfJP), 2022The final copy of this publication is available from the publisher.
Resources
- Author copy (PDF)
- mwh.nz/pdf/ftfjp2022
- this page
- mwh.nz/pubs/ftfjp2022