ICFP Workshops 2024
29th ACM SIGPLAN International Conference on Functional Programming (ICFP 2024)
Powered by
Conference Publishing Consulting

23rd ACM SIGPLAN International Workshop on Erlang (Erlang 2024), September 2, 2024, Milan, Italy

Erlang 2024 – Preliminary Table of Contents

Contents - Abstracts - Authors

23rd ACM SIGPLAN International Workshop on Erlang (Erlang 2024)

Frontmatter

Title Page


Message from the Chairs


Committees


Papers

Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang
Florian Berger ORCID logo, Albert Schimpf ORCID logo, Annette Bieniusa ORCID logo, and Stefan Wehr ORCID logo
(University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.

Article Search Info
Erla+: Translating TLA+ Models into Executable Actor-Based Implementations
Marian Hristov ORCID logo and Annette Bieniusa ORCID logo
(University of Kaiserslautern-Landau, Germany)
Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla+, a translator which automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.

Article Search Info
Nominal Types for Erlang
Isabell Huang ORCID logo, John Högberg ORCID logo, Kiko Fernandez-Reyes ORCID logo, and Tobias Wrigstad ORCID logo
(Ericsson, Sweden; Uppsala University, Sweden)
Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.

Article Search
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Jonah Pears ORCID logo, Laura Bocchi ORCID logo, and Raymond HuORCID logo
(University of Kent, United Kingdom; Queen Mary University of London, United Kingdom)
In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.

Article Search
Modeling Erlang Compiler IR as SMT Formulas
John Högberg ORCID logo
(Ericsson, Sweden)
Erlang is an unorthodox language that has fault-tolerance and observability (tracing) baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation. Because the design choices around tracing err on the side of maximum observability, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain. This report describes an ongoing experiment on translating one of the compiler's intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.

Article Search
Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects
Bendegúz Seres ORCID logo, Dániel Horpácsi ORCID logo, and Simon Thompson ORCID logo
(Eötvös Loránd University, Hungary; University of Kent, United Kingdom)
We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any “false positive” counterexamples.

Article Search Info
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio ORCID logo, Lars-Åke Fredlund ORCID logo, Clara Benac Earle ORCID logo, Ángel Herranz ORCID logo, and Julio Mariño ORCID logo
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.

Article Search
Unsafe Impedance: Safe Languages and Safe by Design Software
Lee BarneyORCID logo and Adolfo Neto ORCID logo
(Brigham Young University-Idaho, USA; Federal University of Technology Paraná, Brazil)
In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software pro- ducing organizations to take responsibility for and oversight of the security of the software their organizations produce. In February 2024, the White House released a cybersecurity outline, highlighting the December document. In this work we review the safe languages listed in these documents, and compare the safety of those languages with Erlang and Elixir, two BEAM languages. These security agencies’ declaration of some languages as safe is necessary but insufficient to make wise decisions regarding what language to use when creating code. We propose an additional way of looking at languages and the ease with which unsafe code can be written and used. We call this new perspective unsafe impedance. We then go on to use unsafe impedance to examine nine languages that are considered to be safe. Finally, we suggest that business processes include what we refer to as an Unsafe Acceptance Process. This Unsafe Acceptance Process can be used as part of the memory safe roadmaps suggested by these agencies. Unsafe Acceptance Processes can aid organizations in their production of safe by design software.

Article Search
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder ORCID logo, Christophe De Troyer, Mart Lubbers ORCID logo, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, n.n.)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.

Article Search
Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production
Carla Rodríguez Estévez ORCID logo and Laura M. CastroORCID logo
(Universidade da Coruña, Spain)
Animal shelters are non-governmental organizations that have to face many difficulties in their management and carry out actions to help unprotected animals in the area. Apart from being small organizations and generally having limited resources, many of them also struggle with outdated tools or face challenges in centralizing their information and pro- cesses. However, the main problem faced by them is related to their economic situation and most of the time they need to use free online tools for their management. This work presents and explains a Phoenix web application solution to assist in the management of these groups, which leverages affordable development and easy maintenance with tailoring to meet their main needs. With this experience report, we aim to demonstrate that BEAM technologies, which have already proven their effectiveness in bigger corporate set- tings, such as WhatsApp or Discord, are also well-suited for smaller and more modest environments. Moreover, this aims to be an example of the use of Elixir/Phoenix in a non-profit environment, typical for social and community projects, with needs specific to the world in which they exist.

Article Search

proc time: 3.19