Skip to main content

Robust Communications in Erlang

Harrison, Joseph Richard (2020) Robust Communications in Erlang. Doctor of Philosophy (PhD) thesis, University of Kent,. (doi:10.22024/UniKent/01.02.87484) (KAR id:87484)

PDF
Language: English


Download (1MB) Preview
[thumbnail of 160Robust_Communications_in_Erlang_by_Joseph_Richard_Harrison.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://doi.org/10.22024/UniKent/01.02.87484

Abstract

Erlang is a dynamically-typed functional and concurrent programming language lauded by its proponents for its relatively simple syntax, process isolation, and fault tolerance. The functional aspect has rich features like pattern matching and tail-call optimisation, while the concurrent aspect uses isolated processes and asynchronous message passing to share state between system components. The two meet with pattern matching on mailboxes, which allows for a process to pick a message from its mailbox - potentially out of order - based on its structure, value, type, or a mixture thereof. A strongly and dynamically typed language like Erlang can experience many kinds of runtime errors, such as ill-typed operands to arithmetic operators. The interaction between Erlang's type system and process mailboxes can lead to a more subtle runtime error which is harder to detect: orphan messages. As the types of messages are not checked either at compile time or runtime, a process can be sent a message which it will never receive. Essentially, non-trivial type discrepancies in Erlang programs can cause subtle bugs when communication is involved. These problems can be hard to detect and fix, with current solutions such as extensive testing and exhaustive model checking. This thesis reports on work to detect communication-related type discrepancies in Erlang programs. A fragment of the Core Erlang intermediate format is modelled formally so that we can reason about the out-of-order communication in Erlang systems, particularly the dependencies between sent messages when determining whether orphan messages exist. Afterwards, a sub-typing relation based on Erlang's type system is introduced to clearly define the notion of an orphan message, forming the foundation of a system for automatic detection via a mix of static analysis and runtime verification. This culminates in automatic tooling to detect certain cases of communication discrepancies via static analysis, and automatic instrumentation of concurrent programs to detect and recover from more complicated cases at runtime.

Item Type: Thesis (Doctor of Philosophy (PhD))
Thesis advisor: Thompson, Simon
Thesis advisor: Wang, Meng
DOI/Identification number: 10.22024/UniKent/01.02.87484
Uncontrolled keywords: Erlang concurrency subtyping type checking static analysis hybrid analysis BDDs ROBDDs binary decision diagrams
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: System Moodle
Depositing User: System Moodle
Date Deposited: 07 Apr 2021 10:10 UTC
Last Modified: 20 May 2021 06:56 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/87484 (The current URI for this page, for reference purposes)
  • Depositors only (login required):