Modelling distributed Erlang within a single node.

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.