Erlang 2025 – Proceedings

24th ACM SIGPLAN International Workshop on Erlang (Erlang 2025)

Frontmatter

Keynote

PyErlang: A Stepping Stone towards Behaviour-Oriented Concurrency in Python (Keynote)
Tobias Wrigstad
(Uppsala University, Sweden)
Python was designed in an era of mostly single-core machines, where concurrency was typically not parallel, and Dennard scaling made us rely on ever-faster single core CPUs coming onto the market every year. In this context, Python's Global Interpreter Lock (GIL)-based design is easily motivated: only one thread may interpret bytecodes at a time in a Python program. This buys a lot of simplicity for your runtime, but it also means that throwing more cores at a Python program does not make it go faster.
Python 3.12 introduced the ability to run multiple Python interpreters in a single OS process, each with its own GIL. Each sub-interpreter runs in isolation from the other sub-interpreters and isolation is enforced by using a serialisation protocol to transfer data from one sub-interpreter to another. Every sub-interpreter has its own private heap, managed by a combination of reference counting and tracing GC dealing with cyclic data. This setup should feel familar to Erlang developers.
Cheeseman et al’s Behaviour-oriented Concurrency (BoC) is a promising technique for expressing concurrency in imperative programming, and delivers guarantees of data-race freedom and dead-lock freedom. As part of a multi-year project for adding BoC to Python, we have recently arrived at an intermediate step that we lovingly refer to as PyErlang. PyErlang enhances the sub-interpreters model with an ability to share immutable data by reference across interpreters, without making one process dependent on GC in another.
This talk is about the core of PyErlang: how to retro-fit immutability onto a mature language around a culture that embraces reflection and monkey-patching. I will discuss challenges at both the language-level and the implementation-level, and how we handle cyclic immutable garbage without tracing GC.

@InProceedings{Erlang25p1, author = {Tobias Wrigstad}, title = {PyErlang: A Stepping Stone towards Behaviour-Oriented Concurrency in Python (Keynote)}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {1-1}, doi = {10.1145/3759161.3771262}, year = {2025}, } Publisher's Version

Papers

Moving Objects and Behavior Safely in Ad Hoc Networks
Juan Camilo Bonet, Mateo Sanabria Ardila, and Nicolás Cardozo
(Universidad de Los Andes, Colombia)
In distributed computing systems, function entities live on a single machine or node, while data is shared between nodes in order to carry out computation. Such computation model gives rise to undesirable system characteristics, such as increased network load and data vulnerabilities, both caused by sharing large amounts of information between nodes. The introduction of fog computing architectures, mitigates these problems by moving part of the computation to edge devices. To further tackle these problems, this work explores the use of the call-by-move parameter passing semantics to enable function mobility between many nodes, effectively reducing network load and avoiding unnecessary information sharing. To build the new parameter passing semantics, we use Elixir’s metaprogramming capabilities, introducing new language constructs and functions. Furthermore, we accompany the implementation by a formal specification of the system using Athena. In order to show the usability of this approach, we implement an exemplar application that demonstrates reduced network load and a reduced amount of shared data, when computation, and hence communication, load increases for each of the nodes in the network.

@InProceedings{Erlang25p2, author = {Juan Camilo Bonet and Mateo Sanabria Ardila and Nicolás Cardozo}, title = {Moving Objects and Behavior Safely in Ad Hoc Networks}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {2-13}, doi = {10.1145/3759161.3763044}, year = {2025}, } Publisher's Version

Mechanised Proofs of Atom Exhaustion in Erlang
Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, and Gergő Lajos Turán
(Eötvös Loránd University, Hungary)
Static analysis tools aid in developing secure software, but they often produce false positives that undermine developer trust. Formal methods can help validate such findings, provided that the vulnerabilities are precisely formalised. This study presents a formalisation of the atom exhaustion vulnerability within the context of the sequential subset of an existing Core Erlang formal semantics. A sound and complete calculus is proposed to support structured reasoning about the presence of the atom exhaustion vulnerability in Erlang programs. All the results of this paper are implemented in the Coq proof assistant.

