Hoare vs. Milner: Comparing Synchronizations in a Graphical Framework With Mobility : Ugo Montanari
Università di Pisa
Ivan Lanese
Università di Pisa Hoare vs. Milner: Comparing Synchronizations in a Graphical Framework With Mobility in collaboration with
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Graphical Approach to Distributed Systems : Graphical Approach to Distributed Systems Motivations:
Intuitive representation of distribution
Natural concurrent semantics
No need of structural axioms
Existing modeling languages, e.g. UML
Applications to software architectures and ADL’s
Well-developed foundations
Graph vs. Term Transformations : Graph vs. Term Transformations Terms
LTS defined via SOS rules
Reduction rules
Abstract semantics
Non-interleaving semantics
Graphs
Double-pushout derivations
Concurrent semantics based on shift equivalence
Synchronized (hyper)edge replacement
(Hyper)Graphs : (Hyper)Graphs Edge: Atomic item with a label from alphabet LE= {LEn}n=0,1,… with as many (ordered) tentacles as the rank of its label.
Graph: A set of nodes and a set of edges such that each edge is connected, by its tentacles, to its attachment nodes. A set of external nodes, identified by distinct names, defines the connecting points with the environment. L L M 1 2 3 4 x y z
A Notation For Graphs : A Notation For Graphs Edge: Atomic item with a label from alphabet LE= {LEn}n=0,1,… with as many (ordered) tentacles as the rank of its label.
Graph: A set of nodes and a set of edges such that each edge is connected, by its tentacles, to its attachment nodes. A set of external nodes, identified by distinct names, defines the connecting points with the environment.
A Notation For Graphs : A Notation For Graphs Well formed judgements for graphs Structural Axioms (AG5) x.G = G if x fn(G) (AG1) (G1|G2)|G3 = G1|(G2|G3) (AG2) G1|G2 = G2|G1 (AG3) G1| nil = G1 (AG4) x.y.G = y.x.G (AG6) x.G = y.G {y/x} if y fn(G) (AG7) x.(G1|G2 ) = (x. G1) | G2 if x fn(G2)
A Notation For Graphs : A Notation For Graphs Well formed judgements for graphs (RG1) x1,…,xn nil (RG2) x1,…,xn L(y1,…,ym) G1|G2 (RG3) Syntactic Rules (RG4) , x G x. G
A Notation For Graphs : A Notation For Graphs Ring Example
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Edge Replacement Systems : Edge Replacement Systems Productions: A context free production rewrites a single edge labeled by L into an arbitrary graph R. (Notation: L R)
L 1 2 3 4 R 1 2 3 4 H
Edge Replacement Systems : Edge Replacement Systems Productions: A context free production rewrites a single edge labeled by L into an arbitrary graph R. (Notation: L R)
Rewritings of different edges can be executed concurrently
Synchronized Edge Replacement : Synchronized Edge Replacement Synchronized rewriting: Actions are associated to nodes in productions. Each rewrite of an edge must match actions with (a number of) its adjacent edges and they have to move simultaneously How many edges synchronize depends on the synchronization policy Synchronized rewriting propagates synchronization
all over the graph
Synchronized Edge Replacement : Synchronized Edge Replacement Hoare Synchronization: All adjacent edges must match the actions on the shared node Milner Synchronization: Only two of the adjacent edges synchronize by matching their complementary actions
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Adding Mobility : Adding Mobility
Transitions as Judgements : Transitions as Judgements Formalization of synchronized rewriting as judgements
Transitions as Judgements : Transitions as Judgements Formalization of synchronized rewriting as judgements Transitions
are generated from the productions by applying the transition rules
of the chosen synchronization mechanism
Synchronization via Unification : Synchronization via Unification Hoare synchronization On each node all edges must have the same action
Synchronization is possible if there is a most general unifier of the new nodes For any R x A x N* (not necessarily a partial function)
(R): n(R) is the mgu of equations (a= b) (Y = Z) with (x,a,Y) and (x,b,Z) in R where (as usual) = {z | (x,a,Y) R, z set(Y), z }
Example : Example
Synchronization via Unification : Synchronization via Unification Milner synchronization On each node at most two edges must have actions, and in this case they must be complementary
Synchronization is possible if there is a most general unifier of the new nodes
Adding Fusion : Adding Fusion Synchronized rewriting with mobility and fusion
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Rewriting Rules, Hoare Synchronization I : Rewriting Rules, Hoare Synchronization I
Rewriting Rules, Hoare Synchronization II : Rewriting Rules, Hoare Synchronization II
Rewriting Rules, Milner Synchronization I : Rewriting Rules, Milner Synchronization I
Rewriting Rules, Milner Synchronization II : Rewriting Rules, Milner Synchronization II
Related Work : Related Work Grammars for distributed systems
[Castellani and Montanari, LNCS 1953, 1982], [Degano and Montanari, JACM 1987]
Graph amalgamation
[Boehm, Fonio and Habel, JCSS, 1987]
CHARM (R for restriction)
[Corradini, Montanari and Rossi, TCS 1994]
Mobile version (w. applications to software architectures, only p-I-like mobility, Hoare synchronization)
[Hirsch and Montanari, Coordination 2000]
Modeling p-calculus (Milner synchronization)
[Hirsch and Montanari, Concur 2001]
Modeling Ambient calculus [Ferrari, Montanari and Tuosto, ICTCS 2001]
Modeling Fusion calculus [Lanese and Montanari, to appear in TCS]
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Expressiveness Measure : Expressiveness Measure (S1,C1) ≥ (S2,C2)
(i.e. style S1 is more expressive than style S2)
iff there exists a uniform simulation function f such that for all P and G
C2-behavS2(P)(G) = C1-behavS1(f(P))(G)
Hoare and Milner, Direct Comparison, I : Hoare and Milner, Direct Comparison, I (Milner,C1) ≥ (Hoare,C2) for all C1 and C2
i.e. Hoare cannot be uniformely simulated by Milner
The reason is that Milner synchronization style is monotone, i.e. in a Milner computation we can always add to a graph an additional part which stays idle, while Hoare style is not monotone
Hoare and Milner, Direct Comparison, II : Hoare and Milner, Direct Comparison, II (Hoare,C1) ≥ (Milner,C2) for all C1 and C2
i.e. Milner cannot be uniformely simulated by Hoare
The reason is that in Hoare synchronization style restriction just hides part of the observation, while in Milner style restriction may forbid computations
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Translation via Amoeboids : Translation via Amoeboids Amoeboids are graphs with suitable edge labels and corresponding productions which simulate the behavior of nodes in a different synchronization style
Function [[-]] replaces nodes with amoeboids while function [[-]]-1 replaces amoeboids with nodes.
We always have that [[([[G]])]]-1 = G
Implementing Hoare with Milner : Implementing Hoare with Milner H-amoeboids implement broadcasting. C-amoeboids saturate nodes with less than 3 tentacles. We have rules for every action a (here with arity 2). We have C-behavH(P)(G) = [[C-behavM(f(P))([[G]])]]-1
Implementing Milner with Hoare : Implementing Milner with Hoare M-amoeboids implement routing. We have rules for every action a and two analogous productions for synchronizing x with z and y with z.
We have only
C-behavM(P)(G) [[C-behavH(f(P))([[G]])]]-1
since the amoeboids can also synchronize several pairs in parallel.
Outline : Outline Graphical Calculi for Distributed Systems
Synchronized Edge Replacement Systems
Mobility
Hoare and Milner Synchronization, with Fusion
Direct Comparison
Comparison with Translations
Conclusions and Future Work
Conclusions and Future Work : Conclusions and Future Work Graph models with synchronized hyperedge replacement allow for more general synchronization mechanisms than ordinary process algebras, e.g. processes can synchronize at more than one channel and with more than one other process.
These extensions are needed for implementing one synchronization style into another.
Reachability in Hoare/Milner synchronization styles cannot be simulated uniformely
No countexample uses mobility, and thus the expressivenesses are incomparable even without mobility, and mobility does not bridge the gap
Distributed simulation via amoeboids of Milner style routers allows only concurrent pairwise synchronization
Generic synchronization styles and more general notions of implementation and refinement involving atomicity and bisimilarity can be considered: see the forthcoming PhD thesis of Ivan Lanese