Reo Coordination Language

Reo-krets: Generator

Reo är ett domänspecifikt språk för programmering och analys av koordinationsprotokoll som sammansätter individuella processer till fullständiga system , brett tolkade. Exempel på klasser av system som kan sammansättas med Reo inkluderar komponentbaserade system, tjänsteorienterade system, flertrådssystem , biologiska system och kryptografiska protokoll. Reo har en grafisk syntax där varje Reo-program, som kallas en kontakt eller krets , är en märkt riktad hypergraf . En sådan graf representerar dataflödet mellan processerna i systemet. Reo har formell semantik , som ligger till grund för dess olika formella verifieringstekniker och kompileringsverktyg.

Definitioner

I Reo består ett samtidigt system av en uppsättning komponenter som limmas ihop av en krets som möjliggör flöde av data mellan komponenter. Komponenter kan utföra I/O-operationer på gränsnoderna för den krets som de är anslutna till. Det finns två typer av I/O-operationer: put-requests skickar dataobjekt till en nod och get-requests hämtar dataobjekt från en nod. Alla I/O-operationer blockeras, vilket innebär att en komponent kan fortsätta först efter att dess väntande I/O-operation har bearbetats.

Bilden uppe till höger visar ett exempel på ett producent-konsumentsystem med tre komponenter: två producenter till vänster och en konsument till höger. Kretsen i mitten definierar protokollet, som säger att producenterna ska skicka data synkront, medan konsumenten tar emot dessa data i omväxlande ordning.

Formellt definieras strukturen för en krets enligt följande:

Definition 1. En krets är en trippel $R=(N,B,C,t)$ där:

1. N är en uppsättning noder ;
2. $B\subseteq N$ är en uppsättning gränsnoder ;
3. $C\subseteq 2^{N}\times 2^{N}$ är en uppsättning kanaler ;
4. $t:C\rightarrow T$ tilldelar en typ till varje kanal.

sådan att $|I\cup O|=2$ , för alla $(I,O)\in C$ . Om $c=(I,O)\in C$ är en kanal, då kallas I uppsättningen av ingångsnoder av c och O kallas uppsättningen av utgångsnoder av c .

Dynamiken i en krets liknar flödet av signaler genom en elektronisk krets .

Noder har fast fusion-replikatorbeteende: data från en av de inkommande kanalerna sprids till alla utgående kanaler, utan att lagra eller ändra data (dvs. replikatorbeteende). Om flera inkommande kanaler kan tillhandahålla data, gör noden ett icke-deterministiskt val bland dem (dvs fusionsbeteende). Noder med endast inkommande eller utgående kanaler kallas sjunknoder respektive källnoder ; noder med både inkommande och utgående kanaler kallas blandade noder .

Till skillnad från noder har kanaler användardefinierat beteende representerat av sin typ. Detta innebär att kanaler kan lagra eller ändra dataelement som flödar genom dem. Även om varje kanal ansluter exakt två noder, behöver dessa noder inte in- och utmatas. Till exempel har den vertikala kanalen i figuren längst upp till höger två ingångar och inga utgångar. Kanaltypen definierar kanalens beteende med avseende på data. Nedan är en lista över vanliga typer:

• Synk : Atomiskt hämtar data från sin ingångsnod och sprider den till sin utgångsnod.
• LossySync : Samma som Sync, men kan förlora data om dess utgångsnod inte är redo att ta data.
• Fifo ⟨ n ⟩ : Hämtar data från sin ingångsnod, lagrar den tillfälligt i en intern buffert av storlek n och sprider den till sin utgångsnod (när denna utgångsnod är redo att ta data).
• SyncDrain : Atomically hämtar data från båda dess ingångsnoder och förlorar den.
• Filter ⟨ c ⟩ : Atomiskt hämtar data från sin ingångsnod och sprider den till sin utgångsnod om filtervillkoret c är uppfyllt; förlorar data annars.

Programvarutekniska egenskaper

Exogenitet

Ett sätt att klassificera koordinationsspråk är i termer av deras locus : locus of coordination hänvisar till var koordinationsaktivitet äger rum, klassificering av koordinationsmodeller och språk som endogena eller exogena . Endogena modeller och språk, såsom Linda , tillhandahåller primitiver som måste inkorporeras i en beräkning för dess koordinering. I applikationer som använder sådana modeller finns primitiver som påverkar koordinationen av varje modul inne i själva modulen. Däremot är Reo ett exogent språk som tillhandahåller primitiver som stödjer samordning av enheter utifrån. I applikationer som använder exogena modeller är primitiver som påverkar koordinationen av varje modul utanför själva modulen.

