Erlang '23: "TLS the Erlang/OTP Way (Experience ..."
TLS the Erlang/OTP Way (Experience Report)
Ingela Anderton Andin, Raimo Niskanen, Péter Dimitrov, and Kiko Fernandez-Reyes
(Ericsson, Sweden)
The Transport Layer Security (TLS) protocol is one of the most used protocols to ensure data privacy, integrity and authenticity on the Internet. Erlang/OTP's TLS implementation is widely used in industry, and especially in the telecommunication sector.
This paper describes an overview of the TLS protocol in the context of Erlang. We explain Erlang/OTP's TLS protocol design and implementation, optimizations, a benchmark evaluation of the Erlang TLS protocol implementation against previous Erlang/OTP's TLS implementations, and a benchmark comparison against the Go's TLS implementation.
@InProceedings{Erlang23p2,
author = {Ingela Anderton Andin and Raimo Niskanen and Péter Dimitrov and Kiko Fernandez-Reyes},
title = {TLS the Erlang/OTP Way (Experience Report)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3609022.3609414},
year = {2023},
}
Publisher's Version
Erlang '23: "Generation and Refinement ..."
Generation and Refinement of Testing Models
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
@InProceedings{Erlang23p14,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Generation and Refinement of Testing Models},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3609022.3609415},
year = {2023},
}
Publisher's Version
Erlang '23: "Generation and Refinement ..."
Generation and Refinement of Testing Models
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
@InProceedings{Erlang23p14,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Generation and Refinement of Testing Models},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3609022.3609415},
year = {2023},
}
Publisher's Version
Erlang '23: "TLS the Erlang/OTP Way (Experience ..."
TLS the Erlang/OTP Way (Experience Report)
Ingela Anderton Andin, Raimo Niskanen, Péter Dimitrov, and Kiko Fernandez-Reyes
(Ericsson, Sweden)
The Transport Layer Security (TLS) protocol is one of the most used protocols to ensure data privacy, integrity and authenticity on the Internet. Erlang/OTP's TLS implementation is widely used in industry, and especially in the telecommunication sector.
This paper describes an overview of the TLS protocol in the context of Erlang. We explain Erlang/OTP's TLS protocol design and implementation, optimizations, a benchmark evaluation of the Erlang TLS protocol implementation against previous Erlang/OTP's TLS implementations, and a benchmark comparison against the Go's TLS implementation.
@InProceedings{Erlang23p2,
author = {Ingela Anderton Andin and Raimo Niskanen and Péter Dimitrov and Kiko Fernandez-Reyes},
title = {TLS the Erlang/OTP Way (Experience Report)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3609022.3609414},
year = {2023},
}
Publisher's Version
Erlang '23: "Mria: An Eventually Consistent ..."
Mria: An Eventually Consistent Mnesia
Dmitrii Fedoseev, Serhii Tupchii, Thales Macedo Garitezi, and Zaiming Shi
(EMQ Technologies, Sweden; EMQ Technologies, Ukraine; EMQ Technologies, Brazil)
Mnesia, an Erlang distributed database, serves as an embedded storage and replication layer for OTP applications requiring low read latency and high availability. EMQX is a publish-subscribe message broker supporting the MQTT protocol that uses Mnesia to replicate its internal state across the cluster. We analyze the limitations of Mnesia's replication protocol scalability in large clusters under high load. To address these limitations, we developed Mria, an extension to the Mnesia database that provides eventual consistency within a cluster and achieves better horizontal scalability. We validated Mria using a variety of testing techniques, including model checking, chaos engineering, and formal verification. Replacing Mnesia with Mria allowed us to scale the EMQX cluster to 23 nodes, handle 100 million simultaneous client sessions and achieve a higher sustained load.
@InProceedings{Erlang23p24,
author = {Dmitrii Fedoseev and Serhii Tupchii and Thales Macedo Garitezi and Zaiming Shi},
title = {Mria: An Eventually Consistent Mnesia},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3609022.3609416},
year = {2023},
}
Publisher's Version
Erlang '23: "A Semantics of Core Erlang ..."
A Semantics of Core Erlang with Handling of Signals
Aurélie Kong Win Chang, Jérôme Feret, and Gregor Gössler
(Inria, France; University Grenoble Alpes, France; CNRS, France; Grenoble INP, France; LIG, France; ENS, France; PSL University, France)
We introduce a small step semantics for a subset of Core Erlang modeling its monitoring and signal systems. The goal of our semantics is to enable the construction of causal explanations for property violations, which will be the object of future work. As a first axis of reflection, we chose to study the impact of the order of messages on a faulty behavior. We present our semantics and discuss some of our design choices. This work is a part of a broader project on causal debugging of concurrent programs in Erlang.
@InProceedings{Erlang23p31,
author = {Aurélie Kong Win Chang and Jérôme Feret and Gregor Gössler},
title = {A Semantics of Core Erlang with Handling of Signals},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {31--38},
doi = {10.1145/3609022.3609417},
year = {2023},
}
Publisher's Version
Erlang '23: "TLS the Erlang/OTP Way (Experience ..."
TLS the Erlang/OTP Way (Experience Report)
Ingela Anderton Andin, Raimo Niskanen, Péter Dimitrov, and Kiko Fernandez-Reyes
(Ericsson, Sweden)
The Transport Layer Security (TLS) protocol is one of the most used protocols to ensure data privacy, integrity and authenticity on the Internet. Erlang/OTP's TLS implementation is widely used in industry, and especially in the telecommunication sector.
This paper describes an overview of the TLS protocol in the context of Erlang. We explain Erlang/OTP's TLS protocol design and implementation, optimizations, a benchmark evaluation of the Erlang TLS protocol implementation against previous Erlang/OTP's TLS implementations, and a benchmark comparison against the Go's TLS implementation.
@InProceedings{Erlang23p2,
author = {Ingela Anderton Andin and Raimo Niskanen and Péter Dimitrov and Kiko Fernandez-Reyes},
title = {TLS the Erlang/OTP Way (Experience Report)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3609022.3609414},
year = {2023},
}
Publisher's Version
Erlang '23: "Generation and Refinement ..."
Generation and Refinement of Testing Models
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
@InProceedings{Erlang23p14,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Generation and Refinement of Testing Models},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3609022.3609415},
year = {2023},
}
Publisher's Version
Erlang '23: "Mria: An Eventually Consistent ..."
Mria: An Eventually Consistent Mnesia
Dmitrii Fedoseev, Serhii Tupchii, Thales Macedo Garitezi, and Zaiming Shi
(EMQ Technologies, Sweden; EMQ Technologies, Ukraine; EMQ Technologies, Brazil)
Mnesia, an Erlang distributed database, serves as an embedded storage and replication layer for OTP applications requiring low read latency and high availability. EMQX is a publish-subscribe message broker supporting the MQTT protocol that uses Mnesia to replicate its internal state across the cluster. We analyze the limitations of Mnesia's replication protocol scalability in large clusters under high load. To address these limitations, we developed Mria, an extension to the Mnesia database that provides eventual consistency within a cluster and achieves better horizontal scalability. We validated Mria using a variety of testing techniques, including model checking, chaos engineering, and formal verification. Replacing Mnesia with Mria allowed us to scale the EMQX cluster to 23 nodes, handle 100 million simultaneous client sessions and achieve a higher sustained load.
@InProceedings{Erlang23p24,
author = {Dmitrii Fedoseev and Serhii Tupchii and Thales Macedo Garitezi and Zaiming Shi},
title = {Mria: An Eventually Consistent Mnesia},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3609022.3609416},
year = {2023},
}
Publisher's Version
Erlang '23: "A Semantics of Core Erlang ..."
A Semantics of Core Erlang with Handling of Signals
Aurélie Kong Win Chang, Jérôme Feret, and Gregor Gössler
(Inria, France; University Grenoble Alpes, France; CNRS, France; Grenoble INP, France; LIG, France; ENS, France; PSL University, France)
We introduce a small step semantics for a subset of Core Erlang modeling its monitoring and signal systems. The goal of our semantics is to enable the construction of causal explanations for property violations, which will be the object of future work. As a first axis of reflection, we chose to study the impact of the order of messages on a faulty behavior. We present our semantics and discuss some of our design choices. This work is a part of a broader project on causal debugging of concurrent programs in Erlang.
@InProceedings{Erlang23p31,
author = {Aurélie Kong Win Chang and Jérôme Feret and Gregor Gössler},
title = {A Semantics of Core Erlang with Handling of Signals},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {31--38},
doi = {10.1145/3609022.3609417},
year = {2023},
}
Publisher's Version
Erlang '23: "Generation and Refinement ..."
Generation and Refinement of Testing Models
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
@InProceedings{Erlang23p14,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Generation and Refinement of Testing Models},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3609022.3609415},
year = {2023},
}
Publisher's Version
Erlang '23: "A Semantics of Core Erlang ..."
A Semantics of Core Erlang with Handling of Signals
Aurélie Kong Win Chang, Jérôme Feret, and Gregor Gössler
(Inria, France; University Grenoble Alpes, France; CNRS, France; Grenoble INP, France; LIG, France; ENS, France; PSL University, France)
We introduce a small step semantics for a subset of Core Erlang modeling its monitoring and signal systems. The goal of our semantics is to enable the construction of causal explanations for property violations, which will be the object of future work. As a first axis of reflection, we chose to study the impact of the order of messages on a faulty behavior. We present our semantics and discuss some of our design choices. This work is a part of a broader project on causal debugging of concurrent programs in Erlang.
@InProceedings{Erlang23p31,
author = {Aurélie Kong Win Chang and Jérôme Feret and Gregor Gössler},
title = {A Semantics of Core Erlang with Handling of Signals},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {31--38},
doi = {10.1145/3609022.3609417},
year = {2023},
}
Publisher's Version
Erlang '23: "Code Analysis at WhatsApp ..."
Code Analysis at WhatsApp (Keynote)
Ke Mao
(Meta, UK)
In the ever-evolving world of software development, code analysis stands as a critical component for quality and efficiency. This keynote will present an overview of code analysis tools at WhatsApp, and then delve into the techniques of dynamic and static analysis, with examples of their industrial deployments. The keynote will discuss the integration of code analysis into early stages of the software development life cycle, from continuous integration pipelines to DevOps practices.
@InProceedings{Erlang23p1,
author = {Ke Mao},
title = {Code Analysis at WhatsApp (Keynote)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3609022.3615585},
year = {2023},
}
Publisher's Version
Erlang '23: "Generation and Refinement ..."
Generation and Refinement of Testing Models
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
Writing property-based testing models is a challenging task. This article introduces a new tool, Faktory, which is capable of automatically generating an executable property-based testing model from less complicated sources: normal function type specifications, and traditional function calling contracts using pre- and post-conditions. Concretely, Faktory is an Elixir library which from an API annotated with executable calling contracts written using the Corsa contract checking library, automatically generates a property-based testing model in the form of a state machine implemented using the Makina state machine DSL. In the article we illustrate the functionalities of the Faktory tool using a number of examples. The first one shows how to test a functional data structure; the second shows how to improve test-case generation by reusing test results; and in the third example a stateful key-value storage is tested by first deriving an initial test model using Faktory, and then refining the generated model using the Makina model/state machine extension mechanism.
@InProceedings{Erlang23p14,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Generation and Refinement of Testing Models},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {14--23},
doi = {10.1145/3609022.3609415},
year = {2023},
}
Publisher's Version
Erlang '23: "TLS the Erlang/OTP Way (Experience ..."
TLS the Erlang/OTP Way (Experience Report)
Ingela Anderton Andin, Raimo Niskanen, Péter Dimitrov, and Kiko Fernandez-Reyes
(Ericsson, Sweden)
The Transport Layer Security (TLS) protocol is one of the most used protocols to ensure data privacy, integrity and authenticity on the Internet. Erlang/OTP's TLS implementation is widely used in industry, and especially in the telecommunication sector.
This paper describes an overview of the TLS protocol in the context of Erlang. We explain Erlang/OTP's TLS protocol design and implementation, optimizations, a benchmark evaluation of the Erlang TLS protocol implementation against previous Erlang/OTP's TLS implementations, and a benchmark comparison against the Go's TLS implementation.
@InProceedings{Erlang23p2,
author = {Ingela Anderton Andin and Raimo Niskanen and Péter Dimitrov and Kiko Fernandez-Reyes},
title = {TLS the Erlang/OTP Way (Experience Report)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3609022.3609414},
year = {2023},
}
Publisher's Version
Erlang '23: "Mria: An Eventually Consistent ..."
Mria: An Eventually Consistent Mnesia
Dmitrii Fedoseev, Serhii Tupchii, Thales Macedo Garitezi, and Zaiming Shi
(EMQ Technologies, Sweden; EMQ Technologies, Ukraine; EMQ Technologies, Brazil)
Mnesia, an Erlang distributed database, serves as an embedded storage and replication layer for OTP applications requiring low read latency and high availability. EMQX is a publish-subscribe message broker supporting the MQTT protocol that uses Mnesia to replicate its internal state across the cluster. We analyze the limitations of Mnesia's replication protocol scalability in large clusters under high load. To address these limitations, we developed Mria, an extension to the Mnesia database that provides eventual consistency within a cluster and achieves better horizontal scalability. We validated Mria using a variety of testing techniques, including model checking, chaos engineering, and formal verification. Replacing Mnesia with Mria allowed us to scale the EMQX cluster to 23 nodes, handle 100 million simultaneous client sessions and achieve a higher sustained load.
@InProceedings{Erlang23p24,
author = {Dmitrii Fedoseev and Serhii Tupchii and Thales Macedo Garitezi and Zaiming Shi},
title = {Mria: An Eventually Consistent Mnesia},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3609022.3609416},
year = {2023},
}
Publisher's Version
Erlang '23: "Mria: An Eventually Consistent ..."
Mria: An Eventually Consistent Mnesia
Dmitrii Fedoseev, Serhii Tupchii, Thales Macedo Garitezi, and Zaiming Shi
(EMQ Technologies, Sweden; EMQ Technologies, Ukraine; EMQ Technologies, Brazil)
Mnesia, an Erlang distributed database, serves as an embedded storage and replication layer for OTP applications requiring low read latency and high availability. EMQX is a publish-subscribe message broker supporting the MQTT protocol that uses Mnesia to replicate its internal state across the cluster. We analyze the limitations of Mnesia's replication protocol scalability in large clusters under high load. To address these limitations, we developed Mria, an extension to the Mnesia database that provides eventual consistency within a cluster and achieves better horizontal scalability. We validated Mria using a variety of testing techniques, including model checking, chaos engineering, and formal verification. Replacing Mnesia with Mria allowed us to scale the EMQX cluster to 23 nodes, handle 100 million simultaneous client sessions and achieve a higher sustained load.
@InProceedings{Erlang23p24,
author = {Dmitrii Fedoseev and Serhii Tupchii and Thales Macedo Garitezi and Zaiming Shi},
title = {Mria: An Eventually Consistent Mnesia},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24--30},
doi = {10.1145/3609022.3609416},
year = {2023},
}
Publisher's Version