💻 computer science

Formally Verified Liveness with Multiparty Session Types in Rocq

Dit artikel presenteert het eerste gemachineerde bewijs van liveness voor synchrone multiparty sessietypes in de Rocq Bewijsassistent, waarbij co-inductieve bomen en relaties worden gebruikt om de veiligheid en liveness van communicatieprotocollen formeel te verifiëren via ongeveer 14.000 regels code.

Oorspronkelijke auteurs: Omer Keskin, Nobuko Yoshida, Rob van Glabbeek

Gepubliceerd 2026-05-25

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Omer Keskin, Nobuko Yoshida, Rob van Glabbeek

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een groep vrienden voor die proberen een complexe dinerpartij te organiseren waarbij iedereen perfect moet coördineren: wie brengt de wijn, wie bereidt het hoofdgerecht en wie dekt de tafel. Als één persoon vastzit te wachten op een signaal dat nooit komt, komt de hele partij tot stilstand. In de wereld van de informatica heet dit een "deadlock" of een "levendigheid"-probleem.

Dit artikel gaat over het bouwen van een wiskundige garantie dat dergelijke coördinatieprotocollen nooit vastlopen. De auteurs hebben een krachtig hulpmiddel gebruikt genaamd Rocq (een "bewijshulp", vergelijkbaar met een superstreng robotwiskundige) om te bewijzen dat een specifieke methode voor het ontwerpen van deze communicatieprotocollen perfect werkt.

Hier is de uiteenzetting van hun werk met behulp van alledaagse analogieën:

1. De Twee Manieren om de Partij te Plannen

Het artikel bespreekt twee manieren om deze communicatieregels te ontwerpen (genaamd "Multiparty Session Types"):

De Bottom-Up Aanpak: Je schrijft eerst de regels voor elke individuele persoon op en probeert vervolgens te controleren of ze bij elkaar passen. Het is alsof je iedereen vraagt hun eigen takenlijst te schrijven en vervolgens hoopt dat ze elkaar niet tegenspreken.
De Top-Down Aanpak (die dit artikel gebruikt): Je schrijft één "Meesterplan" (genaamd een Global Type) dat de hele partij beschrijft vanuit een vogelperspectief. Vervolgens genereer je automatisch een specifiek "Lokaal Plan" voor elke persoon op basis van dat Meesterplan.

De auteurs kozen voor de Top-Down-aanpak omdat deze doorgaans efficiënter is en ervoor zorgt dat de regels vanaf het begin consistent zijn.

2. Het "Vertaal"-Probleem

Het lastige deel is ervoor zorgen dat de voor elke persoon gegenereerde "Lokale Plannen" daadwerkelijk overeenkomen met het "Meesterplan".

Stel dat het Meesterplan zegt: "Alice zal een bericht sturen naar Bob."
Het Lokale Plan voor Alice moet zeggen: "Ik zal een bericht sturen naar Bob."
Het Lokale Plan voor Bob moet zeggen: "Ik zal wachten op een bericht van Alice."

Het artikel introduceert een speciale relatie genaamd Associatie. Denk hierbij aan een vertaler die controleert of de individuele Lokale Plannen trouwe kopieën zijn van het Meesterplan. Als ze "geassocieerd" zijn, weet de robotwiskundige (Rocq) dat ze veilig te gebruiken zijn.

3. De Drie Grote Garanties

De auteurs bewezen dat als je deze Top-Down-methode volgt en je plannen "geassocieerd" zijn, er drie magische dingen gebeuren:

Veiligheid (Geen Misverstanden): Als Alice probeert een bericht te sturen, is gegarandeerd dat Bob luistert naar dat specifieke type bericht. Ze zullen elkaar nooit voorbij praten.
Deadlock-vrijheid (Geen Vastlopen): De partij zal nooit een punt bereiken waar iedereen wacht op iemand anders om eerst te bewegen. Als er werk te doen is, zal er altijd iemand zijn die het kan uitvoeren.
Levendigheid (Geen Uithongering): Dit is de belangrijkste doorbraak van het artikel. Het garandeert dat als een persoon wacht om een bericht te sturen of ontvangen, dat bericht uiteindelijk zal gebeuren. Niemand blijft voor altijd vastzitten terwijl de partij doorgaat zonder hen.

4. Hoe Ze Het Bewezen (Het "Robot"-Werk)

Het bewijzen van "Levendigheid" is berucht moeilijk omdat het oneindige tijd betreft (wat gebeurt er als de partij eeuwig doorgaat?).

