Erlang '20: "Machine-Checked Natural Semantics ..."
Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
This research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language.
In this paper, we present an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.
@InProceedings{Erlang20p1,
author = {Péter Bereczky and Dániel Horpácsi and Simon J. Thompson},
title = {Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3406085.3409008},
year = {2020},
}
Publisher's Version
Erlang '20: "Teaching Practical Realistic ..."
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Peter Zeller, Annette Bieniusa, and Carla Ferreira
(TU Kaiserslautern, Germany; Nova University of Lisbon, Portugal)
Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.
In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.
@InProceedings{Erlang20p14,
author = {Peter Zeller and Annette Bieniusa and Carla Ferreira},
title = {Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3406085.3409009},
year = {2020},
}
Publisher's Version
Erlang '20: "Transformations towards Clean ..."
Transformations towards Clean Functional Code
Boldizsár Poór, Melinda Toth, and István Bozó
(Eötvös Loránd University, Hungary)
The programming style has an impact on the readability and comprehensibility of the source code, and it may also affect run-time performance. This statement also holds for functional languages when the functional style is mixed with imperative design. In this paper, we present a couple of methods that can refactor imperatively styled Erlang source-code into a more functionally styled one. This can be done by transforming unnecessary calls to length, hd and tl into pattern matching or by lifting particular nested expressions. The results of our investigations indicate that these refactorings can not only shorten the length of the source code but also affect the complexity/readability. In this paper, we present some refactorings; moreover, real-life examples and data for its validation.
@InProceedings{Erlang20p24,
author = {Boldizsár Poór and Melinda Toth and István Bozó},
title = {Transformations towards Clean Functional Code},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3406085.3409010},
year = {2020},
}
Publisher's Version
Erlang '20: "Clojerl: The Expressive Power ..."
Clojerl: The Expressive Power of Clojure on the BEAM
Juan Facorro and Natalia Chechina
(Bournemouth University, UK)
The development of new features and approaches in programming languages is a continuous and never-ending task, as languages are ultimately tools for expressing and solving problems. The past decade has seen a surge in languages implemented for the BEAM as part of a search to combine the fault-tolerance and scalability of the BEAM with a set of desired language features.
In this paper we present Clojerl, an implementation of the Clojure language with a rich set of data processing capabilities and the expressive power of Lisp for the BEAM. The main design principles of Clojerl are to provide (1) seamless interoperability with the BEAM to enable frictionless interaction with other BEAM languages and (2) portability with Clojure to enable existing Clojure code to run on the BEAM with little or no modifications. We evaluate Clojerl by running a set of experiments that analyse the performance of eight most widely used expressions. While the results of complex expressions show that Clojerl requires further optimisations, Clojerl significantly outperforms Clojure in a set of basic expressions, confirming that Clojerl has the potential to provide a competitive performance while offering a rich set of programming language features.
@InProceedings{Erlang20p41,
author = {Juan Facorro and Natalia Chechina},
title = {Clojerl: The Expressive Power of Clojure on the BEAM},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {41--52},
doi = {10.1145/3406085.3409012},
year = {2020},
}
Publisher's Version
Erlang '20: "Clojerl: The Expressive Power ..."
Clojerl: The Expressive Power of Clojure on the BEAM
Juan Facorro and Natalia Chechina
(Bournemouth University, UK)
The development of new features and approaches in programming languages is a continuous and never-ending task, as languages are ultimately tools for expressing and solving problems. The past decade has seen a surge in languages implemented for the BEAM as part of a search to combine the fault-tolerance and scalability of the BEAM with a set of desired language features.
In this paper we present Clojerl, an implementation of the Clojure language with a rich set of data processing capabilities and the expressive power of Lisp for the BEAM. The main design principles of Clojerl are to provide (1) seamless interoperability with the BEAM to enable frictionless interaction with other BEAM languages and (2) portability with Clojure to enable existing Clojure code to run on the BEAM with little or no modifications. We evaluate Clojerl by running a set of experiments that analyse the performance of eight most widely used expressions. While the results of complex expressions show that Clojerl requires further optimisations, Clojerl significantly outperforms Clojure in a set of basic expressions, confirming that Clojerl has the potential to provide a competitive performance while offering a rich set of programming language features.
@InProceedings{Erlang20p41,
author = {Juan Facorro and Natalia Chechina},
title = {Clojerl: The Expressive Power of Clojure on the BEAM},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {41--52},
doi = {10.1145/3406085.3409012},
year = {2020},
}
Publisher's Version
Erlang '20: "Teaching Practical Realistic ..."
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Peter Zeller, Annette Bieniusa, and Carla Ferreira
(TU Kaiserslautern, Germany; Nova University of Lisbon, Portugal)
Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.
In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.
@InProceedings{Erlang20p14,
author = {Peter Zeller and Annette Bieniusa and Carla Ferreira},
title = {Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3406085.3409009},
year = {2020},
}
Publisher's Version
Erlang '20: "Secure Design and Verification ..."
Secure Design and Verification of Erlang Systems
Viktória Fördős
(Cisco Systems, Sweden)
Security is a critical part of software development, companies have the utmost responsibility to protect their customers data against any threat. Secure design is a key enabler, since it cultivates security awareness in software projects from day zero. In this paper it is shown how to apply the principles of secure design to Erlang software projects. An Erlang specific method to identify trust zones is presented. The high risk vulnerabilities of the Erlang ecosystem are reviewed and grouped together using the CIA triad model. A dataflow based static analysis together with a prototype to verify security posture of a trust zone are introduced and evaluated using Riak Core as a case study.
@InProceedings{Erlang20p31,
author = {Viktória Fördős},
title = {Secure Design and Verification of Erlang Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {31--40},
doi = {10.1145/3406085.3409011},
year = {2020},
}
Publisher's Version
Erlang '20: "Machine-Checked Natural Semantics ..."
Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
This research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language.
In this paper, we present an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.
@InProceedings{Erlang20p1,
author = {Péter Bereczky and Dániel Horpácsi and Simon J. Thompson},
title = {Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3406085.3409008},
year = {2020},
}
Publisher's Version
Erlang '20: "Transformations towards Clean ..."
Transformations towards Clean Functional Code
Boldizsár Poór, Melinda Toth, and István Bozó
(Eötvös Loránd University, Hungary)
The programming style has an impact on the readability and comprehensibility of the source code, and it may also affect run-time performance. This statement also holds for functional languages when the functional style is mixed with imperative design. In this paper, we present a couple of methods that can refactor imperatively styled Erlang source-code into a more functionally styled one. This can be done by transforming unnecessary calls to length, hd and tl into pattern matching or by lifting particular nested expressions. The results of our investigations indicate that these refactorings can not only shorten the length of the source code but also affect the complexity/readability. In this paper, we present some refactorings; moreover, real-life examples and data for its validation.
@InProceedings{Erlang20p24,
author = {Boldizsár Poór and Melinda Toth and István Bozó},
title = {Transformations towards Clean Functional Code},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3406085.3409010},
year = {2020},
}
Publisher's Version
Erlang '20: "Machine-Checked Natural Semantics ..."
Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
This research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language.
In this paper, we present an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.
@InProceedings{Erlang20p1,
author = {Péter Bereczky and Dániel Horpácsi and Simon J. Thompson},
title = {Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3406085.3409008},
year = {2020},
}
Publisher's Version
Erlang '20: "Transformations towards Clean ..."
Transformations towards Clean Functional Code
Boldizsár Poór, Melinda Toth, and István Bozó
(Eötvös Loránd University, Hungary)
The programming style has an impact on the readability and comprehensibility of the source code, and it may also affect run-time performance. This statement also holds for functional languages when the functional style is mixed with imperative design. In this paper, we present a couple of methods that can refactor imperatively styled Erlang source-code into a more functionally styled one. This can be done by transforming unnecessary calls to length, hd and tl into pattern matching or by lifting particular nested expressions. The results of our investigations indicate that these refactorings can not only shorten the length of the source code but also affect the complexity/readability. In this paper, we present some refactorings; moreover, real-life examples and data for its validation.
@InProceedings{Erlang20p24,
author = {Boldizsár Poór and Melinda Toth and István Bozó},
title = {Transformations towards Clean Functional Code},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3406085.3409010},
year = {2020},
}
Publisher's Version
Erlang '20: "Teaching Practical Realistic ..."
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Peter Zeller, Annette Bieniusa, and Carla Ferreira
(TU Kaiserslautern, Germany; Nova University of Lisbon, Portugal)
Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.
In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.
@InProceedings{Erlang20p14,
author = {Peter Zeller and Annette Bieniusa and Carla Ferreira},
title = {Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3406085.3409009},
year = {2020},
}
Publisher's Version