# CESAn: A Core Erlang Semantics Analyser

Aurélie Kong Win Chang, Jérôme Feret, Gregor Gössler

► To cite this version:

Aurélie Kong Win Chang, Jérôme Feret, Gregor Gössler. CESAn: A Core Erlang Semantics Analyser. DisCoTec 2025 - 20th International Federated Conference on Distributed Computing Techniques / CORSE - Components Operationally: Reversibility and System Engineering, Jun 2025, Lille, France. pp.103-115, 10.1007/978-3-031-99717-4_6. hal-05353119

HAL Id: hal-05353119

https://inria.hal.science/hal-05353119v1

Submitted on 7 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# CESAn: a Core Erlang Semantics Analyser*

Aurélie Kong Win Chang

Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France

Jérôme Feret

Département d'Informatique de l'ENS, ENS, CNRS, PSL University, Inria
Paris, France

Gregor Gössler

Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France

## Abstract

In the concurrent distributed language Erlang, processes interact through message passing and signals. One of the main sources of non-determinism that make Erlang programs difficult to debug, is the order in which messages are handled.

We present a prototype tool called CESAn that implements a small-step semantics that faithfully represents message handling in Core Erlang, enabling the user to investigate the causes of non-determinism in Erlang stemming from message handling. We see CESAn as a building block for debugging and analysis tools for Erlang.

## 1 Introduction

Understanding and debugging concurrent systems is notoriously difficult, in particular due to the difficulty of reproducing particular, faulty executions of a non-deterministic program. Erlang [1] is a functional language for programming large-scale distributed systems such as telecommunication systems. In Erlang, processes interact through message passing. One of the main sources of non-determinism of Erlang programs is the order in which messages are handled. In [17] we have formalized a small-step semantics of a subset of Core Erlang that faithfully represents how, and in which order, messages are handled.

In this paper we present a tool called CESAn [16] that implements the semantics of [17], and that features a minimalistic implementation of an algorithm based on [15], to explain program errors in terms of non-deterministic choices within the program semantics. After a brief presentation of alternative Erlang semantics and related debugging tools that have proposed in the literature, we present the CESAn tool and discuss some of its underlying design choices. We then discuss its application to a simple example of a Core Erlang program whose outcome depends on a race condition involving signal handling, and sketch how CESAn can help in understanding the causes of the non-deterministic program behavior.

<footnote>*This work has been funded by the ANR grant ANR-18-CE25-0007 DCore.</footnote>
## 2 Related work

Erlang is translated by the Erlang compiler in a language with less syntactic sugar: Core Erlang. We thus chose to base our analysis on a subset of Core Erlang. We are aware that there exists another language in which any Erlang code can be translated, and which is used as compilation language by Elixir, seen as a successor of Erlang: Abstract Erlang. However, as it does not have any formal semantics, and the only relevant document on the matter we found was the official documentation, we considered it wiser to stick with Core Erlang.

Our semantics is by no means the first one for Core Erlang. [5] is the most recent official specification of Core Erlang we found, but whilst useful it is informal and partly obsolete. A small step semantics of a subset of Core Erlang was proposed in [20], making some choices such as the order of evaluation of function arguments based on its implementation rather than the official documentation. In [12] and [13], Huch used a semantics of what he called Core Erlang, but was actually a subset of Erlang. A modular reversible semantics for a fragment of Core Erlang is proposed in [21], focused on causal-consistent reversibility. A semantics dedicated to type inference for a subset of Core Erlang was presented in [11]. More recently, [2] formalized a subset of Core Erlang with a big step semantics, following [20] in some aspects, and validated it with the proof assistant Coq. [4] introduced the concept of medium step semantics, which considers as a step not only assignments, but also some events of interactions between processes. This semantics is used by a declarative debugger [3]. Starting from the code and an expression that returned an incorrect value, it explores the execution with the help of questions asked to the developer whether the current evaluation is correct.

However, all these semantics lack the signal handling and monitoring part. The only semantics we found that finely modeled signals [23] treats them as side effects of operations that are instantaneously dealt with. This implies a strong hypothesis on their order of reception, and prevents the generation of scenarios with a degraded network, which are not uncommon in Erlang [14]. Our work inherited of several aspect of some of these contributions: [5] is our main reference document. Our model of signals sent per process is a slightly more general version of [4]'s messages sent box.

Soter [8] implements an actor model close to a subset of Core Erlang equipped with a parametric abstract interpretation framework, ensuring that several sources of infinite state spaces are reduced to finite representations. In particular, the content of mailboxes is abstracted into a multiset, thus losing the ordering of messages. This abstraction would break our analysis of the causes of non-deterministic program behavior.

