Search Results

Documents authored by Melgratti, Hernán

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.17
Fair Join Pattern Matching for Actors

Authors: Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance. In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).
Cite as

Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Fair Join Pattern Matching for Actors. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 17:1-17:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haller_et_al:LIPIcs.ECOOP.2024.17,
  author =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Fair Join Pattern Matching for Actors}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{17:1--17:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.17},
  URN =		{urn:nbn:de:0030-drops-208663},
  doi =		{10.4230/LIPIcs.ECOOP.2024.17},
  annote =	{Keywords: Concurrency, join patterns, join calculus, actor model}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.8
Fair Join Pattern Matching for Actors (Artifact)

Authors: Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance. In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).
Cite as

Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Fair Join Pattern Matching for Actors (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{haller_et_al:DARTS.10.2.8,
  author =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Fair Join Pattern Matching for Actors (Artifact)}},
  pages =	{8:1--8:3},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.8},
  URN =		{urn:nbn:de:0030-drops-209062},
  doi =		{10.4230/DARTS.10.2.8},
  annote =	{Keywords: Concurrency, join patterns, join calculus, actor model}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.15
Behavioural Types for Local-First Software

Authors: Roland Kuhn, Hernán Melgratti, and Emilio Tuosto

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. Our model elaborates on the Actyx industrial platform and provides the basis for tool support: we sketch an implemented prototype which proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.
Cite as

Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kuhn_et_al:LIPIcs.ECOOP.2023.15,
  author =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  title =	{{Behavioural Types for Local-First Software}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.15},
  URN =		{urn:nbn:de:0030-drops-182086},
  doi =		{10.4230/LIPIcs.ECOOP.2023.15},
  annote =	{Keywords: Distributed coordination, local-first software, behavioural types, publish-subscribe, asynchronous communication}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.14
Behavioural Types for Local-First Software (Artifact)

Authors: Roland Kuhn, Hernán Melgratti, and Emilio Tuosto

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
This artifact supports the theory of swarm protocols presented in the related article. Specifically, following the top-down development typical of choreographic approaches, our artifact enables the specification of systems of peers communicating through an event notification mechanism from a global viewpoint which can then be projected to local specifications of peers, rendered as machines. To the best of our knowledge, ours is the first implementation of a behavioural type framework supporting the application of the principles of local-first software for network devices which collaborate on a common task while retaining full autonomy. The artifact can be integrated in the Actyx industrial platform; this proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.
Cite as

Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{kuhn_et_al:DARTS.9.2.14,
  author =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  title =	{{Behavioural Types for Local-First Software (Artifact)}},
  pages =	{14:1--14:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.14},
  URN =		{urn:nbn:de:0030-drops-182541},
  doi =		{10.4230/DARTS.9.2.14},
  annote =	{Keywords: Distributed coordination, local-first software, behavioural types, publish-subscribe, asynchronous communication}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.14
Probabilistic Analysis of Binary Sessions

Authors: Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.
Cite as

Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. Probabilistic Analysis of Binary Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{inverso_et_al:LIPIcs.CONCUR.2020.14,
  author =	{Inverso, Omar and Melgratti, Hern\'{a}n and Padovani, Luca and Trubiani, Catia and Tuosto, Emilio},
  title =	{{Probabilistic Analysis of Binary Sessions}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.14},
  URN =		{urn:nbn:de:0030-drops-128264},
  doi =		{10.4230/LIPIcs.CONCUR.2020.14},
  annote =	{Keywords: Probabilistic choices, session types, static analysis, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.42
A Categorical Account of Replicated Data Types

Authors: Fabio Gadducci, Hernán Melgratti, Christian Roldán, and Matteo Sammartino

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Replicated Data Types (RDTs) have been introduced as a suitable abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are commonly specified in terms of two relations: visibility, which accounts for the different views that a store may have, and arbitration, which states the logical order imposed on the operations executed over the store. Different flavours, e.g., operational, axiomatic and functional, have recently been proposed for the specification of RDTs. In this work, we propose an algebraic characterisation of RDT specifications. We define categories of visibility relations and arbitrations, show the existence of relevant limits and colimits, and characterize RDT specifications as functors between such categories that preserve these additional structures.
Cite as

Fabio Gadducci, Hernán Melgratti, Christian Roldán, and Matteo Sammartino. A Categorical Account of Replicated Data Types. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 42:1-42:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gadducci_et_al:LIPIcs.FSTTCS.2019.42,
  author =	{Gadducci, Fabio and Melgratti, Hern\'{a}n and Rold\'{a}n, Christian and Sammartino, Matteo},
  title =	{{A Categorical Account of Replicated Data Types}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{42:1--42:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.42},
  URN =		{urn:nbn:de:0030-drops-116042},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.42},
  annote =	{Keywords: Replicated data type, Specification, Functorial characterisation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact