Joseph Harrison
ABSTRACT
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.
- Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. 2017. Behavioural Types: From Theory to Tools. River Publishers, Chapter 3, 49–76.Google Scholar
- F. Barbanera, M. Dezaniciancaglini, and U. Deliguoro. 1995. Intersection and Union Types: Syntax and Semantics. Information and Computation 119, 2 (1995), 202 – 230. Google ScholarDigital Library
- Richard Carlsson. 2001. An introduction to Core Erlang. In PLI’01 Erlang Workshop.Google Scholar
- Richard Carlsson, Björn Gustavsson, Erik Johansson, Thomas Lindgren, Sven-Olof Nyström, Mikael Pettersson, and Robert Virding. 2004. Core Erlang 1.0.3 language specification. Technical Report. Uppsala University.Google Scholar
- Maria Christakis and Konstantinos Sagonas. 2011. Detection of Asynchronous Message Passing Errors Using Static Analysis. In Practical Aspects of Declarative Languages. Springer, Berlin, Heidelberg, 5–18. Google ScholarDigital Library
- Emanuele D’Osualdo, Jonathan Kochems, and C. H. Luke Ong. 2013. Automatic Verification of Erlang-Style Concurrency. In Static Analysis, Francesco Logozzo and Manuel Fähndrich (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 454–476.Google Scholar
- Emanuele D’Osualdo, Jonathan Kochems, and Luke Ong. 2013. SOTER - Safety verifier fOr The ERlang language. https://mjolnir.cs.ox.ac.uk/ soter/Google Scholar
- Erlang/OTP Team. 2018. Erlang Reference Manual. Ericsson AB. v9.3, Chapter: Expressions.Google Scholar
- Erlang/OTP Team. 2018. Erlang/OTP. http://erlang.org/download/ otp_src_20.3.tar.gz v20.3.Google Scholar
- Lars Fredlund and Hans Svensson. 2007. McErlang: A Model Checker for a Distributed Functional Programming Language. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP ’07). ACM, New York, NY, USA, 125–136. Google ScholarDigital Library
- Alkis Gotovos, Maria Christakis, and Konstantinos Sagonas. 2011. Testdriven Development of Concurrent Programs Using Concuerror. In Proceedings of the 10th ACM SIGPLAN Workshop on Erlang (Erlang ’11). ACM, New York, NY, USA, 51–61. Google ScholarDigital Library
- Joe Harrison. 2018. sigwinch28/pdis: Erlang’18 artifact.Google Scholar
- Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A Static Verification Framework for Message Passing in Go Using Behavioural Types. In Proceedings of the 40th International Conference on Software Engineering (ICSE ’18). ACM, New York, NY, USA, 1137– 1148. Google ScholarDigital Library
- Tobias Lindahl and Konstantinos Sagonas. 2006. Practical Type Inference Based on Success Typings. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’06). ACM, New York, NY, USA, 167–178. Google ScholarDigital Library
- Simon Marlow and Philip Wadler. 1997. A Practical Subtyping System for Erlang. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (ICFP ’97). ACM, New York, NY, USA, 136–149. Google ScholarDigital Library
- Rumyana Neykova and Nobuko Yoshida. 2017. Let It Recover: Multiparty Protocol-induced Recovery. In Proceedings of the 26th International Conference on Compiler Construction (CC 2017). ACM, New York, NY, USA, 98–108. Google ScholarDigital Library
- Sven-Olof Nyström. 2003. A Soft-typing System for Erlang. In Proceedings of the 2003 ACM SIGPLAN Workshop on Erlang (ERLANG ’03). ACM, New York, NY, USA, 56–71. Google ScholarDigital Library
- David J. Pearce. 2013. Sound and Complete Flow Typing with Unions, Intersections and Negations. In Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 7737 (VMCAI 2013). Springer-Verlag, Berlin, Heidelberg, 335– 354. Google ScholarDigital Library
- Josef Svenningsson. 2018. A gradual type system. (06 2018). Talk at Code BEAM STO.Google Scholar
Index Terms
- Automatic detection of core Erlang message passing errors
Recommendations
Bidirectional typing for Erlang
Erlang 2021: Proceedings of the 20th ACM SIGPLAN International Workshop on ErlangErlang is a strict, dynamically typed functional programming language popular for its use in distributed and fault-tolerant applications. The absence of static type checking allows ill-typed programs to cause type errors at run time. The benefits of ...
Typing the wild in Erlang
Erlang 2018: Proceedings of the 17th ACM SIGPLAN International Workshop on ErlangDeveloping 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 ...
Runtime type safety for Erlang/otp behaviours
Erlang 2019: Proceedings of the 18th ACM SIGPLAN International Workshop on ErlangCallback-oriented Erlang/OTP behaviours such as the gen_server library are susceptible to malformed requests and ill-typed messages, causing server processes to crash unless a defensive programming style is used. We contribute an alternative approach in ...
Comments