With a similar goal as our work but an entirely different approach, the tool Concuerror [10] is dedicated to detecting crash events caused by specific race conditions. Starting with the source code, it searches through, and executes, all possible interleavings of operations with side effects, such as message handling, to identify those in which an error occurs. However, no explanation for the error is provided. CauDEr [19] is a causal-consistent reversible debugger for Erlang: in order to undo some action, all of its consequences, and only those, need to be undone beforehand. Using a different notion of causality than the construction of explanations in CESAn, both are complementary [18].
# 3 CESAn

CESAn is open source. It takes as input a Core Erlang program, and outputs its semantic graph G in the form of a labelled transition system, if G is finite. Each state of G is a state of the program execution. Each transition is the application of a rule in the semantic derivation tree of the program. The label of a transition is the name of the rule applied during said transition.

When given, in addition, an execution trace of the program in the form of a path $\pi$ in the semantic graph, and a subset $B$ of set of states of $G$ that are considered as *failing*, CESAn will construct an explanation identifying the subset of transitions of $\pi$ that are choices in $G$ that contribute to bringing the execution closer to $B$, in the sense of [15].

## 3.1 Design choices

CESAn is essentially constituted of two parts. One — which we will refer to as the engine — is dedicated to read the inputs and generate the semantic graph, while the other is in charge of the user interface. The engine is written in Maude [7]. The lack of Maude library dedicated to visual representations is why the user interface is written in Python, which comes with libraries for handling graphs and programming user interfaces.

**Philosophy.** The prototype of [20] has some very good characteristics, such as properly commented code and a functional though slightly outdated Core Erlang parser, and it had been made with modularity on mind. However, the way it was implemented did not allow us to easily implement the graphical user interface we needed. Furthermore, the way some of its modules were intertwined created undesirable dependencies which made it difficult to simply add the semantics we picked to the project. We therefore refactored the code of [20] in order to make it more easily reusable by making it more modular. Some dependencies between modules made it hard to readapt the original code to some specificities of our implementation like the binding with Python instead of just getting a full-text output. Doing so, we also tried to make it easier to read and to change. The adventurous reader wanting to perform such a task will find very useful advice on the matter of refactoring in [9].

We tried to keep the design of CESAn as reusable as possible. As much as possible, we tested our code and automated the test phase with unit tests executable from a makefile command. Right now, everything tested is done so automatically, except for the behavior of the semantics rules, which are visually tested because of a lack of time: the user has to play the role of the oracle. As per the tests themselves, we documented them, saying for each of them what we are testing and, in general, what we are expecting and why if the case is not trivial.

## 3.2 Structure of the implementation

Figure 1 shows a simplified representation of the structure of the code. We tried to keep the number of dependencies between modules low. For instance, if one wanted to parse Erlang instead of Core Erlang while keeping our current
<figure><img src="image_2.png" /><figcaption>Figure 1: Dependency graph of the slightly abstracted structure. Ovals represent groups of modules, and arrows represent dependencies.</figcaption></figure>

internal model, only two files have to be changed: the parsed syntax, and the parser translating from the program syntax to the internal one.

**Maude engine.** As said earlier, the Maude part is dedicated to generating the semantic graph of the program given as input. The core of the engine is the set of Maude modules which implements the semantics of [17] and its syntax, which is slightly different from Core Erlang. For instance, the `receive` instruction no longer exists since the OTP 23 update. This modification of Core Erlang has been done in order to fix some behaviors about maps which are out of the scope of this work. It complicates a lot the code representation and, for our model, it has the same behavior as the old `receive`, which is why we kept a `receive` in the internal syntax. This transformation is handled by the `parsing` modules. The curious reader can see how it is done in lines 236 to 271 and 295 to 315 of the `parsing.maudle` file.

The internal syntax, a more explicit variant of the Core Erlang syntax, is used by the Maude engine, where are implemented the rules of our semantics. A simple rule such as `MONITOR` is implemented in Maude as shown in Figure 2. For other rules such as `SUBEXPR_OK` shown in Figure 3, the translation is somewhat less straight-forward. In order to have Maude rewrite the sub-expressions step by step, we use meta-level rewriting [6].

**Python interface and graphical representation.** CESAn is started with a command-line interface written in Python. The user is able to describe the
<figure><img src="image_3.png" /><figcaption>Figure 5: Interactive user interface showing the semantic graph of a Core Erlang program along with information about the selected state.</figcaption></figure>

