Erlang 2017 – Proceedings

Message from the Chairs
It is our great pleasure to welcome you to the Sixteenth ACM SIGPLAN Erlang Workshop – Erlang’17. This year’s workshop continues the tradition of being co-located with the annual International Conference on Functional Programming (ICFP) and being a forum for the presentation of research efforts and experience reports on all aspects of theory, implementation, and applications of the Erlang and Erlang-like programming language and related technologies, such as functional programming, distribution, concurrency, scalability, and so on. The Erlang model of concurrent programming has been widely emulated, for example by Akka in Scala, and even new programming languages have been designed atop of the Erlang BEAM VM, such as Elixir and LFE.

Technical Report

Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm
Evgeniy Shishkin
(JSC InfoTeCS, Russia)
Distributed fault-tolerant control algorithms are in great demand nowadays due to their practical importance in cloud computing, Internet of Things (IoT) technology, swarm robotics, and other areas. It is usually hard to make a distributed algorithm fault-tolerant. It is even harder to ensure that such algorithm behaves correctly in the presence of faults of some kind.
In this work, we construct a reliable, adaptive, fault-tolerant distributed mutual exclusion algorithm based on the well-known Ricart-Agrawala algorithm. In order to formally verify it, we use a hybrid approach of deductive reasoning and bounded model-checking.
First, a safety property of the Ricart-Agrawala algorithm is proved in Calculus of Inductive Constructions of Coq proof assistant using assertional reasoning. Then, an extension of that algorithm turning it into fault-tolerant and adaptive to participants set change, is formalized in TLA and checked on a bounded model.
Besides constructing and verifying the algorithm, this work aims to familiarize those interested in constructing highly reliable components with well established verification methods that were used to verify the proposed algorithm.

Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang
Kagumi Azuma, Nagisa Ishiura, Nobuaki Yoshida, and Hiroyuki Kanbara
(Kwansei Gakuin University, Japan; ASTEM RI/KYOTO, Japan)
This paper presents a distributed memory architecture for dedicated hardware automatically synthesized from Erlang programs. Our team had developed a framework for generating embedded systems controllers whose behavior was specified by a subset of Erlang, where each process was mapped into hardware (a logic circuit) running independently of the circuits for the other processes. However, the resulting hardware was not of practical use because it shared a single main memory potentially accessed by all the circuits for the processes simultaneously. To address this issue, in this paper, the main memory is partitioned into banks so that each process can access its own memory independently of the other processes. In order to keep the interconnections for message passing to a practical size, a bus architecture is employed where send requests are arbitrated by an arbiter (logic circuit). In order to make the resulting hardware as small as possible, a garbage collection circuit is shared among the circuits for the processes also under the control of the arbiter. From a simple Erlang specification, Verilog HDL codes for necessary hardware to construct a system has been generated.

eAOP: An Aspect Oriented Programming Framework for Erlang
Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir
(University of Malta, Malta; Reykjavik University, Iceland)
Aspect oriented programming (AOP) is a paradigm ideal for defining cross-cutting concerns within an existing application. Although several AOP frameworks exist for more renowned languages such as Java and C#, little to no frameworks have been developed for actor oriented languages such as Erlang. We thus present eAOP, a new AOP framework specifically designed to instrument actor-oriented constructs in Erlang such as message sends and receives, along with other traditional constructs such as function calls.

Structuring Erlang BEAM Control Flow
Dániel Lukács and Melinda Tóth
(ELTE Eötvös Loránd University, Hungary)
As source code dependencies are usually stored in some precompiled executable representation like bytecode, static analysis frameworks for high-level languages have to be specifically adapted so they can meaningfully analyse these libraries too. This adaptation is not trivial, since compilation is in general not injective, the semantics of low-level instruction sets are often not specified adequately, and the structure of the high-level sources and the low-level target is considerably different. This is also true for the functional Erlang programming language and its assembly-like BEAM bytecode. In this paper, we present a structuring algorithm capable of recovering the Erlang syntax tree of functional branching expressions compiled to BEAM. The implementation of the presented algorithm is part of the RefactorErl static analyser framework. Therefore, the tool is able to represent the semantics of the BEAM programs with an Erlang syntax tree and perform further semantic analysis on it to discover the source dependencies.

The Shared-Memory Interferences of Erlang/OTP Built-Ins
Stavros Aronis and Konstantinos Sagonas
(Uppsala University, Sweden)
Erlang is a concurrent functional language based on the actor model of concurrency. In the purest form of this model, actors are realized by processes that do not share memory and communicate with each other exclusively via message passing. Erlang comes quite close to this model, as message passing is the primary form of interprocess communication and each process has its own memory area that is managed by the process itself. For this reason, Erlang is often referred to as implementing ``shared nothing'' concurrency. Although this is a convenient abstraction, in reality Erlang's main implementation, the Erlang/OTP system, comes with a large number of built-in operations that access memory which is shared by processes. In this paper, we categorize these built-ins, and characterize the interferences between them that can result in observable differences of program behaviour when these built-ins are used in a concurrent setting. The paper is complemented by a publicly available suite of more than one hundred small Erlang programs that demonstrate the racing behaviour of these built-ins.

Info

Towards an Isabelle/HOL Formalisation of Core Erlang
Joseph R. Harrison
(University of Kent, UK)
As part of broader work to improve the safety of Erlang systems, we are attempting to detect (and prevent) messages which remain forever unreceived in process' mailboxes using a mix of static and runtime analysis. We have formalised the communicating portion of Core Erlang using Isabelle/HOL, an interactive theorem prover. We can use the Isabelle toolchain to prove properties of our model, automatically prepare documents, and generate verified executable code in a variety of functional programming languages.
We formally model a communicating fragment of Core Erlang in a language we call CoErl. After defining the evaluation of expressions, we model the process-local and concurrent semantics of the language using a labelled transition system. We also introduce the notion of mailbox traces which capture communication events during process execution. This is followed by some illustrative examples of the concurrent semantics.
Although our CoErl model is a solid foundation for a full formalisation of Core Erlang, it currently lacks higher-order and recursive behaviour. Isabelle/HOL has proved practical for formalising and verifying several properties of CoErl and its trace system, while ongoing and future work focuses on bringing the language to feature parity with Core Erlang and Erlang/OTP.

Experience Report

Towards Change-Driven Testing
Viktória Fördős, István Bozó, and Melinda Tóth
(Klarna, Sweden; ELTE Eötvös Loránd University, Hungary)
Engineering complex business critical systems that should never stop or fail is very much challenging. In Klarna, we tackle this challenge day by day. The secret sauce, which enables us to ensure the highest software quality, is the thorough validation process. However, one must pay the price of such validation process, which is essentially time. In this paper we present our initial work on fast tracking the validation of code changes without compromising software quality and give a preliminary evaluation on our technique.

Erlang 2017 – Proceedings

16th ACM SIGPLAN International Workshop on Erlang (Erlang 2017)

Frontmatter

Technical Report

Experience Report