AGERE '21: "Session Types in Elixir ..."
Session Types in Elixir
Gerard Tabone and Adrian Francalanza
(University of Malta, Malta)
This paper proposes an adaptation of session types to provide behavioural information about public functions in Elixir modules. We formalise typechecking rules for the main constructs of the language. This allows us to statically determine whether a function implementation observes its session endpoint specification. Based on this type system, we then construct a tool that automates typechecking for Elixir modules.
@InProceedings{AGERE21p12,
author = {Gerard Tabone and Adrian Francalanza},
title = {Session Types in Elixir},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {12--23},
doi = {10.1145/3486601.3486708},
year = {2021},
}
Publisher's Version
AGERE '21: "What’s the Problem? Interrogating ..."
What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs
Carmen Torres Lopez, Louise Van Verre, and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium)
Programs written using Communicating Event-Loops (CEL) concurrency model do not suffer from low-level data races by design but are not exempt from other concurrency bugs, such as behavioral deadlocks and message order violations.
When programmers need to find the root cause of a bug, they typically ask questions about the application's behavior. However, current debugging tools are mostly operational, offering features at the source code level like breakpoints and watchpoints. Consequently, understanding the program behavior when debugging can take a lot of time for developers since questions on behaviors need to be mapped into operations in the debugger.
Inspired by interrogative debugging, this paper proposes an interactive debugging approach for actor-based programs that enable developers to reason about the program output by selecting questions from a set of predefined questions about the code and the program's execution. We present the design of the questions and answers, and we describe a prototype implementation in Apgar, an online debugger for actor-based programs written in SOMns. We define questions based on key concepts of the actor model: actors, turns, messages, and promises. The debugger then computes the answers by analyzing a recorded trace of events about the program execution.
@InProceedings{AGERE21p24,
author = {Carmen Torres Lopez and Louise Van Verre and Elisa Gonzalez Boix},
title = {What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {24--36},
doi = {10.1145/3486601.3486709},
year = {2021},
}
Publisher's Version
AGERE '21: "Contract-Based Return-Value ..."
Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions
Tim Soethout, Tijs van der Storm, and Jurgen J. Vinju
(ING Bank, Netherlands; CWI, Netherlands; University of Groningen, Netherlands; Eindhoven University of Technology, Netherlands)
A key challenge of designing distributed software systems is maintaining data consistency. We can define data consistency and data isolation guarantees --e.g. serializability-- in terms of schedules of atomic reads and writes, but this excludes schedules that would be semantically consistent. Others use manually provided information on "non-conflicting operations" to define guarantees that work for more applications allowing more parallel schedules. To be safe, an engineer might avoid marking operations as non-conflicting, with detrimental effects to efficiency. To be fast, they might mark more non-conflicting operations than is strictly safe.
Our goal is to help engineers by automatically deriving commutative operations (using their respective contracts) such that more parallel schedules with global consistency are possible. We define a new general consistency and isolation guarantee named "Return-Value Serializability" to check consistency claims automatically, and we present distributed event processing algorithms that make use of the same "Contract-based Commutativity" information. We validated both the definitions and the algorithms using model-checking with TLA+. Previous work provided evidence that local coordination avoidance such as applied here has a significant positive effect on the performance of distributed transaction systems.
Client-centric return-value commutativity promises to hit a sweet spot in design trade-offs for business applications, such as payment systems, that must scale-out while their operations are not embarrassingly parallel and consistency guarantees are of the highest priority. It can also provide design feedback, indicating that some operations will simply not scale together even before a line of code has been written.
@InProceedings{AGERE21p1,
author = {Tim Soethout and Tijs van der Storm and Jurgen J. Vinju},
title = {Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486601.3486707},
year = {2021},
}
Publisher's Version
AGERE '21: "Session Types in Elixir ..."
Session Types in Elixir
Gerard Tabone and Adrian Francalanza
(University of Malta, Malta)
This paper proposes an adaptation of session types to provide behavioural information about public functions in Elixir modules. We formalise typechecking rules for the main constructs of the language. This allows us to statically determine whether a function implementation observes its session endpoint specification. Based on this type system, we then construct a tool that automates typechecking for Elixir modules.
@InProceedings{AGERE21p12,
author = {Gerard Tabone and Adrian Francalanza},
title = {Session Types in Elixir},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {12--23},
doi = {10.1145/3486601.3486708},
year = {2021},
}
Publisher's Version
AGERE '21: "What’s the Problem? Interrogating ..."
What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs
Carmen Torres Lopez, Louise Van Verre, and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium)
Programs written using Communicating Event-Loops (CEL) concurrency model do not suffer from low-level data races by design but are not exempt from other concurrency bugs, such as behavioral deadlocks and message order violations.
When programmers need to find the root cause of a bug, they typically ask questions about the application's behavior. However, current debugging tools are mostly operational, offering features at the source code level like breakpoints and watchpoints. Consequently, understanding the program behavior when debugging can take a lot of time for developers since questions on behaviors need to be mapped into operations in the debugger.
Inspired by interrogative debugging, this paper proposes an interactive debugging approach for actor-based programs that enable developers to reason about the program output by selecting questions from a set of predefined questions about the code and the program's execution. We present the design of the questions and answers, and we describe a prototype implementation in Apgar, an online debugger for actor-based programs written in SOMns. We define questions based on key concepts of the actor model: actors, turns, messages, and promises. The debugger then computes the answers by analyzing a recorded trace of events about the program execution.
@InProceedings{AGERE21p24,
author = {Carmen Torres Lopez and Louise Van Verre and Elisa Gonzalez Boix},
title = {What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {24--36},
doi = {10.1145/3486601.3486709},
year = {2021},
}
Publisher's Version
AGERE '21: "Contract-Based Return-Value ..."
Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions
Tim Soethout, Tijs van der Storm, and Jurgen J. Vinju
(ING Bank, Netherlands; CWI, Netherlands; University of Groningen, Netherlands; Eindhoven University of Technology, Netherlands)
A key challenge of designing distributed software systems is maintaining data consistency. We can define data consistency and data isolation guarantees --e.g. serializability-- in terms of schedules of atomic reads and writes, but this excludes schedules that would be semantically consistent. Others use manually provided information on "non-conflicting operations" to define guarantees that work for more applications allowing more parallel schedules. To be safe, an engineer might avoid marking operations as non-conflicting, with detrimental effects to efficiency. To be fast, they might mark more non-conflicting operations than is strictly safe.
Our goal is to help engineers by automatically deriving commutative operations (using their respective contracts) such that more parallel schedules with global consistency are possible. We define a new general consistency and isolation guarantee named "Return-Value Serializability" to check consistency claims automatically, and we present distributed event processing algorithms that make use of the same "Contract-based Commutativity" information. We validated both the definitions and the algorithms using model-checking with TLA+. Previous work provided evidence that local coordination avoidance such as applied here has a significant positive effect on the performance of distributed transaction systems.
Client-centric return-value commutativity promises to hit a sweet spot in design trade-offs for business applications, such as payment systems, that must scale-out while their operations are not embarrassingly parallel and consistency guarantees are of the highest priority. It can also provide design feedback, indicating that some operations will simply not scale together even before a line of code has been written.
@InProceedings{AGERE21p1,
author = {Tim Soethout and Tijs van der Storm and Jurgen J. Vinju},
title = {Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486601.3486707},
year = {2021},
}
Publisher's Version
AGERE '21: "What’s the Problem? Interrogating ..."
What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs
Carmen Torres Lopez, Louise Van Verre, and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium)
Programs written using Communicating Event-Loops (CEL) concurrency model do not suffer from low-level data races by design but are not exempt from other concurrency bugs, such as behavioral deadlocks and message order violations.
When programmers need to find the root cause of a bug, they typically ask questions about the application's behavior. However, current debugging tools are mostly operational, offering features at the source code level like breakpoints and watchpoints. Consequently, understanding the program behavior when debugging can take a lot of time for developers since questions on behaviors need to be mapped into operations in the debugger.
Inspired by interrogative debugging, this paper proposes an interactive debugging approach for actor-based programs that enable developers to reason about the program output by selecting questions from a set of predefined questions about the code and the program's execution. We present the design of the questions and answers, and we describe a prototype implementation in Apgar, an online debugger for actor-based programs written in SOMns. We define questions based on key concepts of the actor model: actors, turns, messages, and promises. The debugger then computes the answers by analyzing a recorded trace of events about the program execution.
@InProceedings{AGERE21p24,
author = {Carmen Torres Lopez and Louise Van Verre and Elisa Gonzalez Boix},
title = {What’s the Problem? Interrogating Actors to Identify the Root Cause of Concurrency Bugs},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {24--36},
doi = {10.1145/3486601.3486709},
year = {2021},
}
Publisher's Version
AGERE '21: "Contract-Based Return-Value ..."
Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions
Tim Soethout, Tijs van der Storm, and Jurgen J. Vinju
(ING Bank, Netherlands; CWI, Netherlands; University of Groningen, Netherlands; Eindhoven University of Technology, Netherlands)
A key challenge of designing distributed software systems is maintaining data consistency. We can define data consistency and data isolation guarantees --e.g. serializability-- in terms of schedules of atomic reads and writes, but this excludes schedules that would be semantically consistent. Others use manually provided information on "non-conflicting operations" to define guarantees that work for more applications allowing more parallel schedules. To be safe, an engineer might avoid marking operations as non-conflicting, with detrimental effects to efficiency. To be fast, they might mark more non-conflicting operations than is strictly safe.
Our goal is to help engineers by automatically deriving commutative operations (using their respective contracts) such that more parallel schedules with global consistency are possible. We define a new general consistency and isolation guarantee named "Return-Value Serializability" to check consistency claims automatically, and we present distributed event processing algorithms that make use of the same "Contract-based Commutativity" information. We validated both the definitions and the algorithms using model-checking with TLA+. Previous work provided evidence that local coordination avoidance such as applied here has a significant positive effect on the performance of distributed transaction systems.
Client-centric return-value commutativity promises to hit a sweet spot in design trade-offs for business applications, such as payment systems, that must scale-out while their operations are not embarrassingly parallel and consistency guarantees are of the highest priority. It can also provide design feedback, indicating that some operations will simply not scale together even before a line of code has been written.
@InProceedings{AGERE21p1,
author = {Tim Soethout and Tijs van der Storm and Jurgen J. Vinju},
title = {Contract-Based Return-Value Commutativity: Safely Exploiting Contract-Based Commutativity for Faster Serializable Transactions},
booktitle = {Proc.\ AGERE},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486601.3486707},
year = {2021},
}
Publisher's Version