Doriana Medić

Assistant Professor (RTDA)
Alpha Research Group (Parallel Computing)
University of Turin, Computer Science Dept.
Via Pessinetto 12, 10149 Torino – Italy 
Email: doriana.medic@unito.it

Short Bio

Doriana Medić is a Computer Science Assistant Professor (RTDA) 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 and workflow modeling.

Research Projects

  • Space Center of Excellence (EC HE, HORIZON-EUROHPC-JU-2021-COE-01): Scalable Parallel and distributed Astrophysical Codes for Exascale (2023, 48 months, total cost 8M€, G.A. n. 101093441).
  • European Pilot (EC H2020 RIA, EuroHPC-02-2020, 42 months, total cost 30M€, G.A. n. 101034126).
  • EUPEX (EC H2020 RIA, EuroHPC-02-2020): European Pilot for Exascale (2021, 48 months, total cost 41M€, G.A. n. 101033975).

Publications

2023

  • M. Aldinucci, E. M. Baralis, V. Cardellini, I. Colonnelli, M. Danelutto, S. Decherchi, G. D. Modica, L. Ferrucci, M. Gribaudo, F. Iannone, M. Lapegna, D. Medic, G. Muscianisi, F. Righetti, E. Sciacca, N. Tonellotto, M. Tortonesi, P. Trunfio, and T. Vardanega, “A Systematic Mapping Study of Italian Research on Workflows,” in Proceedings of the SC ’23 Workshops of The International Conference on High Performance Computing, Network, Storage, and Analysis, SC-W 2023, Denver, CO, USA, 2023, p. 2065–2076. doi:10.1145/3624062.3624285
    [BibTeX] [Abstract] [Download PDF]

    An entire ecosystem of methodologies and tools revolves around scientific workflow management. They cover crucial non-functional requirements that standard workflow models fail to target, such as interactive execution, energy efficiency, performance portability, Big Data management, and intelligent orchestration in the Computing Continuum. Characterizing and monitoring this ecosystem is crucial to develop an informed view of current and future research directions. This work conducts a systematic mapping study of the Italian workflow research community, collecting and analyzing 25 tools and 10 applications from several scientific domains in the context of the “National Research Centre for HPC, Big Data, and Quantum Computing” (ICSC). The study aims to outline the main current research directions and determine how they address the critical needs of modern scientific applications. The findings highlight a variegated research ecosystem of tools, with a prominent interest in advanced workflow orchestration and still immature but promising efforts toward energy efficiency.

    @inproceedings{WORKS2023,
    title = {A Systematic Mapping Study of Italian Research on Workflows},
    author = {Marco Aldinucci and Elena Maria Baralis and Valeria Cardellini and Iacopo Colonnelli and Marco Danelutto and Sergio Decherchi and Giuseppe Di Modica and Luca Ferrucci and Marco Gribaudo and Francesco Iannone and Marco Lapegna and Doriana Medic and Giuseppa Muscianisi and Francesca Righetti and Eva Sciacca and Nicola Tonellotto and Mauro Tortonesi and Paolo Trunfio and Tullio Vardanega},
    year = {2023},
    month = nov,
    booktitle = {Proceedings of the {SC} '23 Workshops of The International Conference on High Performance Computing, Network, Storage, and Analysis, {SC-W} 2023},
    publisher = {{ACM}},
    address = {Denver, CO, USA},
    pages = {2065--2076},
    doi = {10.1145/3624062.3624285},
    abstract = {An entire ecosystem of methodologies and tools revolves around scientific workflow management. They cover crucial non-functional requirements that standard workflow models fail to target, such as interactive execution, energy efficiency, performance portability, Big Data management, and intelligent orchestration in the Computing Continuum. Characterizing and monitoring this ecosystem is crucial to develop an informed view of current and future research directions. This work conducts a systematic mapping study of the Italian workflow research community, collecting and analyzing 25 tools and 10 applications from several scientific domains in the context of the ``National Research Centre for HPC, Big Data, and Quantum Computing'' (ICSC). The study aims to outline the main current research directions and determine how they address the critical needs of modern scientific applications. The findings highlight a variegated research ecosystem of tools, with a prominent interest in advanced workflow orchestration and still immature but promising efforts toward energy efficiency.},
    keywords = {streamflow, jupyter-workflow, icsc},
    url = {https://doi.org/10.1145/3624062.3624285}
    }

  • D. Medić and M. Aldinucci, “Towards formal model for location aware workflows,” in 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023, Torino, Italy, 2023, p. 1864–1869. doi:10.1109/COMPSAC57700.2023.00289
    [BibTeX] [Abstract] [Download PDF]

    Designing complex applications and executing them on large-scale topologies of heterogeneous architectures is becoming increasingly crucial in many scientific domains. As a result, diverse workflow modelling paradigms are developed, most of them with no formalisation provided. In these circumstances, comparing two different models or switching from one system to the other becomes a hard nut to crack. This paper investigates the capability of process algebra to model a location aware workflow system. Distributed $\pi$-calculus is considered as the base of the formal model due to its ability to describe the communicating components that change their structure as an outcome of the communication. Later, it is discussed how the base model could be extended or modified to capture different features of location aware workflow system. The intention of this paper is to highlight the fact that due to its flexibility, $\pi$-calculus, could be a good candidate to represent the behavioural perspective of the workflow system.

    @inproceedings{23:medic:formal-model,
    title = {Towards formal model for location aware workflows},
    author = {Doriana Medi\'{c} and Marco Aldinucci},
    year = {2023},
    booktitle = {47th {IEEE} Annual Computers, Software, and Applications Conference, {COMPSAC} 2023},
    publisher = {{IEEE}},
    address = {Torino, Italy},
    pages = {1864--1869},
    doi = {10.1109/COMPSAC57700.2023.00289},
    abstract = {Designing complex applications and executing them on large-scale topologies of heterogeneous architectures is becoming increasingly crucial in many scientific domains. As a result, diverse workflow modelling paradigms are developed, most of them with no formalisation provided. In these circumstances, comparing two different models or switching from one system to the other becomes a hard nut to crack. This paper investigates the capability of process algebra to model a location aware workflow system. Distributed $\pi$-calculus is considered as the base of the formal model due to its ability to describe the communicating components that change their structure as an outcome of the communication. Later, it is discussed how the base model could be extended or modified to capture different features of location aware workflow system. The intention of this paper is to highlight the fact that due to its flexibility, $\pi$-calculus, could be a good candidate to represent the behavioural perspective of the workflow system.},
    editor = {Hossain Shahriar and Yuuichi Teranishi and Alfredo Cuzzocrea and Moushumi Sharmin and Dave Towey and A. K. M. Jahangir Alam Majumder and Hiroki Kashiwazaki and Ji{-}Jiang Yang and Michiharu Takemoto and Nazmus Sakib and Ryohei Banno and Sheikh Iqbal Ahamed},
    keywords = {eupex, icsc, semantics},
    url = {https://iris.unito.it/retrieve/1f9f959c-cd88-4d9c-90ea-54f1c86a15bc/6210-medic.pdf},
    bdsk-url-1 = {https://iris.unito.it/retrieve/1f9f959c-cd88-4d9c-90ea-54f1c86a15bc/6210-medic.pdf},
    bdsk-url-2 = {https://doi.org/10.1109/COMPSAC57700.2023.00289}
    }

  • G. Mittone, N. Tonci, R. Birke, I. Colonnelli, D. Medić, A. Bartolini, R. Esposito, E. Parisi, F. Beneventi, M. Polato, M. Torquati, L. Benini, and M. Aldinucci, “Experimenting with Emerging RISC-V Systems for Decentralised Machine Learning,” in 20th ACM International Conference on Computing Frontiers (CF ’23), Bologna, Italy, 2023. doi:10.1145/3587135.3592211
    [BibTeX] [Abstract] [Download PDF]

    Decentralised Machine Learning (DML) enables collaborative machine learning without centralised input data. Federated Learning (FL) and Edge Inference are examples of DML. While tools for DML (especially FL) are starting to flourish, many are not flexible and portable enough to experiment with novel systems (e.g., RISC-V), non-fully connected topologies, and asynchronous collaboration schemes. We overcome these limitations via a domain-specific language allowing to map DML schemes to an underlying middleware, i.e. the FastFlow parallel programming library. We experiment with it by generating different working DML schemes on two emerging architectures (ARM-v8, RISC-V) and the x86-64 platform. We characterise the performance and energy efficiency of the presented schemes and systems. As a byproduct, we introduce a RISC-V porting of the PyTorch framework, the first publicly available to our knowledge.

    @inproceedings{23:mittone:fl-riscv,
    title = {Experimenting with Emerging {RISC-V} Systems for Decentralised Machine Learning},
    author = {Mittone, Gianluca and Tonci, Nicol{\`o} and Birke, Robert and Colonnelli, Iacopo and Medi\'{c}, Doriana and Bartolini, Andrea and Esposito, Roberto and Parisi, Emanuele and Beneventi, Francesco and Polato, Mirko and Torquati, Massimo and Benini, Luca and Aldinucci, Marco},
    year = {2023},
    month = may,
    booktitle = {20th {ACM} International Conference on Computing Frontiers ({CF} '23)},
    publisher = {{ACM}},
    address = {Bologna, Italy},
    doi = {10.1145/3587135.3592211},
    isbn = {979-8-4007-0140-5/23/05},
    note = {https://arxiv.org/abs/2302.07946},
    abstract = {Decentralised Machine Learning (DML) enables collaborative machine learning without centralised input data. Federated Learning (FL) and Edge Inference are examples of DML. While tools for DML (especially FL) are starting to flourish, many are not flexible and portable enough to experiment with novel systems (e.g., RISC-V), non-fully connected topologies, and asynchronous collaboration schemes. We overcome these limitations via a domain-specific language allowing to map DML schemes to an underlying middleware, i.e. the FastFlow parallel programming library. We experiment with it by generating different working DML schemes on two emerging architectures (ARM-v8, RISC-V) and the x86-64 platform. We characterise the performance and energy efficiency of the presented schemes and systems. As a byproduct, we introduce a RISC-V porting of the PyTorch framework, the first publicly available to our knowledge.},
    date-added = {2023-03-14 15:34:00 +0000},
    institution = {Computer Science Department, University of Torino},
    keywords = {eupilot, icsc, learning, parallel, riscv, federated},
    url = {https://dl.acm.org/doi/pdf/10.1145/3587135.3592211}
    }

  • I. Colonnelli, B. Casella, G. Mittone, Y. Arfat, B. Cantalupo, R. Esposito, A. R. Martinelli, D. Medić, and M. Aldinucci, “Federated Learning meets HPC and cloud,” in Astrophysics and Space Science Proceedings, Catania, Italy, 2023, p. 193–199. doi:10.1007/978-3-031-34167-0_39
    [BibTeX] [Abstract] [Download PDF]

    HPC and AI are fated to meet for several reasons. This article will discuss some of them and argue why this will happen through the set of methods and technologies that underpin cloud computing. As a paradigmatic example, we present a new federated learning system that collaboratively trains a deep learning model in different supercomputing centers. The system is based on the StreamFlow workflow manager designed for hybrid cloud-HPC infrastructures.

    @inproceedings{22:ml4astro,
    title = {Federated Learning meets {HPC} and cloud},
    author = {Iacopo Colonnelli and Bruno Casella and Gianluca Mittone and Yasir Arfat and Barbara Cantalupo and Roberto Esposito and Alberto Riccardo Martinelli and Doriana Medi\'{c} and Marco Aldinucci},
    year = {2023},
    booktitle = {Astrophysics and Space Science Proceedings},
    publisher = {Springer},
    address = {Catania, Italy},
    volume = {60},
    pages = {193--199},
    doi = {10.1007/978-3-031-34167-0_39},
    isbn = {978-3-031-34167-0},
    abstract = {HPC and AI are fated to meet for several reasons. This article will discuss some of them and argue why this will happen through the set of methods and technologies that underpin cloud computing. As a paradigmatic example, we present a new federated learning system that collaboratively trains a deep learning model in different supercomputing centers. The system is based on the StreamFlow workflow manager designed for hybrid cloud-HPC infrastructures.},
    editor = {Bufano, Filomena and Riggi, Simone and Sciacca, Eva and Schilliro, Francesco},
    url = {https://iris.unito.it/retrieve/5631da1c-96a0-48c0-a48e-2cdf6b84841d/main.pdf},
    bdsk-url-1 = {https://iris.unito.it/retrieve/5631da1c-96a0-48c0-a48e-2cdf6b84841d/main.pdf},
    keywords = {across, eupilot, streamflow, federated}
    }

2021

  • I. Lanese, D. Medić, and C. A. Mezzina, “Static versus dynamic reversibility in CCS,” Acta Informatica, vol. 58, p. 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}},
    author = {Ivan Lanese and Doriana Medi\'{c} and Claudio Antares Mezzina},
    year = {2021},
    journal = {Acta Informatica},
    volume = {58},
    pages = {1--34},
    doi = {10.1007/s00236-019-00346-6},
    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.},
    keywords = {, semantics},
    url = {https://doi.org/10.1007/s00236-019-00346-6},
    bdsk-url-1 = {https://doi.org/10.1007/s00236-019-00346-6}
    }

  • C. Aubert and D. Medić, “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,
    title = {Explicit Identifiers and Contexts in Reversible Concurrent Calculus},
    author = {Cl{\'{e}}ment Aubert and Doriana Medi\'{c}},
    year = {2021},
    booktitle = {Reversible Computation - 13th International Conference, {RC} 2021, Virtual Event, July 7-8, 2021, Proceedings},
    publisher = {Springer},
    doi = {10.1007/978-3-030-79837-6\_9},
    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.},
    bdsk-url-1 = {https://doi.org/10.1007/978-3-030-79837-6\_9},
    keywords = {semantics},
    url = {https://doi.org/10.1007/978-3-030-79837-6\_9}
    }

2020

  • D. Medić, 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 Pi-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,
    title = {A parametric framework for reversible \emph{{\(\pi\)}}-calculi},
    author = {Doriana Medi\'{c} and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
    year = {2020},
    journal = {Information and Computation},
    volume = {275},
    pages = {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 Pi-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 = {, semantics},
    url = {https://doi.org/10.1016/j.ic.2020.104644},
    bdsk-url-1 = {https://doi.org/10.1016/j.ic.2020.104644}
    }

  • I. Lanese and D. Medić, “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,
    title = {A General Approach to Derive Uncontrolled Reversible Semantics},
    author = {Ivan Lanese and Doriana Medi\'{c}},
    year = {2020},
    booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)},
    publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
    series = {LIPIcs},
    volume = {171},
    pages = {33:1--33:24},
    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 = {, semantics},
    url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.33},
    bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.33}
    }

  • D. Medić, 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,
    title = {Towards a Formal Account for Software Transactional Memory},
    author = {Doriana Medi\'{c} and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
    year = {2020},
    booktitle = {Reversible Computation - 12th International Conference, {RC} 2020, Oslo, Norway, July 9-10, 2020, Proceedings},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    volume = {12227},
    pages = {255--263},
    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 = {semantics},
    url = {https://doi.org/10.1007/978-3-030-52482-1_16},
    bdsk-url-1 = {https://doi.org/10.1007/978-3-030-52482-1_16}
    }

2019

  • D. Medić, “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,
    title = {Relative expressiveness of calculi for reversible concurrency},
    author = {Doriana Medi\'{c}},
    year = {2019},
    journal = {Bull. {EATCS}},
    volume = {129},
    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.},
    keywords = {, semantics},
    url = {http://bulletin.eatcs.org/index.php/beatcs/article/view/590/601},
    bdsk-url-1 = {http://bulletin.eatcs.org/index.php/beatcs/article/view/590/601}
    }