initial state — as the one shown in Figure 4 — of the system to be analyzed. This description is then pre-processed with a Perl script based on the one of [20] in order to make it compatible with Maude. The Python side is also in charge of generating a graphical representation of the Maude output. Knowing the kind of framework we ultimately wanted to create, we chose netgraph, a Python library that enables interactive representations. Thanks to it, it is possible to display a wealth of information while still keeping it readable. netgraph offers the possibility of zooming in the graph, as well as moving nodes and edges, and export the graph. However, netgraph has shown some limits, such as the impossibility to create interactive tables linked to the interactive graph without lengthy code. It would be worthwhile considering the use of more versatile tools, or swap to another language, for the user interface of CESAn.

Figure 5 shows the user interface of CESAn after analyzing the example of Section 4. The left-hand side shows the semantic graph generated by the Maude engine. Each state of the graph represents a state of the program execution, and each arrow represents the semantics rule applied in order to go from one state to another. The label on the arrows indicates the name of the rule that has been applied, and the identifier of the process(es) modified by the rule. Clicking on a state will make a table appear on the right-hand side. This table describes the selected state.

**About testing.** Unfortunately, Maude does not seem to have a library dedicated to unit testing. This is why all of the automated tests are written in Python and use the `unittest` Python library. The downside of this situation is that, in order to test Maude code, we are actually comparing strings instead of directly comparing Maude entities. This means, and it happened, that if some-
thing changes in the binding Python library about how Maude is translated to Python strings, all of the tests dedicated to Maude parts of the system will fail.

It is possible to run all or part of the automatized tests through commands defined in the Makefile.

## 3.3 Using CESAn

CESAn is used through command line. As said earlier, from the description of the initial state of the system the user will want to analyze, it will generate its semantic graph. There are two ways to describe such an initial state:

* either by giving it directly, in a file, written in the internal language of CESAn,

* or by giving the first expression evaluated by the first process of the system and, if needed, the path to the file in which a Core Erlang module is described.

**Directly describing a state.** The first option gives the most freedom to the users, allowing them to describe a system composed of any number of processes, themselves in any valid state. For instance, Figure 4 shows a system composed of two processes. The one of identifier `pid(0)` creates a new process by calling the function `spawn`, and the one of identifier `pid(1)` evaluates the instruction `do 1 2`. The two processes are separated with three pipes `|||`, and after the description of the processes global information about the system is given, such as the table of the functions loaded by default on any new process of the system, and the list of the identifiers already in use. More information about the way to describe such systems is given in the documentation of CESAn, and more examples can be found in the `tests` repository. The call to CESAn is then

```
python CESAn from_file path
```

where `path` is the path of the file containing the description of the system state.

**Creating the initial state from the first expression called.** It is also possible to ask CESAn to generate itself the initial state of a system, by giving it the first expression evaluated by the first process, and optionally a module in Core Erlang to load. The module can be written by hand or generated by the Erlang compiler.

If no module needs to be loaded, the call to CESAn is

```
python CESAn create_state expr
```

where `expr` is the first expression called. If a module needs to be loaded, this call becomes

```
python CESAn create_state expr --src_module path
```

where `path` is the path of the file of the module, or, in a shorter way:

```
python CESAn create_state expr --m path
```
**Interacting with the graph.** Once the semantic graph is generated, it is possible to interact with it, e.g. by moving nodes and zooming in or out. Clicking on a node gives access to more information about the state it represents, in the table on the right of the graph Figure 5. For each process of the system at the state represented by the selected node, one can get what is the next expression it will evaluate, the map $\theta$ of the affected variable with their value, the module of the last evaluated expression, the value currently stored as the reason of the termination of the process, the list of signals sent by the process, and the links existing between the process and the other ones of the system.

## 4 Example

Consider a simple program composed of one process, of identifier pid(0), that is about to evaluate the expression

```
do call "erlang": "spawn" ("mod1", "f", [1, 2]) call "erlang"
: "monitor"("process", pid(1))
```

The process spawns a new process, of identifier pid(1), and then creates a monitor link with it. The new process calls function f in module mod1 to evaluate the expression do on its input parameters:

```
1 module 'mod1' ['f' / 2]
2 attributes []
3 ('f' / 2 =
4 fun (X,Y) ->
5 do X Y)
6 end
```

**Generating the semantic graph.** Figure 6 shows the semantic graph of our program as generated by CESAn. The initial state is on the top of the graph, in bold. Each transition is represented with an arrow, and its label tells which rule has been applied and which processes have been modified.

