Koreografisk programmering

Inom datavetenskap är koreografisk programmering ett programmeringsparadigm där program är sammansättningar av interaktioner mellan flera samtidiga deltagare .

Översikt

Koreografier

I koreografisk programmering använder utvecklare ett koreografiskt programmeringsspråk för att definiera det avsedda kommunikationsbeteendet för samtidiga deltagare. Program i detta paradigm kallas koreografier . Koreografiska språk är inspirerade av säkerhetsprotokollnotation (även känd som "Alice och Bob"-notation). Nyckeln till dessa språk är till exempel den primitiva kommunikationen

Alice.expr -> Bob.x

läser " Alice kommunicerar resultatet av utvärderingen av uttrycket expr till Bob , som lagrar det i sin lokala variabel x ". Alice, Bob, etc. kallas vanligtvis roller eller processer .

Exemplet nedan visar en koreografi för ett förenklat protokoll för enkel inloggning (SSO) baserat på en central autentiseringstjänst (CAS) som involverar tre roller:

Klient som vill erhålla en åtkomsttoken från CAS för att interagera med tjänsten .
Tjänst , som behöver veta från CAS om Kunden ska ges åtkomst.
CAS , som är den centrala autentiseringstjänsten som ansvarar för att kontrollera kundens autentiseringsuppgifter.

Koreografin är:

 Client.(credentials, serviceID) -> CAS.authRequest  if CAS.check(authRequest) then  CAS.token = genToken(authRequest)  CAS.Success(token) -> Client.result  CAS.Success(token) -> Service.result  else  CAS.Failure -> Client.result  CAS.Failure -> Service.result

Koreografin börjar på rad 1, där klienten kommunicerar ett par som består av några referenser och identifieraren för tjänsten den vill ha åtkomst till CAS . CAS lagrar detta par i sin lokala variabel authRequest (för autentiseringsbegäran). På rad 2 CAS om begäran är giltig för att erhålla en autentiseringstoken. Om så är fallet genererar den en token och kommunicerar ett framgångsmeddelande som innehåller token till både klienten och tjänsten (raderna 3–5). I annat fall informerar CAS klienten och tjänsten om att autentiseringen misslyckades genom att skicka ett felmeddelande (raderna 7–8). Vi hänvisar till denna koreografi som "SSO-koreografin" i resten.

Endpoint Projection

En nyckelfunktion i koreografisk programmering är förmågan att sammanställa koreografier till distribuerade implementeringar. Dessa implementeringar kan vara bibliotek för programvara som behöver delta i ett datornätverk genom att följa ett protokoll, eller fristående distribuerade program.

Översättningen av en koreografi till distribuerade program kallas för endpoint projection (förkortat EPP).

Endpoint-projektion returnerar ett program för varje roll som beskrivs i källkoreografin. Till exempel, med tanke på koreografin ovan, skulle slutpunktsprojektion returnera tre program: ett för Client , ett för Service och ett för CAS . De visas nedan i pseudokodform, där send och recv är primitiver för att skicka och ta emot meddelanden till/från andra roller.

Endpoint Projection (EPP) av SSO-koreografin

Klient

Service

CAS

 skicka (referenser, serviceID) till CAS  recv resultat från CAS

recv resultat från CAS

 recv authRequest från Client  if check(authRequest) then  token = genToken(authRequest)  skicka Success(token) till klienten  skicka Success(token) till tjänsten  annars  skicka Misslyckande till klienten  skicka Misslyckad tjänst

För varje roll innehåller dess kod de åtgärder som rollen ska utföra för att implementera koreografin korrekt tillsammans med de andra.

Utveckling

Paradigmet för koreografisk programmering kommer från dess titulära doktorsavhandling. Inspirationen till syntaxen för koreografiska programmeringsspråk kan spåras tillbaka till säkerhetsprotokollnotation , även känd som "Alice och Bob"-notation. Koreografisk programmering har också starkt påverkats av standarder för tjänstekoreografi och interaktionsdiagram , såväl som utvecklingen av teorin om processkalkyler .

Koreografisk programmering är ett aktivt forskningsområde. Paradigmet har använts i studiet av informationsflöde , parallell beräkning , cyberfysiska system , runtime-anpassning och systemintegration .

språk

AIOCJ ( hemsida ). Ett koreografiskt programmeringsspråk för anpassningsbara system som producerar kod i Jolie .
Chor ( hemsida ). Ett sessionstypat koreografiskt programmeringsspråk som kompileras till mikrotjänster i Jolie .
Choral ( hemsida ). Ett objektorienterat koreografiskt programmeringsspråk av högre ordning som kompileras till bibliotek i Java .
Kärnkoreografier. En grundläggande teoretisk modell för koreografisk programmering. En mekaniserad implementering finns tillgänglig i Coq .
Kalas. Ett koreografiskt programmeringsspråk med en verifierad kompilator till CakeML.
Piruett. En mekaniserad koreografisk programmeringsspråksteori med procedurer av högre ordning.

Se även

externa länkar

www.choral-lang.org