De Boom-Metafoor: De auteurs stellen de communicatieplannen voor als oneindige bomen. Een "Global Type" is een enorme boom die alle mogelijke toekomstige gesprekken toont.
De Enttechniek: Om te bewijzen dat de boom nooit vastloopt, gebruiken ze een techniek genaamd "enten". Stel je voor dat je een eindig stuk van de oneindige boom afsnijdt (een "context") en bewijst dat ongeacht hoe je de ontbrekende gaten invult, de logica standhoudt. Het is alsof je bewijst dat een brug veilig is door een klein, verwijderbaar stuk te testen in plaats van de hele brug tegelijk.
De Aanneming van Rechtvaardigheid: Ze gaan uit van een "rechtvaardige" wereld. In een rechtvaardige wereld zullen twee mensen die klaarstaan om te praten, dat uiteindelijk ook doen. Ze gaan er niet van uit dat het universum kwaadaardig is; ze gaan er gewoon van uit dat als een deur openstaat, er uiteindelijk iemand doorheen zal lopen.

5. Het Resultaat

De auteurs schreven ongeveer 14.000 regels code in Rocq. Dit is niet zomaar een theorie; het is een geverifieerd, machinegecontroleerd bewijs.

Ze zeiden niet zomaar: "Het lijkt erop dat het werkt."
Ze lieten de robotwiskundige elke stap van de logica controleren om ervoor te zorgen dat er geen gaten in het argument zitten.

Samenvatting

In eenvoudige termen zegt dit artikel: "We hebben een robot-proof systeem gebouwd dat garandeert dat als je je communicatieregels voor meerdere personen ontwerpt vanuit één enkel Meesterplan, iedereen aan de beurt komt om te spreken, niemand voor altijd vastzit te wachten en iedereen elkaar begrijpt."

Dit is de eerste keer dat deze specifieke "Levendigheid"-garantie volledig is geverifieerd door een computerbewijshulp voor dit type systeem, waardoor een complex wiskundig concept is omgezet in een gecertificeerd, betrouwbaar feit.

Technische Samenvatting: Formeel Geverifieerde Lichtheid met Multiparty Session Types in Rocq

Probleemstelling
Multiparty Session Types (MPST) bieden een type-discipline voor het specificeren van berichtoverdrachtsprotocollen die meerdere deelnemers betrekken. Hoewel MPST's bekend staan om het garanderen van eigenschappen zoals communicatieveiligheid en afwezigheid van deadlock, blijft het waarborgen van lichtheid (ook wel lock-freedom of starvation-freedom genoemd) een aanzienlijke uitdaging. Lichtheid vereist dat als een proces wacht om te zenden of te ontvangen, er uiteindelijk een communicatie plaatsvindt die dit proces betrekt. Bestaande literatuur vertrouwt vaak op informele bewijzen voor lichtheid, met name in de top-down aanpak waarbij een globaal type wordt geprojecteerd op lokale types. Bovendien hebben eerdere mechaniseringen van MPST (bijvoorbeeld in Rocq/Coq) nog geen formeel bewijs van lichtheid voor synchrone multiparty sessies geboden, noch hebben zij de specifieke "associatie"-relatie gemecaniseerd die lokale type-omgevingen koppelt aan globale types om deze eigenschappen te garanderen.

Methodologie
De auteurs presenteren een formalisering van een synchroon MPST-systeem binnen de Rocq Bewijshulpmiddel (voorheen Coq). De methodologie rust op de volgende kerncomponenten:

Co-inductieve Representatie: Op basis van recent werk van Ekici et al. stelt het systeem globale en lokale types voor als co-inductieve bomen. Deze equirecursieve aanpak maakt directe manipulatie mogelijk van oneindige typebomen die worden verkregen door het ontvouwen van geguardede syntactische types.
De Associatie-relatie ( $\sqsubseteq$ ): De auteurs definiëren een relatie tussen een lokale type-omgeving (een mapping van deelnemers naar lokale types) en een globaal type. Deze relatie wordt vastgesteld via:
- Projectie: Een co-inductieve plain-merge projectie die globale types relateert aan lokale types.
- Subtyping: Een co-inductieve subtyping-relatie op lokale types.
- Balans: Een regulariteitsvoorwaarde op globale types die garandeert dat elke deelnemer vaak genoeg voorkomt op paden om oneindige starvation te voorkomen.
Operationele Correspondentie: De auteurs definiëren Labelled Transition System (LTS) semantiek voor zowel lokale type-omgevingen als globale types. Zij bewijzen dat als een lokale omgeving geassocieerd is met een globaal type, hun reductiesequenties overeenkomen (geluidheid en volledigheid van associatie).
Lichtheid via Lineaire Temporele Logica (LTL) en Paco:
- Lichtheid en eerlijkheid worden gedefinieerd over uitvoeringssporen (co-inductieve streams).
- De auteurs maken gebruik van de Paco-bibliotheek voor geparametriseerde co-inductie. Dit stelt hen in staat eerlijkheids- en lichtheidspredicaten te definiëren als gemengde inductief-co-inductieve relaties, waardoor de niet-compositionele syntactische guardedness-checks van native cofix-tactieken worden vermeden.
- Eerlijkheid wordt geformaliseerd met LTL-operatoren (specifiek eventually en always), waarbij wordt gegarandeerd dat geactiveerde communicaties uiteindelijk worden uitgevoerd.
Enttechniek (Grafting): Om bewijzen op oneindige bomen te hanteren, maken de auteurs gebruik van een "grafting"-techniek. Zij ontleden gebalanceerde globale types in eindige "g-contexten" (voorvoegsels met gaten) en oneindige subbomen. Dit maakt het mogelijk bewijzen per co-inductie op oneindige bomen om te zetten in bewijzen per inductie op de hoogte van eindige g-contexten.