Endogena modeller är ibland mer naturliga för en given tillämpning. Emellertid leder de i allmänhet till en sammanblandning av koordinationsprimitiver med beräkningskod, vilket trasslar in beräkningens semantik med koordinationsprotokoll. Denna sammanblandning tenderar att sprida kommunikations-/koordinationsprimitiver genom källkoden, vilket gör samarbetsmodellen och koordinationsprotokollet för en applikation oklar och implicit: i allmänhet finns det ingen källkod som kan identifieras som samarbetsmodellen eller koordinationsprotokollet för en applikation , som kan designas, utvecklas, felsöka, underhållas och återanvändas, isolerat från resten av applikationskoden. Å andra sidan uppmuntrar exogena modeller utveckling av koordinationsmoduler separat och oberoende av de beräkningsmoduler de ska koordinera. Följaktligen kan resultatet av den betydande ansträngning som satsas på design och utveckling av koordinationskomponenten i en applikation visa sig som påtagliga "rena koordinatormoduler" som är lättare att förstå, och som även kan återanvändas i andra applikationer.

Kompositionalitet / återanvändbarhet

Reo-kretsar är sammansatta. Det betyder att man kan konstruera komplexa kretsar genom att återanvända enklare kretsar. För att vara mer tydlig kan två kretsar limmas ihop på sina gränsnoder för att bilda en ny gemensam krets. Till skillnad från många andra modeller för samtidighet (t.ex. pi-kalkyl ) bevaras synkroniseringen under sammansättning. Det betyder att om vi komponerar en krets med synkront flöde mellan noderna A och B med en annan krets med synkront flöde mellan noderna B och C så har den gemensamma kretsen synkront flöde mellan noderna A och C. Med andra ord sammansättningen av två synkrona kretsar ger en synkron krets.

Semantik

Semantiken för en Reo-krets är en formell beskrivning av dess beteende. Olika semantiker för Reo finns.

Historiskt sett baserades Reos första semantik på den koalgebraiska föreställningen om strömmar (dvs. oändliga sekvenser). Denna semantik är baserad på konceptet med en tidsinställd dataström , som är ett par som består av en ström av dataobjekt och en ström av monotont ökande tidsstämplar (reella tal). Genom att associera varje nod med en sådan tidsinställd dataström kan beteendet hos en kanal modelleras som en relation på strömmarna på de anslutna noderna.

Senare utvecklades en automatbaserad semantik, som kallas constraint automata . En begränsningsautomat är ett märkt övergångssystem, där övergångsetiketter består av en synkroniseringsrestriktion och en datarestriktion . En synkroniseringsrestriktion specificerar vilka noder som synkroniserar i exekveringssteget som modelleras av övergången, och en datarestriktion specificerar vilka dataobjekt som flödar på dessa noder.

En begränsning av begränsningsautomater (och tidsinställda dataströmmar) är att de inte direkt kan modellera kontextkänsligt beteende, där beteendet hos en kanal beror på (o)tillgängligheten hos en väntande I/O-operation. Till exempel, med hjälp av begränsningsautomater, är det omöjligt att direkt modellera beteendet hos en LossySync, som endast bör förlora data om dess utmatningsnod inte har någon väntande get-begäran. För att lösa detta problem har en annan semantik av Reo utvecklats, kallad connector coloring .

Annan semantik för Reo gör det möjligt att modellera tidsbestämt eller probabilistiskt beteende.

Genomföranden

Extensible Coordination Tools (ECT) är en uppsättning plug-ins för Eclipse som utgör en integrerad utvecklingsmiljö ( IDE) för Reo. ECT består av en grafisk editor för att rita kretsar och en animationsmotor för att animera dataflödet genom kretsar. För kodgenerering innehåller ECT en Reo-to-Java-kompilator, som genererar kod för kretsar baserat på deras begränsningsautomatiska semantik. I synnerhet, vid inmatning av en Reo-krets, producerar den en Java-klass, som simulerar begränsningsautomaten som modellerar kretsen. För verifiering innehåller ECT ett verktyg som översätter Reo-kretsar till processdefinitioner i mCRL2 . Användare kan sedan använda mCRL2 för modellkontroll mot mu-calculus- egenskapsspecifikationer. (Alternativt stöder Vereofy-modellkontrollen också verifiering av Reo-kretsar.)

En annan implementering av Reo är utvecklad i programmeringsspråket Scala och exekverar kretsar på ett distribuerat sätt.

externa länkar

• Reos hemsida