Sessionstyp

I typteorin används sessionstyper för att säkerställa korrekthet i samtidiga program . De garanterar att meddelanden som skickas och tas emot mellan samtidiga program är i den förväntade ordningen och av den förväntade typen . Sessionstypssystem har anpassats för både kanal- och aktörssystem .

Sessionstyper används för att säkerställa önskvärda egenskaper i samtidiga och distribuerade system, dvs frånvaro av kommunikationsfel eller dödlägen, och protokollöverensstämmelse.

Binära kontra flerpartssessionstyper

Interaktion mellan två processer kan kontrolleras med binära sessionstyper, medan interaktioner mellan fler än två processer kan kontrolleras med flerpartssessionstyper . I flerpartssessionstyper beskrivs interaktioner mellan alla deltagare med en global typ , som sedan projiceras till lokala typer som beskriver kommunikation från varje deltagares lokala vy. Viktigt är att den globala typen kodar sekvenseringsinformationen för kommunikationen, som skulle gå förlorad om vi skulle använda binära sessionstyper för att koda samma kommunikation.

Formell definition av binära sessionstyper

Binära sessionstyper kan beskrivas med sändningsoperationer ( $!$ ), mottagningsoperationer ( $?$ ), grenar ( $\&$ ), val ( $\oplus$ ) , rekursion ( $rec$ ) och terminering ( ${\displaystyle end} )$ .

Till exempel, $S=\;!bool.?int.end$ representerar en sessionstyp $S$ som först skickar en boolesk ( $!bool$ ), sedan tar emot en heltal ( $?int$ ) innan den slutligen avslutas ( ${\displaystyle end} )$ .

Genomföranden

Sessionstyper har anpassats för flera befintliga programmeringsspråk, inklusive:

• l-kanaler ( Scala )
• Effpi (Scala)
• STMonitor (Scala)
• EnsembleS
• Sessionstyper ( rost )
• sesh (rost)
• Session Actors ( Python )
• Övervakad session Erlang ( Erlang )
• FuSe ( OCaml )
• session-ocaml (OCaml)
• Priority Sesh ( Haskell )