556:
communication/coordination primitives throughout the source code, making the cooperation model and the coordination protocol of an application nebulous and implicit: generally, there is no piece of source code identifiable as the cooperation model or the coordination protocol of an application, that can be designed, developed, debugged, maintained, and reused, in isolation from the rest of the application code. On the other hand, exogenous models encourage development of coordination modules separately and independently of the computation modules they are supposed to coordinate. Consequently, the result of the substantial effort invested in the design and development of the coordination component of an application can manifest itself as tangible "pure coordinator modules" which are easier to understand, and can also be reused in other applications.
642:(IDE) for Reo. The ECT consists of a graphical editor for drawing circuits and an animation engine for animating data-flow through circuits. For code generation, the ECT contains a Reo-to-Java compiler, which generates code for circuits based on their constraint automaton semantics. In particular, on input of a Reo circuit, it produces a Java class, which simulates the constraint automaton that models the circuit. For verification, the ECT contains a tool that translates Reo circuits to process definitions in
552:, provide primitives that must be incorporated within a computation for its coordination. In applications that use such models, primitives that affect the coordination of each module are inside the module itself. In contrast, Reo is an exogenous language that provides primitives that support coordination of entities from without. In applications that use exogenous models, primitives that affect the coordination of each module are outside the module itself.
569:), synchrony is preserved under composition. This means that if we compose a circuit with synchronous flow between nodes A and B with another circuit with synchronous flow between nodes B and C, the joint circuit has synchronous flow between nodes A and C. In other words, the composition of two synchronous circuits yields a synchronous circuit.
458:
In contrast to nodes, channels have user-defined behavior represented by their type. This means that channels may store or alter data items that flow through them. Although every channel connects exactly two nodes, these nodes need not to be input and output. For instance, the vertical channel in the
91:
The figure on the top-right shows an example of a producers-consumer system with three components: two producers on the left and one consumer on the right. The circuit in the middle defines the protocol, which states that the producers should send data synchronously, while the consumer receives those
442:
Nodes have fixed merger-replicator behavior: the data of one of the incoming channels is propagated to all outgoing channels, without storing or altering the data (i.e., replicator behavior). If multiple incoming channels can provide data, the node makes a nondeterministic choice among them (i.e.,
614:
behavior, where the behavior of a channel depends on the (un)availability of a pending I/O operation. For example, using constraint automata, it is impossible to directly model the behavior of a LossySync, which should lose data only if its output node has no pending get-request. To solve this
87:
of the circuit to which they are connected. There are two kinds of I/O operations: put-requests dispatch data items to a node, and get-requests fetch data items from a node. All I/O operations are blocking, which means that a component can proceed only after its pending I/O operation has been
555:
Endogenous models are sometimes more natural for a given application. However, they generally lead to an intermixing of coordination primitives with computation code, which entangles the semantics of computation with coordination protocols. This intermixing tends to scatter
588:, which is a pair consisting of a stream of data items and a stream of monotonically increasing time stamps (real numbers). By associating every node with such a timed data stream, the behavior of a channel can be modeled as a relation on the streams on the connected nodes.
564:
Reo circuits are compositional. This means that one can construct complex circuits by reusing simpler circuits. To be more explicit, two circuits can be glued together on their boundary nodes to form a new joint circuit. Unlike many other models of concurrency (e.g.,
17:
83:
In Reo, a concurrent system consists of a set of components which are glued together by a circuit that enables flow of data between components. Components can perform I/O operations on the
244:
607:. A synchronization constraint specifies which nodes synchronize in the execution step modeled by the transition, and a data constraint specifies which data items flow on these nodes.
282:
414:
192:
332:
153:
370:
459:
figure on the top-right has two inputs and no outputs. The channel type defines the behavior of the channel with respect to data. Below is a list of common types:
826:
851:
724:. In Martin Wirsing, Dirk Pattinson, and Rolf Hennicker, editors, Proceedings of WADT 2002, volume 2755 of LNCS, pages 34--55. Springer, 2003.
836:
40:
639:
685:. In Gul Agha, Olivier Danvy, Jose Meseguer, editors, Talcott Festschrift, volume 7000 of LNCS, pages 169-206. Springer, 2011.
841:
831:
653:
Another implementation of Reo is developed in the Scala programming language and executes circuits in a distributed fashion.
540:: locus of coordination refers to where coordination activity takes place, classifying coordination models and languages as
549:
44:
72:
698:. In Dina Goldin, Scott Smolka, and Peter Wegner, editors, Interactive Computation, pages 277-321. Springer, 2006.
203:
650:
property specifications. (Alternatively, the
Vereofy model checker also supports verification of Reo circuits.)
28:
846:
577:
The semantics of a Reo circuit is a formal description of its behavior. Various semantics for Reo exist.
518:: Atomically gets data from its input node and propagates it to its output node if the filter condition
255:
55:
systems, and cryptographic protocols. Reo has a graphical syntax in which every Reo program, called a
647:
596:
610:
One limitation of constraint automata (and timed data streams) is that they cannot directly model
375:
171:
635:
436:
295:
108:
48:
337:
75:, which stand at the basis of its various formal verification techniques and compilation tools.
599:. A constraint automaton is a labeled transition system, where transition labels consist of a
592:
584:
notion of streams (i.e., infinite sequences). This semantics is based on the concept of a
52:
39:, broadly construed. Examples of classes of systems that can be composed with Reo include
495:, and propagates it to its output node (whenever this output node is ready to take data).
779:
763:
733:
820:
491:: Gets data from its input node, temporarily stores it in an internal buffer of size
622:
Other semantics for Reo make it possible to model timed or probabilistic behavior.
16:
750:
737:
721:
682:
566:
468:: Atomically gets data from its input node and propagates it to its output node.
767:
669:
476:: Same as Sync, but can lose data if its output node is not ready to take data.
783:
695:
64:
708:
31:
for programming and analyzing coordination protocols that compose individual
581:
443:
merger behavior). Nodes with only incoming or outgoing channels are called
451:, respectively; nodes with both incoming and outgoing channels are called
768:
Models and temporal logical specifications for timed component connectors
68:
796:
672:. Mathematical Structures in Computer Science 14(3):329--366, 2004.
643:
435:
The dynamics of a circuit resemble the flow of signals through an
15:
670:
Reo: a channel-based coordination model for component composition
536:
One way to classify coordination languages is in terms of their
786:. Journal of Universal Computer Science 11(10):1718-1748, 2005.
646:. Users can subsequently use mCRL2 for model checking against
503:: Atomically gets data from both its input nodes and loses it.
811:
751:
Connector colouring I: Synchronisation and context dependency
615:
problem, another semantics of Reo has been developed, called
711:. Scientific Annals of Computer Science 22(1):201-251, 2012.
631:
95:
Formally, the structure of a circuit is defined as follows:
738:
Modeling component connectors in Reo by constraint automata
580:
Historically the first semantics of Reo was based on the
753:. Science of Computer Programming 66(3):205-225, 2007.
740:. Science of Computer Programming 61(2):75-113, 2006.
378:
340:
298:
258:
206:
174:
111:
797:Synchronous Coordination of Distributed Components
408:
364:
326:
276:
238:
186:
147:
770:. Software and Systems Modeling 6(1):59-82, 2007.
736:, Marjan Sirjani, Farhad Arbab, and Jan Rutten:
595:-based semantics was developed, which is called
784:Probabilistic Models for Reo Connector Circuits
749:Dave Clarke and David Costa and Farhad Arbab:
722:A Coinductive Calculus of Component Connectors
709:Overview of Thirty Semantic Formalisms for Reo
8:
239:{\displaystyle C\subseteq 2^{N}\times 2^{N}}
548:. Endogenous models and languages, such as
71:among the processes in the system. Reo has
377:
339:
313:
299:
297:
257:
230:
217:
205:
173:
110:
696:Composition of Interacting Computations
661:
522:is satisfied; loses the data otherwise.
799:. PhD thesis, Leiden University, 2011.
428:is called the set of output nodes of
827:Programming languages created in 2001
707:Sung-Shik Jongmans and Farhad Arbab:
7:
420:is called the set of input nodes of
640:integrated development environment
14:
766:, Frank de Boer, and Jan Rutten:
634:(ECT) are a set of plug-ins for
277:{\displaystyle t:C\rightarrow T}
527:Software engineering properties
852:Concurrency (computer science)
560:Compositionality / reusability
397:
385:
353:
341:
314:
300:
268:
142:
118:
67:. Such a graph represents the
1:
720:Farhad Arbab and Jan Rutten:
632:Extensible Coordination Tools
837:Scala (programming language)
409:{\displaystyle c=(I,O)\in C}
187:{\displaystyle B\subseteq N}
327:{\displaystyle |I\cup O|=2}
148:{\displaystyle R=(N,B,C,t)}
92:data in alternating order.
868:
601:synchronization constraint
365:{\displaystyle (I,O)\in C}
683:Puff, The Magic Protocol
88:successfully processed.
63:, is a labeled directed
29:domain-specific language
20:Reo circuit: Alternator
410:
366:
328:
278:
240:
188:
149:
21:
842:Models of computation
832:Distributed computing
411:
367:
329:
279:
241:
189:
150:
19:
376:
338:
296:
256:
204:
172:
109:
638:that constitute an
597:constraint automata
416:is a channel, then
617:connector coloring
437:electronic circuit
406:
362:
324:
274:
236:
184:
145:
22:
612:context-sensitive
586:timed data stream
288:to every channel.
859:
800:
793:
787:
777:
771:
760:
754:
747:
741:
731:
725:
718:
712:
705:
699:
692:
686:
679:
673:
666:
521:
517:
516:
502:
494:
490:
489:
475:
467:
431:
427:
423:
419:
415:
413:
412:
407:
371:
369:
368:
363:
333:
331:
330:
325:
317:
303:
283:
281:
280:
275:
245:
243:
242:
237:
235:
234:
222:
221:
193:
191:
190:
185:
161:
154:
152:
151:
146:
73:formal semantics
45:service-oriented
867:
866:
862:
861:
860:
858:
857:
856:
817:
816:
808:
803:
794:
790:
778:
774:
761:
757:
748:
744:
732:
728:
719:
715:
706:
702:
693:
689:
680:
676:
667:
663:
659:
628:
626:Implementations
605:data constraint
575:
562:
534:
529:
519:
510:
506:
498:
492:
483:
479:
471:
463:
429:
425:
421:
417:
374:
373:
336:
335:
294:
293:
254:
253:
226:
213:
202:
201:
170:
169:
159:
107:
106:
81:
41:component-based
12:
11:
5:
865:
863:
855:
854:
849:
847:Model checking
844:
839:
834:
829:
819:
818:
815:
814:
807:
806:External links
804:
802:
801:
795:José Proença:
788:
780:Christel Baier
772:
764:Christel Baier
762:Farhad Arbab,
755:
742:
734:Christel Baier
726:
713:
700:
694:Farhad Arbab:
687:
681:Farhad Arbab:
674:
668:Farhad Arbab:
660:
658:
655:
627:
624:
574:
571:
561:
558:
533:
530:
528:
525:
524:
523:
504:
496:
477:
469:
405:
402:
399:
396:
393:
390:
387:
384:
381:
361:
358:
355:
352:
349:
346:
343:
323:
320:
316:
312:
309:
306:
302:
290:
289:
273:
270:
267:
264:
261:
251:
233:
229:
225:
220:
216:
212:
209:
199:
196:boundary nodes
183:
180:
177:
167:
144:
141:
138:
135:
132:
129:
126:
123:
120:
117:
114:
85:boundary nodes
80:
77:
49:multithreading
13:
10:
9:
6:
4:
3:
2:
864:
853:
850:
848:
845:
843:
840:
838:
835:
833:
830:
828:
825:
824:
822:
813:
810:
809:
805:
798:
792:
789:
785:
781:
776:
773:
769:
765:
759:
756:
752:
746:
743:
739:
735:
730:
727:
723:
717:
714:
710:
704:
701:
697:
691:
688:
684:
678:
675:
671:
665:
662:
656:
654:
651:
649:
645:
641:
637:
633:
625:
623:
620:
618:
613:
608:
606:
602:
598:
594:
589:
587:
583:
578:
572:
570:
568:
559:
557:
553:
551:
547:
543:
539:
531:
526:
514:
509:
505:
501:
497:
487:
482:
478:
474:
470:
466:
462:
461:
460:
456:
454:
450:
446:
440:
438:
433:
403:
400:
394:
391:
388:
382:
379:
359:
356:
350:
347:
344:
321:
318:
310:
307:
304:
287:
271:
265:
262:
259:
252:
249:
231:
227:
223:
218:
214:
210:
207:
200:
197:
181:
178:
175:
168:
165:
158:
157:
156:
139:
136:
133:
130:
127:
124:
121:
115:
112:
104:
100:
99:Definition 1.
96:
93:
89:
86:
78:
76:
74:
70:
66:
62:
58:
54:
50:
46:
42:
38:
34:
30:
26:
18:
791:
775:
758:
745:
729:
716:
703:
690:
677:
664:
652:
629:
621:
616:
611:
609:
604:
600:
590:
585:
579:
576:
563:
554:
545:
541:
537:
535:
512:
507:
499:
485:
480:
472:
464:
457:
452:
449:source nodes
448:
444:
441:
434:
291:
285:
247:
246:is a set of
195:
194:is a set of
163:
162:is a set of
105:is a triple
102:
98:
97:
94:
90:
84:
82:
60:
56:
36:
32:
24:
23:
812:Reo website
648:mu-calculus
582:coalgebraic
567:pi-calculus
453:mixed nodes
79:Definitions
821:Categories
657:References
591:Later, an
542:endogenous
532:Exogeneity
445:sink nodes
334:, for all
292:such that
284:assigns a
65:hypergraph
53:biological
35:into full
593:automaton
573:Semantics
546:exogenous
500:SyncDrain
473:LossySync
401:∈
357:∈
308:∪
269:→
224:×
211:⊆
179:⊆
69:data-flow
57:connector
51:systems,
47:systems,
43:systems,
33:processes
515:⟩
511:⟨
488:⟩
484:⟨
248:channels
636:Eclipse
155:where:
103:circuit
61:circuit
37:systems
603:and a
508:Filter
372:. If
644:mCRL2
550:Linda
538:locus
286:types
164:nodes
27:is a
630:The
481:Fifo
465:Sync
424:and
544:or
447:or
59:or
25:Reo
823::
782::
619:.
455:.
439:.
432:.
101:A
520:c
513:c
493:n
486:n
430:c
426:O
422:c
418:I
404:C
398:)
395:O
392:,
389:I
386:(
383:=
380:c
360:C
354:)
351:O
348:,
345:I
342:(
322:2
319:=
315:|
311:O
305:I
301:|
272:T
266:C
263::
260:t
250:;
232:N
228:2
219:N
215:2
208:C
198:;
182:N
176:B
166:;
160:N
143:)
140:t
137:,
134:C
131:,
128:B
125:,
122:N
119:(
116:=
113:R
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