**Explaining a failure.** Consider the program execution shown in bold in the semantic graph of Figure 7. We assume here that the execution is fully observable. Further suppose that we expect our program to behave in such a way that by the end of the execution of the program, the process in charge of the computation must have sent to its monitoring process the message saying it has ended. This is our expected safety property *P*. Figure 7 highlights in green the states where the message to the monitoring process has been sent (and hence *P* is satisfied), and in red the states where the program has ended without the message being sent (and hence *P* is violated); the colors have been added manually. Obviously, our execution path $\pi$ violates *P*.

In order to evaluate how much the order in which messages have been handled causes the observed fault, we use the algorithm of [15]. It describes a game-theoretic approach to explain error traces, which we instantiate for our needs as follows. The state space is partitioned into a set of *n* layers such that from layer 0 a violation of the safety property is inevitable, and from each layer
<figure><img src="image_4.png" /><figcaption>Figure 6: Semantic graph of the example program.</figcaption></figure>
<figure><img src="image_5.png" /><figcaption>Figure 7: Semantic graph of the example program. The execution path $\pi$ is shown in bold. States where the message to the monitoring process has been sent are shown in green. States where the program has ended without the message being sent are shown in red.</figcaption></figure>
$1 \le i \le n-1$, a single bad choice is sufficient to enter layer $i-1$. Hence, the layer to which a state belongs indicates how precarious it is, in terms if its distance to the property violation.

Figure 8 shows the result of applying the analysis to the semantic graph of our example. The numbers on the states represent the layer they are part of. The layer from which the property violation is inevitable is shown in orange. A transition crossing layers towards a lower layer contributes to the program execution violating the property, and gives a hint to which order to enforce so as to fix the program. In our example the termination of the process with pid(1) is fatal in the state where it happens. By following, from the last state of the highlighted execution that belongs to layer 1, the *safe alternatives* that remain within layer 1, one can see that satisfaction of *P* is ensured by the partial order of precedence

sig-monitored-by-ij["pid(0)", "pid(1)"] < term-Val["pid(1)"] < term-Val["pid(0)"].

# 5 Discussion

CESAn is a proof of concept tool that needs to be improved in many ways, but we hope that it will be useful in exploring new analyses. First an foremost, an abstraction is needed to be able to handle programs with a large or infinite state space, and to focus explanations on an appropriate level of abstraction. Beyond explaining failures, leveraging the mechanisms used for localizing bugs for program *repair* is not a new idea, but doing this in our framework looks like a promising avenue of work.

From the point of view of user experience, our first tests suggest that the — basic — interactive graphical representation of the explanation in CESAn helps the user in grasping the causes of a failure. More specifically, it can be used in order to enrich the programmers’ foraging diet [22] and give them some hints during the exploration of the behaviors of the system in order to debug it. For instance, a graphical representation of the layers could provide hints about where to investigate alternatives to transitions bringing the system closer to a failure, enabling the user to explore them interactively. CESAn has, however, not been confronted to the field yet. User feedback would certainly raise many suggestions on how it is actually used, and knowing that the use of a tool can change the way data is explored [24], we would be interested in seeing how developers explore data when using CESAn.

# References

[1] Joe L. Armstrong. *Making reliable distributed systems in the presence of software errors*. PhD thesis, The Royal Institute of Technology Stockholm, Sweden, 2003.

[2] Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson. Machine-checked natural semantics for Core Erlang: exceptions and side effects. In *Proceedings of the 19th ACM SIGPLAN International Workshop on Erlang*, pages 1–13, Virtual Event USA, August 2020. ACM.
<figure><img src="image_6.png" /><figcaption>Figure 8: Semantic graph of the example program, with the premises of our explanation.</figcaption></figure>
[3] Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, and Salvador Tamarit. Declarative debugging of concurrent Erlang programs. *Journal of Logical and Algebraic Methods in Programming*, 101:22–41, December 2018.

[4] Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, and Salvador Tamarit. A core Erlang semantics for declarative debugging. *Journal of Logical and Algebraic Methods in Programming*, 107:1–37, October 2019.

[5] Richard Carlsson, Thomas Lindgren, Bjorn Gustavsson, Sven-Olof Nystrom, Robert Virding, Erik Johansson, and Mikael Pettersson. Core Erlang 1.0.3 language specification. Technical report, 2004.

[6] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C.L. Talcott. *All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic*, volume 4350 of LNCS. Springer, 2007.

[7] Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Marti-Oliet, José Meseguer, Rubén Rubio, and Carolyn Talcott. Maude manual (version 3.1). *SRI International University of Illinois at Urbana-Champaign http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html*, 2020.

