WADT 2008
19th International Workshop on
Algebraic Development Techniques
Tiles for
Reo
Roberto Bruni
Dipartimento di Informatica
Università di Pisa
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
Farhad Arbab (CWI)
Dave Clarke (CWI)
Ivan Lanese (Bologna)
Ugo Montanari (Pisa)
1
Content





Introduction
Tiles basics
Reo basics
Tile semantics of Reo
Conclusion
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
2
Introduction
• Reo is an exogenous coordination language
based on a calculus of connector composition
– http://homepages.cwi.nl/~proenca/webreo/
• Tile Systems offer a coordination model
equipped with flexible synchronization primitives
• We aim to show that tiles give an adequate
semantic setting for Reo
– exercise in understanding
– tiles have some advantages w.r.t. colouring tables,
constraint-automata, graph transformations
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
3
Content
 Introduction

 Tiles basics
 Reo basics
 Tile semantics of Reo
 Conclusion
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
4
Tiling as a Domino Game
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
5
Graph-like Decorated Tiles
• Next slides will focus on tiles that exploit
some graph-like structures of
configurations and observations
– a bit vague about exact tile syntax
• Key notions:
– configurations (with interfaces)
– observations
– tiles = trigger+effect rewrites
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
6
Configurations
input
interface
output
interface
(interfaces can be typed)
parallel
composition
sequential
composition
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
7
Configurations
input
interface
output
interface
parallel
composition
functoriality
sequential
composition
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
8
Configurations
input
interface
output
interface
functoriality
+
symmetries
=
symmetric monoidal cat
Roberto Bruni @
Pisa, Italy
13 June 2008
parallel
composition
sequential
composition
WADT 2008
9
Observations
initial
interface
concurrent
computation
final
interface
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
10
Tiles
• Combine horizontal and vertical structures
through interfaces
initial configuration
trigger
effect
final configuration
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
11
Tiles
• Compose tiles
– horizontally
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
12
Tiles
• Compose tiles
symmetric monoidal double cat
– horizontally
– (also vertically and in parallel)
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
13
Tile Semantics Recipee
• Operational semantics:
– define interfaces, configurations and observations
– define tiles for configuration constructors
• Abstract semantics:
– ordinary LTS where labels are trigger-effect pairs
– tile bisimilarity, tile trace equivalence
• Congruence results:
– tile decomposition property
– basic source format
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
14
Content
 Introduction

 Tiles basics

 Reo basics
 Tile semantics of Reo
 Conclusion
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
15
Reo Basics
• Reo channels: point-to-point primitive connectors
– one input-end + one output-end
– two input-ends
– two output-ends
• Reo node: the points where channel ends conjoin
– input node: only input-ends
– output-node: only output-ends
– mixed node: both input-ends and output-ends
• Interaction with components:
– write operation
– take operation
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
16
Replicators
• A write to an input node succeeds only if
all input-ends coincident on that node
accept the data item
– input nodes act essentially as replicators
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
17
Mergers
• A take on an output node succeeds only if at
least one of the output-ends coincident on that
node offers a data item
– if more than one available, one is selected nondeterministically and the others excluded
– output nodes act essentially as mergers
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
18
Replicators and Mergers
• Mixed nodes as pumping stations:
merger+replicator
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
19
Colouring Tables
Sync
Roberto Bruni @
Pisa, Italy
13 June 2008
LossySync
WADT 2008
SyncDrain
20
Exclusive Router
A
sA
lossy synchronous channel
B
lsC
C
sC
sF
F
Roberto Bruni @
Pisa, Italy
13 June 2008
sd
E
lsD
synchronous channel
D
sD
synchronous drain
sG
G
WADT 2008
21
Content
 Introduction

 Tiles basics

 Reo basics

 Tile semantics of Reo
 Conclusion
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
22
Tiles Ingredients
• Node machinery:
– typed interfaces
– node constructors (stateless)
• Stateless connectors
• Stateful connectors
• Observations
– write, take
– not-allowed
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
23
Reo (Mixed) Node
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
24
Merger
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
25
Replicator
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
26
Example: a mixed node
A
Syntactic sugar
Roberto Bruni @
Pisa, Italy
13 June 2008
A
WADT 2008
27
Sync Channel
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
28
Lossy Sync
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
29
Sync Drain
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
30
Sync Spout
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
31
Example: Exclusive Router
A
sA
A
B
sA
B
lsC
C
sd
sC
sF
F
Roberto Bruni @
Pisa, Italy
13 June 2008
E
C
lsD
sG
G
lsD
D
sF
D
sD
lsC
sC
sD
sG
sd
E
G
F
WADT 2008
32
Tiling the Example
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
33
Tiling the Example
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
34
Tiling the Example
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
35
Some Obvious Equivalences



Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
36
Some Obvious Equivalences
...

Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
37
Stateless vs Stateful
• Only stateless connectors so far
– colouring tables are ok
– static tile configurations
• (see axiomatization in TCS, journal version of our
CALCO 2005 paper)
• Stateful connectors are more interesting
– colouring tables miss final configuration
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
38
Empty Async FIFO1
[ ]
[ ]
[ ]
[d]
[ ]
d
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
39
Full Async FIFO1
[d]
[d]
[d]
[ ]
[d]
d
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
40
Towards Async FIFO2
[ ]
d
[ ]
[d]
many FIFO1
introduce delays
depending on their
number
[ ]
[ ]
[d]
d
[ ]
[ ]
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
41
Empty Sync FIFO1
{ }
{ }
{ }
{ }
d
d
d
{d}
Roberto Bruni @
Pisa, Italy
13 June 2008
{ }
WADT 2008
{ }
42
Full Sync FIFO1
{ }
{d}
{ d1 }
{d}
d2
d
d1
{ }
Roberto Bruni @
Pisa, Italy
13 June 2008
{d}
WADT 2008
{ d2 }
43
Async FIFO2 and FIFOk
{ }
{ }
d
[ ]
...
{ }
{ }
d
[d]
{ }
{ }
{ }
[ ]
[ ]
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
44
Async FIFO∞
( ]
( ]
(d]
(d]
( ]
( ]
d
(d]
(d]
d
( ]
(d]
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
45
Derived Operators: PAR
_|_
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
46
Derived Operators: SEQ
_::_
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
47
Derived Operators: PLUG(x)
x
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
48
Derived Operators: CLOSE
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
49
Content
 Introduction

 Tiles basics

 Reo basics

 Tile semantics of Reo

 Conclusion
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
50
Conclusion
• Operational semantics:
– local rewrite rules combined by flexible
synchronizations
• Abstract semantics:
– compositional: tile bisimilarity is a congruence
• Advantages w.r.t.
– colouring: final configurations are explicit for stateful
connectors
– c-automata: structured proofs, concurrent semantics
– graph transformations: uniform framework for
dynamic reconfigurations
Roberto Bruni @
Pisa, Italy
13 June 2008
WADT 2008
51