@InProceedings{Erlang25p14, author = {Arsenii Fomin and Péter Bereczky and Dániel Horpácsi and Gergő Lajos Turán}, title = {Mechanised Proofs of Atom Exhaustion in Erlang}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {14-25}, doi = {10.1145/3759161.3763045}, year = {2025}, } Publisher's Version

Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, and Simon Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
We present an interpreter for Erlang in Haskell, derived from a formal semantics for Core Erlang mechanised in Coq. The interpreter function is derived from the Coq inductive definitions that make up the semantics by extracting Haskell code from Gallina functions provably equivalent to the inductive definitions, and optimising the result. The semantics is inherently non-deterministic, and it is made deterministic by introducing a scheduler component; we also present a computation graph that shows all the non-deterministic choices that arise during computation. The paper concludes with an evaluation of the work and preliminary performance data.

@InProceedings{Erlang25p26, author = {Gergő Lajos Turán and Arsenii Fomin and Péter Bereczky and Dániel Horpácsi and Simon Thompson}, title = {Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {26-39}, doi = {10.1145/3759161.3763046}, year = {2025}, } Publisher's Version

A Stop-the-World Debugger for Erlang (and the BEAM)
Daniel Gorin, Björn Gustavsson, and Roberto Aloi
(Meta, UK; Ericsson, Sweden; Meta, Sweden)
Erlang and the BEAM are remarkable for their tracing capabilities and the type of troubleshooting this enables on live production systems. At other stages of the development cycle, though, a traditional debugger is arguably more natural and convenient to use. While Erlang/OTP has included a step-debugger (int) since its very first public release, it has generally been regarded as ineffective beyond very simple scenarios. To bridge this gap, we have extended OTP with a new debugging API (available since release 28), and used it to build edb, a novel debugger for Erlang that aims to overcome some of int’s known limitations. In this note we motivate this work, discuss technical challenges and provide a general implementation overview.

@InProceedings{Erlang25p40, author = {Daniel Gorin and Björn Gustavsson and Roberto Aloi}, title = {A Stop-the-World Debugger for Erlang (and the BEAM)}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {40-51}, doi = {10.1145/3759161.3763047}, year = {2025}, } Publisher's Version

Evaluating AtomVM for Fault-Tolerant ESP32-Based Systems
Daniel Ferenczi, Gergely Ruda, and Melinda Tóth
(Eötvös Loránd University, Hungary; evosoft, Hungary)
Components of IoT setups are subject to hardware failures, independently of software quality. These errors can be addressed by introducing hardware-level fault tolerance. This requires additional hardware components and the orchestration of tasks between them.
Erlang and Elixir, when running on BEAM, solve this problem for server-grade computers. However, IoT systems can also contain many microcontrollers that are too limited in resources to host BEAM.
AtomVM is a novel runtime for languages that traditionally run on BEAM. It brings many features of the runtime to embedded devices, including those necessary to monitor the failure of remote nodes and build fault-tolerant systems. As memory and computational power on microcontrollers are scarce, gauging how these features perform is essential.
In this study, we measure the cost of fault tolerance on ESP32-based AtomVM systems by comparing a single-node implementation of a particular setup with that of a fault-tolerant one. This test system handles the reception and processing of radio messages, a typical task for the embedded components of an IoT deployment.
Our measurements should help developers design applications that, while building on Erlang's fault tolerance, fit the limited resources available on microcontrollers.

@InProceedings{Erlang25p52, author = {Daniel Ferenczi and Gergely Ruda and Melinda Tóth}, title = {Evaluating AtomVM for Fault-Tolerant ESP32-Based Systems}, booktitle = {Proc.\ Erlang}, publisher = {ACM}, pages = {52-61}, doi = {10.1145/3759161.3763048}, year = {2025}, } Publisher's Version

proc time: 0.82