A comparative study of type systems for deadlock-free processes
Een vergelijkende studie van typesystemen voor deadlock-vrije processen
Dit proefschrift gaat over verificatietechnieken voor message-passing programma's, die centraal staan in grootschalige softwaresystemen die essentieel zijn voor de samenleving. In deze context onderscheidt statische verificatie op basis van typesystemen zich, omdat zij compositional analyses mogelijk maakt en strikte correctheidsgaranties biedt voor programma's. Er zijn veel geavanceerde typesystemen ontwikkeld voor gelijktijdige programma's met message passing. Dit roept een natuurlijke vraag op: hoe verhouden deze systemen zich tot elkaar, en kunnen ze verder worden ontwikkeld om complexe programma's effectiever te analyseren?
Logica biedt een solide basis voor het ontwerpen van typesystemen voor gelijktijdigheid. Recente ontwikkelingen benutten overeenkomsten tussen lineaire logica (LL), de bekende logica van hulpbronnen, en session types, die protocollen specificeren voor kanaalgebaseerde communicatie. Deze overeenkomsten, geformuleerd in de stijl van Curry–Howard, worden vaak aangeduid als propositions-as-sessions. Dit proefschrift ontwikkelt een vergelijkende studie van typesystemen, waarbij propositions-as-sessions dient als maatstaf voor vergelijkingen, analyses en uitbreidingen. We zijn geïnteresseerd in hoe logische principes de eigenschap van deadlock-vrijheid afdwingen, die de afwezigheid van “vastgelopen toestanden” in interacterende programma's garandeert.
Onze studie omvat verschillende typesystemen voor de π-calculus, die elk voortkomen uit varianten van LL via de Curry–Howard-correspondentie. We beschouwen typesystemen gebaseerd op intuïtionistische lineaire logica (ILL), klassieke lineaire logica (CLL), klassieke lineaire logica met hypersequenten (HLL), en differentiële lineaire logica (DiLL). Daarnaast beschouwen we een level-based typesysteem, dat niet op logische principes is gebaseerd, maar toch (dead)lock-vrijheid afdwingt, zelfs voor procesnetwerken met circulaire topologieën. Ons doel is om de klassen van processen die door logica-gebaseerde systemen worden geïnduceerd met elkaar in verband te brengen; daarnaast willen we logische benaderingen vergelijken met het level-based typesysteem.
Onze bijdragen bestrijken verschillende invalshoeken. We richten ons eerst op propositions-as-sessions en leggen verbanden tussen de gelijktijdige interpretaties van CLL, ILL en HLL. Vervolgens vergelijken we de gelijktijdige interpretatie van HLL met het level-based systeem, waarbij we eerdere resultaten generaliseren. Deze resultaten betreffen bestaande typesystemen. In het laatste deel stellen we een nieuw logica-gebaseerd typesysteem voor dat DiLL uitbreidt met levels. Het resultaat is een modulair typesysteem dat de canonieke principes van propositions-as-sessions uniform combineert met de effectiviteit van de level-based benadering. Al met al bieden onze bevindingen nieuwe inzichten in het afdwingen van deadlock-vrijheid in message-passing gelijktijdigheid; ze bevestigen opnieuw de ongebruikelijke effectiviteit van logica voor programma-analyse.