[8] E. D'Osualdo, J. Kochems, and L. Ong. Automatic Verification of Erlang-Style Concurrency. In D. Hutchison, T. Kanade, J. Kittler, J.M. Kleinberg, F. Mattern, J.C. Mitchell, M. Naor, O. Nierstrasz, C. Pandu Rangan, B. Steffen, M. Sudan, D. Terzopoulos, D. Tygar, M.Y. Vardi, G. Weikum, F. Logozzo, and M. Fähndrich, editors, *Static Analysis*, volume 7935, pages 454–476. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. LNCS.

[9] Martin Fowler. Refactoring: improving the design of existing code. Addison-Wesley signature series. Addison-Wesley, Boston, second edition edition, 2019. OCLC: on1064139838.

[10] Alkis Gotovos, Maria Christakis, and Konstantinos Sagonas. Test-driven development of concurrent programs using concuerror. In *Proceedings of the 10th ACM SIGPLAN workshop on Erlang - Erlang '11*, page 51, Tokyo, Japan, 2011. ACM Press.

[11] Joseph Harrison. Automatic detection of core Erlang message passing errors. In *Proceedings of the 17th ACM SIGPLAN International Workshop on Erlang*, pages 37–48, St. Louis MO USA, September 2018. ACM.

[12] Frank Huch. Verification of Erlang programs using abstract interpretation and model checking. In *Proceedings of the fourth ACM SIGPLAN international conference on functional programming*, Icfp '99, pages 261–272, New York, NY, USA, 1999. Association for Computing Machinery. Number of pages: 12 Place: Paris, France.

[13] Frank Huch. Verification of Erlang Programs using Abstract Interpretation and Model Checking. PhD thesis, RWTH Aachen, 2001.
[14] Fred Hébert. Stuff goes bad Erlang in anger. https://www.erlang-in-anger.com, 2016.

[15] HoonSang Jin, Kavita Ravi, and Fabio Somenzi. Fate and free will in error traces. *International Journal on Software Tools for Technology Transfer*, 6(2):102–116, August 2004.

[16] A. Kong Win Chang. CESAn: a core erlang semantics analyser. https://gitlab.inria.fr/dcore-pub/erlangsemantics.git, 2025.

[17] Aurélie Kong Win Chang, Jérôme Feret, and Gregor Gössler. A Semantics of Core Erlang with Handling of Signals. In *Proceedings of the 22nd ACM SIGPLAN International Workshop on Erlang*, pages 31–38, Seattle WA USA, August 2023. ACM.

[18] Ivan Lanese and Gregor Gössler. Causal debugging for concurrent systems. In Torben Ægidius Mogensen and Lukasz Mikulski, editors, *Reversible Computation - 16th International Conference, RC 2024, Toruń, Poland, July 4-5, 2024, Proceedings*, volume 14680 of LNCS, pages 3–9. Springer, 2024.

[19] Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In John P. Gallagher and Martin Sulzmann, editors, *Functional and Logic Programming*, volume 10818 of LNCS, pages 247–263. Springer International Publishing, Cham, 2018.

[20] Martin Neuhäußer and Thomas Noll. Abstraction and Model Checking of Core Erlang Programs in Maude. *Electronic Notes in Theoretical Computer Science*, 176(4):147–163, July 2007.

[21] Naoki Nishida, Adrián Palacios, and Germán Vidal. A Reversible Semantics for Erlang. In Manuel V Hermenegildo and Pedro Lopez-Garcia, editors, *Logic-Based Program Synthesis and Transformation*, volume 10184 of LNCS, pages 259–274. Springer International Publishing, Cham, 2017.

[22] David J. Piorkowski, Scott D. Fleming, Irwin Kwan, Margaret M. Burnett, Christopher Scaffidi, Rachel K.E. Bellamy, and Joshua Jordahl. The whats and hows of programmers’ foraging diets. In *Proceedings of the SIGCHI Conference on Human Factors in Computing Systems*, pages 3063–3072, Paris France, April 2013. ACM.

[23] Hans Svensson and Lars-Åke Fredlund. A more accurate semantics for distributed erlang. In *Proceedings of the 2007 SIGPLAN workshop on Erlang Workshop - Erlang '07*, page 43, Freiburg, Germany, 2007. ACM Press.

[24] M. Adil Yalçin, Niklas Elmqvist, and Benjamin B. Bederson. Cognitive Stages in Visual Data Exploration. In *Proceedings of the Sixth Workshop on Beyond Time and Errors on Novel Evaluation Methods for Visualization*, pages 86–95, Baltimore MD USA, October 2016. ACM.