Short Bio

Doriana Medić is a Computer Science research fellow at the University of Turin.
She obtained her Ph.D. degree in Computer Science and Systems Engineering at IMT School for Advanced Studies Lucca with a thesis on the expressiveness of calculi for reversible concurrency.

Her research focuses on the interplay between formal methods, concurrent, distributed and reversible computing. More recently, here interests are in federated learning.

Publications

2021

• I. Lanese, D. Medic, and C. A. Mezzina, “Static versus dynamic reversibility in CCS,” Acta informatica, vol. 58, pp. 1-34, 2021. doi:10.1007/s00236-019-00346-6
  [BibTeX] [Abstract] [Download PDF]
  

  The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism.

  @article{21:journals:LaneseMM21,
  title = {Static versus dynamic reversibility in {CCS}},
  journal = {Acta Informatica},
  volume = {58},
  pages = {1-34},
  year = {2021},
  doi = {10.1007/s00236-019-00346-6},
  url = {https://doi.org/10.1007/s00236-019-00346-6},
  author = {Ivan Lanese and Doriana Medic and Claudio Antares Mezzina},
  keywords = {reversibility, encoding, RCCS, CCSK, isomorphism},
  abstract = {The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism.}
  }

• C. Aubert and D. Medic, “Explicit identifiers and contexts in reversible concurrent calculus,” in Reversible computation – 13th international conference, RC 2021, virtual event, july 7-8, 2021, proceedings, 2021. doi:10.1007/978-3-030-79837-6_9
  [BibTeX] [Abstract] [Download PDF]
  

  Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions usual in ?forward-only? process algebras, such as replication or context. Existing formalisms disallow the ?hot-plugging? of processes during their execution in contexts with their own past. They also assume the existence of ?eternally fresh? keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ?reversible? contexts.

  @inproceedings{21:RC:AubertM21,
  abstract = {Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions usual in ?forward-only? process algebras, such as replication or context. Existing formalisms disallow the ?hot-plugging? of processes during their execution in contexts with their own past. They also assume the existence of ?eternally fresh? keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ?reversible? contexts.},
  author = {Cl{\'{e}}ment Aubert and Doriana Medic},
  booktitle = {Reversible Computation - 13th International Conference, {RC} 2021, Virtual Event, July 7-8, 2021, Proceedings},
  doi = {10.1007/978-3-030-79837-6\_9},
  keywords = {Formal semantics, process algebras and calculi, context for reversible calculi},
  publisher = {Springer},
  title = {Explicit Identifiers and Contexts in Reversible Concurrent Calculus},
  url = {https://doi.org/10.1007/978-3-030-79837-6\_9},
  year = {2021}
  }

2020

• D. Medic, C. A. Mezzina, I. Phillips, and N. Yoshida, “A parametric framework for reversible \emph\(\pi\)-calculi,” Information and computation, vol. 275, p. 104644, 2020. doi:10.1016/j.ic.2020.104644
  [BibTeX] [Abstract] [Download PDF]
  

  This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in ?-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible ?-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible \emph{{\(\pi\)}}-calculus causal semantics.

  @article{20:journals:MedicMPY20,
  author = {Doriana Medic and
  Claudio Antares Mezzina and
  Iain Phillips and
  Nobuko Yoshida},
  title = {A parametric framework for reversible \emph{{\(\pi\)}}-calculi},
  journal = {Information and Computation},
  volume = {275},
  pages = {104644},
  year = {2020},
  url = {https://doi.org/10.1016/j.ic.2020.104644},
  doi = {10.1016/j.ic.2020.104644},
  abstract = {This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in ?-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible ?-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible \emph{{\(\pi\)}}-calculus causal semantics.},
  keywords = {Causal semantics, \emph{{\(\pi\)}}-Calculus, Causally-consistent reversibility}
  }

• I. Lanese and D. Medic, “A general approach to derive uncontrolled reversible semantics,” in 31st international conference on concurrency theory, CONCUR 2020, september 1-4, 2020, vienna, austria (virtual conference), 2020, p. 33:1–33:24. doi:10.4230/LIPIcs.CONCUR.2020.33
  [BibTeX] [Abstract] [Download PDF]
  

  Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone. This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order ?-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.

  @inproceedings{20:concur:LaneseM20,
  author = {Ivan Lanese and
  Doriana Medic},
  title = {A General Approach to Derive Uncontrolled Reversible Semantics},
  booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020,
  September 1-4, 2020, Vienna, Austria (Virtual Conference)},
  series = {LIPIcs},
  volume = {171},
  pages = {33:1--33:24},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year = {2020},
  url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.33},
  doi = {10.4230/LIPIcs.CONCUR.2020.33},
  abstract = {Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone.
  This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order ?-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.},
  keywords = {Reversible computing, causality, process calculi, Erlang}
  }

• D. Medic, C. A. Mezzina, I. Phillips, and N. Yoshida, “Towards a formal account for software transactional memory,” in Reversible computation – 12th international conference, RC 2020, oslo, norway, july 9-10, 2020, proceedings, 2020, p. 255–263. doi:10.1007/978-3-030-52482-1_16
  [BibTeX] [Abstract] [Download PDF]
  

  Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.

  @inproceedings{20:RC:MedicM0Y20,
  author = {Doriana Medic and
  Claudio Antares Mezzina and
  Iain Phillips and
  Nobuko Yoshida},
  title = {Towards a Formal Account for Software Transactional Memory},
  booktitle = {Reversible Computation - 12th International Conference, {RC} 2020,
  Oslo, Norway, July 9-10, 2020, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {12227},
  pages = {255--263},
  publisher = {Springer},
  year = {2020},
  url = {https://doi.org/10.1007/978-3-030-52482-1\_16},
  doi = {10.1007/978-3-030-52482-1\_16},
  abstract = {Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.},
  keywords = {STM, transactions, concurrency}
  }

2019

• D. Medic, “Relative expressiveness of calculi for reversible concurrency,” Bull. EATCS, vol. 129, 2019.
  [BibTeX] [Abstract] [Download PDF]
  

  A number of formalisms have been proposed to model various approaches to reversibility and to better understand its properties and characteristics. However, the relation between these formalisms has hardly been studied. This paper examines the expressiveness of the causal-consistent reversibility in process algebras CCS and \emph{{\(\pi\)}}-calculus. In particular, we show, by means of encodings, that LTSs of two reversible extensions of CCS, Reversible CCS [1] and CCS with Keys [2], are isomorphic up to some structural transformations of processes. To study different causal semantics for ?-calculus, we devise a uniform framework for reversible \emph{{\(\pi\)}}-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Depending on the used data structure, different causal semantics can be obtained. We show that reversibility induced by our framework when instantiated with three different data structures is causally-consistent and prove a causal correspondence between certain causal semantics and matching instance of the framework.

  @article{19:eatcs:Medic19,
  author = {Doriana Medic},
  title = {Relative expressiveness of calculi for reversible concurrency},
  journal = {Bull. {EATCS}},
  volume = {129},
  year = {2019},
  url = {http://bulletin.eatcs.org/index.php/beatcs/article/view/590/601},
  abstract = {A number of formalisms have been proposed to model various approaches to reversibility and to better understand its properties and characteristics. However, the relation between these formalisms has hardly been studied. This paper examines the expressiveness of the causal-consistent reversibility in process algebras CCS and \emph{{\(\pi\)}}-calculus. In particular, we show, by means of encodings, that LTSs of two reversible extensions of CCS, Reversible CCS [1] and CCS with Keys [2], are isomorphic up to some structural transformations of processes. To study different causal semantics for ?-calculus, we devise a uniform framework for reversible \emph{{\(\pi\)}}-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Depending on the used data structure, different causal semantics can be obtained. We show that reversibility induced by our framework when instantiated with three different data structures is causally-consistent and prove a causal correspondence between certain causal semantics and matching instance of the framework.},
  }