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.
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.
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.
Implementing concurrent systems based on asynchronous communications is intrinsically complex. 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.
The rising threat of climate change is leading countries to commit to ambitious carbon-reduction goals. Concurrently, a significant portion of Fortune 500 companies are targeting carbon emission cuts by 2030. As digital integration grows, Technology represents a huge opportunity, yet, the energy footprint of software is often overlooked. Each application transaction, interaction and new data asset adds to the energy demand, making sustainable software and data practices crucial. While improving sustainability in data and software alone won't solve climate change, with an understanding of technology's contribution to carbon emissions, a focus on tech's foundational elements at multiple levels can pave the way for more substantial reductions in the future: (i) Software engineers can reduce the carbon emissions from their software and data by being aware of the effects of their choices. (ii) CTOs can make environmental sustainability a non-functional requirement for all software development. (iii) Companies can incorporate the environmental effects of software as a metric when gauging the quality of a solution. The goal is to cultivate a culture that embeds environmental sustainability into standard software and data engineering practices. Now is the perfect time to start!
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 newversions 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.
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.
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.
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.
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.
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 producing 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.
We introduce a small step semantics for a subset of Core Erlang modeling its monitoring and signal systems. The goal of our semantics is to enable the construction of causal explanations for property violations, which will be the object of future work. As a first axis of reflection, we chose to study the impact of the order of messages on a faulty behavior. We present our semantics and discuss some of our design choices. This work is a part of a broader project on causal debugging of concurrent programs in Erlang.
Mnesia, an Erlang distributed database, serves as an embedded storage and replication layer for OTP applications requiring low read latency and high availability. EMQX is a publish-subscribe message broker supporting the MQTT protocol that uses Mnesia to replicate its internal state across the cluster. We analyze the limitations of Mnesia's replication protocol scalability in large clusters under high load. To address these limitations, we developed Mria, an extension to the Mnesia database that provides eventual consistency within a cluster and achieves better horizontal scalability. We validated Mria using a variety of testing techniques, including model checking, chaos engineering, and formal verification. Replacing Mnesia with Mria allowed us to scale the EMQX cluster to 23 nodes, handle 100 million simultaneous client sessions and achieve a higher sustained load.
The Transport Layer Security (TLS) protocol is one of the most used protocols to ensure data privacy, integrity and authenticity on the Internet. Erlang/OTP's TLS implementation is widely used in industry, and especially in the telecommunication sector. This paper describes an overview of the TLS protocol in the context of Erlang. We explain Erlang/OTP's TLS protocol design and implementation, optimizations, a benchmark evaluation of the Erlang TLS protocol implementation against previous Erlang/OTP's TLS implementations, and a benchmark comparison against the Go's TLS implementation.
In the ever-evolving world of software development, code analysis stands as a critical component for quality and efficiency. This keynote will present an overview of code analysis tools at WhatsApp, and then delve into the techniques of dynamic and static analysis, with examples of their industrial deployments. The keynote will discuss the integration of code analysis into early stages of the software development life cycle, from continuous integration pipelines to DevOps practices.
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
In the last two years at WhatsApp we have developed eqWAlizer - a type-checker for Erlang AS IS - in style of Flow, Pyre, Hack. It’s already used in a significant part of our codebase. In this talk we overview the key eqWAlizer's design choices we made and explain the reasons behind them. Moreover, we'll report about the challenges of using Erlang in large code bases and how static typing has allowed us to scale development through providing fast signal to developers. Finally, we'll also present the lessons learned from enabling static typing for the code underpinning the largest messaging app in the world.
Federated Learning allows multiple distributed agents to contribute to a global machine learning model. Each agent trains locally and contributes to a global model by sending gradients to a central parameter server. The approach has some limitations: 1) some events may only occur in the local environment, so a global model may not perform as well as a specialized model; 2) changes in the local environment may require an agent to use some dedicated model, that is not available in a single global model; 3) a single global model approach is unable to derive new models from dealing with complex environments. This paper proposes a novel federated learning approach, CAEFL, that is local environment aware and composes new dedicated models for new complex environments. CAEFL is implemented in Elixir to exploit transparent distribution, pattern matching, and hot-code-swapping. Pattern matching is used to transform environment sensors data to corresponding tags and aggregate data with the same environment tags on agents. It is also used on parameter server to match client's push/pull request for these tagged models. It enables a declarative way for environment aware federated learning approach. CAEFL outperforms state of the art federated learning by 7-10% for the MNIST dataset and 2% for the FashionMNIST dataset in specific and complex environments.
In this paper we introduce InfERL, an open source, scalable, and extensible static analyzer for Erlang, based on Meta’s Infer tool. InfERL has been developed at WhatsApp and it is deployed to regularly scan WhatsApp server’s Erlang code- base, detecting reliability issues and checking user-defined properties. The paper describes the Erlang specific technical challenges we had to address and our design choices. We also report on our experience in running InfERL on Erlang code at scale, supporting the messaging app used everyday by over 2 billion people.
This paper discusses our experiences troubleshooting and optimizing Hyper-Q, an enterprise software written in Erlang. Hyper-Q implements database virtualization that translates the SQL queries of an existing application to a new database system and converts the data returned by the database system to the data representation expected by the existing application. Using a real world example, we present effective troubleshooting techniques to identify poor-performing code and general refactorings and optimizations that can improve the performance of other Erlang systems.
