Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Synchronization Strategies for Global Computing Models
Ivan Lanese
abstract:
We analyze different aspects of synchronization in models for Global Computing, concentrating on mobility, heterogeneity and compositionality. We start by presenting a comparison among three different models from the literature: Fusion Calculus, a calculus with mobility; Synchronized Hyperedge Replacement (SHR), a graph transformation framework that can be equipped with both Milner (i.e., CCS style) and Hoare (i.e., CSP style) synchronization; and Logic Programming, used as goal rewriting mechanism. We show that Milner SHR is essentially a graphical concurrent extension of Fusion Calculus with multi-party synchronization. The comparison between Hoare and Milner SHR shows that the two models have different expressiveness, and that Hoare SHR can be mimicked using Milner SHR, while the contrary is not always possible. The last step of the comparison shows a strict correspondence between Hoare SHR and an extension of Logic Programming with a transactional mechanism and an hiding operator. The choice of the synchronization policy to be used in a modeling framework is crucial, since implementing a synchronization policy on top of another one is not an easy task. Thus we introduce Synchronization Algebras with Mobility (SAMs), an abstract description of a synchronization model obtained by extending Winskel's synchronization algebras to cope with mobility and local resource handling. SAMs are used to make existing frameworks parametric w.r.t. a synchronization model, which can thus be chosen to match the characteristics of the modeled system. Parametric SHR applies this approach to SHR while PRISMA Calculus is the corresponding extension for Fusion Calculus. Furthermore, we introduce SHR for heterogeneous systems, where different SAMs can be used at the same time to manage interactions performed in different parts of an heterogeneous system. We also study compositionality properties of the observational semantics of the analyzed frameworks. In particular we choose bisimilarity as semantics and we show whether this is a congruence w.r.t. the operators of system composition. We extend standard bialgebraic techniques to prove that bisimilarity is a congruence for parametric SHR. We also present a concurrent operational semantics for Fusion Calculus and we prove that the corresponding bisimilarity is a congruence, while the same property does not hold for standard interleaving semantics.