Belangrijkste Bijdragen

Eerste Gemecaniseerd Bewijs van Lichtheid: Dit werk presenteert het eerste gemecaniseerde bewijs van lichtheid voor synchrone multiparty session types in een bewijshulpmiddel.
Mecanisatie van de Associatie-relatie: Het is het eerste werk dat een MPST-systeem mecaniseert gebaseerd op de associatie-relatie tussen lokale type-omgevingen en globale types, waarbij de correctheid van het systeem wordt bewezen door eigenschappen van de lokale omgevingen te formaliseren.
Formele Verificatie van Veiligheid en Afwezigheid van Deadlock: De auteurs bewijzen dat sessies getypeerd door een geassocieerde lokale type-omgeving communicatieveilig en deadlock-vrij zijn.
Operationele Correspondentie: Het artikel vestigt een rigoureuze operationele correspondentie tussen de LTS van lokale type-omgevingen en globale types, waarbij wordt aangetoond dat reducties in het ene kunnen worden gekoppeld aan reducties in het andere.
Implementatie: De formalisering bestaat uit ongeveer 14.000 regels Rocq-code, beschikbaar als open-source software.

Resultaten
De auteurs bewijzen drie hoofdtheorema's met betrekking tot sessies die getypeerd zijn door lokale type-omgevingen die geassocieerd zijn met een gebalanceerd globaal type:

Communicatieveiligheid (Theorema 6.5): Getypeerde sessies evolueren zodanig dat als een deelnemer probeert een bericht te zenden met een specifiek label, de ontvangende deelnemer in staat is om dat label te ontvangen.
Afwezigheid van Deadlock (Theorema 6.6): Een getypeerde sessie eindigt of kan altijd een reductiestap uitvoeren; zij bereikt nooit een vastgelopen toestand waarin geen vooruitgang mogelijk is.
Lichtheid (Theorema 6.9): Als een sessie typeerbaar is door een geassocieerde omgeving, is deze levend. Specifiek: als een deelnemer wacht om te zenden of te ontvangen, vindt er uiteindelijk een communicatie plaats die die deelnemer betrekt, mits het uitvoeringspad eerlijk is.

Het bewijs van lichtheid (Theorema 5.8 voor omgevingen en Theorema 6.9 voor sessies) wordt geïdentificeerd als het meest ingewikkelde resultaat. Het verloopt door eerst lichtheid te bewijzen voor de "directe projectie" van het globale type, en vervolgens de associatie-relatie te gebruiken om deze eigenschap te heffen naar elke geassocieerde lokale omgeving. Het bewijs rust op een inductie-invariant gebaseerd op de hoogte van de "grafting" van het globale type.

Betekenis en Claims
Het artikel claimt dat de primaire betekenis ligt in het verduidelijken van vaak informele bewijzen die in de MPST-literatuur worden aangetroffen en het bieden van een gecertificeerde basis voor lichtheideigenschappen in communicatieprotocollen. Door over te stappen van bewijzen met potlood en papier naar een machine-gecontroleerde formalisering, elimineert het werk potentiële gaten in de redenering met betrekking tot oneindig gedrag en eerlijkheidsaannames.

De auteurs merken op dat hun aanpak met geparametriseerde co-inductie en LTL leidt tot compositionele en duidelijke bewijzen, wat moeilijk te bereiken is met standaard syntactische guardedness-checks. Zij positioneren dit werk als een raamwerk dat potentieel kan worden uitgebreid naar andere procescalculus (zoals de $\pi$ -calculus) of verschillende eerlijkheidsaannames, mits de kern eigenschappen van de operationele correspondentie gelden. Het werk claimt niet lichtheid op te lossen voor alle procescalculus of een algemeen algoritme voor lichtheidscontrole te bieden, maar vestigt eerder een geverifieerd typesysteem voor een specifiek synchroon MPST-calculus.