Erlang 2018 – Proceedings

Full Document

It is our great pleasure to welcome you to the Seventeenth ACM SIGPLAN Erlang Workshop (Erlang’18), which is once again co-located with the annual International Conference on Functional Programming (ICFP), held in St. Louis, Missouri. The workshop continues the tradition of being a forum for presenting research effort and experience reporting on all aspects of theory, implementation, and applications of the Erlang language and BEAM-related technologies, which typically include topics such as functional programming, distribution, concurrency, scalability, etc. The Erlang model of concurrent programming has been widely emulated, for example by Akka in Scala and Java, and a wave of exciting programming languages are being developed atop of the Erlang VM (BEAM), such as Elixir.
Full Document

We present iDeA, an immersive user interface for debugging concurrent actor programs communicating through asynchronous message passing. iDeA is based on the hypothesis that debugging and understanding actor programs is a cognitive task which can be greatly facilitated by the visualization and interaction capabilities of modern immersive environments. The fundamental abstraction for visualization in iDeA is a concurrent trace: a partially ordered sequence of asynchronous messages exchanged in the execution. iDeA provides a 3D interface in virtual reality for users to visualize and manipulate program traces: users can set breakpoints, query actor state, step through traces forward and backward, and perform causal history of messages in a trace. While the modularity of iDeA enables debugging any actor program provided that the program events are collected and communicated to the visualization end, our implementation of iDeA targets actor programs written in Akka framework in Scala.
Full Document

Formal specifications of software applications are hard to understand, even for domain experts. Because a formal specification is abstract, reading it does not immediately convey the expected behaviour of the software. Carefully chosen examples of the software’s behaviour, on the other hand, are concrete and easy to understand—but poorly-chosen examples are more confusing than helpful. In order to understand formal specifications, software developers need good examples.

We have created a method that automatically derives a suite of good examples from a formal specification. Each example is judged by our method to illustrate one feature of the specification. The generated examples give users a good understanding of the behaviour of the software. We evaluated our method by measuring how well students understood an API when given different sets of examples; the students given our examples showed significantly better understanding.

Full Document

This paper was motivated by a challenge we faced while re-architecting a critical component in Klarna's software stack. We wanted to increase our confidence about correctness aspects of a new distributed algorithm, developed for an Erlang system at the very core of Klarna's business. Reasoning about the correctness of concurrent Erlang systems is a difficult task, but tools exist that can help, for instance, Concuerror. However, our algorithm was intimately linked to distributed Erlang's behaviours, which are not supported by Concuerror. The solution we came up with was to design and implement vnet, a modelling library which can be used to simulate the behaviour of distributed Erlang nodes within a single Erlang node. We discuss aspects of vnet showing its capabilities and limitations. We also report on two case studies, showing how vnet can be used to prototype, test and verify simple and advanced distributed Erlang systems. We finally demonstrate that we were able to find errors and verify properties in the systems of our case studies, using Concuerror.
Full Document

Erlang's powerful communication model allows us to build high-level concurrent systems. These can, however, harbour subtle communication errors less severe than global deadlock or crashes: messages never received can degrade performance and consume swaths of memory. We believe that some of these errors can be quickly detected with static analysis. We have built a prototype tool which operates at the Core Erlang level to assist identification of some of these errors. We present a fragment of Erlang's type system as a subtyping relation, following up with type inference functions for a portion of Core Erlang's patterns, guards, and message syntax. The implementation of the prototype is detailed, noting specific behaviours of the Erlang compiler and nuances of Core Erlang's syntax along the way, some of which complicate our analysis. Although our tool is at a very early stage of development, we show examples of the errors we can identify, despite using a considerable over-approximation in our type inference system. After comparing our tool to other work in the Erlang community and beyond, we reflect on the current state of the prototype, before considering further applications of our concept of message compatibility.
Full Document

Developing a static type system suitable for Erlang has been of ongoing interest for almost two decades now. The challenge with retrofitting a static type system onto a dynamically typed language, such as Erlang, is the loss of flexibility in programming offered by the language. In light of this, many attempts to type Erlang trade sound type checking for the ability to retain flexibility. Hence, simple type errors which would be caught by the type checker of a statically typed language are easily missed in these developments. This has us wishing for a way to avoid such errors in Erlang programs. In this paper, we develop a static type system for Erlang which strives to remain sound without being too restrictive. Our type system is based on Hindley-Milner type inference, however it---unlike contemporary implementations of Hindley-Milner---is flexible enough to allow overloading of data constructors, branches of different types etc. Further, to allow Erlang's dynamic type behaviour, we employ a program specialization technique called partial evaluation. Partial evaluation simplifies programs prior to type checking, and hence enables the type system to type such behaviour under certain restricted circumstances.
Full Document

Distributed systems are more important in systems design than ever. Partitioning systems into independent, distributed components has many advantages but also brings about design challenges. The OTP framework addresses such challenges by providing process templates that separate application-dependent from application-specific logic. This way the OTP framework hosts a variety of modeling techniques, e.g., finite state machines. Petri nets are a modeling technique especially suited for distributed systems. We introduce gen_pnet, a behavior for designing Erlang processes as Petri nets. We give a short introduction to Petri net semantics and demonstrate how Erlang applications can be modeled as Petri nets. Furthermore, we discuss two Erlang applications modeled and implemented as Petri nets. For both applications we introduce a Petri net model and discuss design challenges.
Full Document

At Klarna we handle customer's data with utmost care since we believe protecting data is one of the most basic obligations of any companies. Achieving our goal requires more effort since the Erlang ecosystem was designed for private networks where the concern about malicious users performing attacks was not given relevance. Therefore, every day we also put on our security hat to develop and review code changes going into production. In this paper, we show the challenges that today's Erlang systems are faced with and explain why all Erlang developers and operators must have a security aware mindset.
Full Document