💻 computer science

Reasoning about concurrent loops and recursion with rely-guarantee rules

Dit artikel presenteert mechanisch geverifieerde, algemene verfijningsregels voor het redeneren over recursieve programma's en while-loops in concurrente systemen met behulp van de rely-guarantee-benadering, zonder uit te gaan van atomaire expressie-evaluatie.

Oorspronkelijke auteurs: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

Gepubliceerd 2026-06-12

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

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 voor dat je een recept probeert te schrijven voor een team van chefs die in een chaotische, gedeelde keuken werken. Iedereen is tegelijkertijd aan het snijden, roeren en proeven. Het probleem is dat terwijl Chef A een stap uit het recept leest, Chef B er tussendoor kan komen om een ingrediënt te verplaatsen, de temperatuur te veranderen of een hulpmiddel te verstoppen. Dit is de wereld van concurrente programmering: meerdere programma's die tegelijkertijd draaien en elkaars gegevens verstoren.

Dit artikel van Hayes, Meinicke en Jones is als een nieuw, ultra-strikt regelboek voor het schrijven van deze recepten, zodat ze gegarandeerd werken, zelfs in de chaos. Ze richten zich op twee specifieke soorten kookinstructies: loops (iets herhaaldelijk doen) en recursie (een recept dat zichzelf aanroept om een kleiner deel van het probleem op te lossen).

Hier is de uitsplitsing van hun "keukenregels" met behulp van eenvoudige analogieën:

1. Het "Rely-Guarantee" Pact

In een normale keuken ga je er gewoon van uit dat niemand aan je pan komt. In dit artikel zeggen de auteurs: "Vertrouwen is niet genoeg. We hebben een contract nodig."

De Rely-voorwaarde (De "Niet Aanraken"-lijst): Voordat je aan je taak begint, ga je ervan uit dat de andere chefs zich aan bepaalde regels houden. Bijvoorbeeld: "Ik vertrouw erop dat niemand zout aan mijn soep toevoegt terwijl ik aan het proeven ben."
De Guarantee-voorwaarde (De "Ik Beloof"-lijst): In ruil daarvoor beloof je dat jij ook regels zult volgen. "Ik garandeer dat ik nooit mijn lepel tegen de muur zal gooien."
De Magie: Als iedereen hun "Rely" en "Guarantee" contracten naleeft, verloopt de hele keuken soepel, zelfs als ze allemaal tegelijkertijd aan het werk zijn.

2. Het Probleem met "Atomaire" Aannames

Veel oude regelboeken gingen ervan uit dat wanneer een chef een stap in een recept leest, hij dit onmiddellijk doet, zoals een magische knip met de vingers. Ze namen aan dat de chef leest "Voeg 2 eieren toe" en de eieren toevoegt voordat iemand ook maar kan knipperen.

De auteurs zeggen: "Nee, dat is niet hoe echte keukens werken."
In werkelijkheid kost het lezen van "Voeg 2 eieren toe" tijd. Terwijl de chef naar de eieren reikt, kan een andere chef de doos verplaatsen. Dit artikel bouwt regels die rekening houden met deze rommelige realiteit. Ze gaan er niet vanuit dat alles onmiddellijk gebeurt; ze gaan ervan uit dat alles een beetje tijd kost en onderbroken kan worden.

3. Het Temmen van de "While"-loop (Het Nooit-eindigende Roeren)

Een "while loop" is als een chef die in een pan roert "totdat de saus dik is".

Het Oude Probleem: In een gedeelde keuken kan een chef roeren, de saus controleren en besluiten dat deze nog niet dik genoeg is. Maar terwijl de chef naar het fornuis loopt, voegt een andere chef water toe, waardoor de saus weer dun wordt. De eerste chef blijft misschien eeuwig doorroeren, of stopt juist wanneer hij dat niet zou moeten doen.
De Nieuwe Regel (Vroegtijdige Beëindiging): De auteurs introduceren een slimme truc genaamd "Early Termination" (Vroegtijdige Beëindiging).
- Stel je voor dat de chef een timer heeft (een "variant"). Elke keer dat hij roert, gaat de timer omlaag.
- Normaal gesproken moet de chef roeren om de timer omlaag te laten gaan.
- De Twist: Als een andere chef per ongeluk water toevoegt (interferentie), kan de timer sneller omlaag gaan dan verwacht, of kan de saus plotseling dik genoeg worden zodat de loop zou moeten stoppen.
- De nieuwe regel staat toe dat de loop voortijdig stopt als de omgeving (de andere chefs) helpt om de taak te voltooien, in plaats van de loop te dwingen al het werk zelf te doen. Het is als zeggen: "Als de saus al dik is omdat iemand anders heeft geholken, kun je direct stoppen met roeren."

4. Het Temmen van Recursie (Het Recept dat Zichzelf Aanroept)

Recursie is als een chef die zegt: "Om deze grote stoofpot te maken, moet ik eerst een kleine batch bouillon maken. Om die bouillon te maken, moet ik een heel klein beetje bouillon maken..."

De Uitdaging: In een gedeelde keuken kan Chef A de bouillon aan het maken zijn, terwijl Chef B de bouillonpan steelt.
De Oplossing: De auteurs hebben een wiskundige "ladder" gecreëerd (een well-founded relation). Stel je voor dat de chef een ladder afdaalt om steeds kleinere problemen op te lossen.
- De Regel: Je mag alleen de ladder afdalen als je zeker weet dat je niet vast komt te zitten.
- De "Early Exit"-truc: Net als bij de loops, als de andere chefs je helpen om sneller bij de onderkant van de ladder te komen (door een sub-probleem voor je op te lossen), mag je eerder stoppen met afdalen. Je hoeft niet elke stap zelf te forceren als de omgeving helpt om je taak te voltooien.

5. De "Aczel Trace" (De Keukenbeveiligingscamera)

Om te bewijzen dat hun regels werken, gebruiken de auteurs een concept genaamd een Aczel trace.

Stel je een beveiligingscamera voor die de keuken opneemt.
De camera registreert twee soorten bewegingen: Programma-bewegingen (wat de chef die jij observeert doet) en Omgevings-bewegingen (wat de andere chefs doen).
De regels van de auteurs zorgen ervoor dat, ongeacht hoe de camera de chaos registreert, het eindresultaat perfect is, mits de "Rely" en "Guarantee" contracten worden nageleefd.

Samenvatting

Dit artikel biedt een nieuwe, robuuste manier om instructies te schrijven voor computerprogramma's die tegelijkertijd draaien.

Geen Magie: Het stopt met de aanname dat dingen onmiddellijk gebeuren.
Contracten: Het gebruikt "Rely" en "Guarantee" om de interactie tussen programma's te beheren.
Flexibiliteit: Het staat loops en recursieve functies toe om voortijdig te stoppen als de omgeving helpt om de taak te voltooien, wat voorkomt dat ze in oneindige loops terechtkomen of falen door interferentie.

De auteurs hebben hun regels al getest met een computergestuurde bewijsassistent (Isabelle/HOL), die fungeert als een superstrikte wiskundeleraar die elke stap controleert om te garanderen dat de logica foutloos is. Ze hebben niet alleen gegokt; ze hebben bewezen dat het werkt.

Technische Samenvatting: Redeneren over Concurrente Loops en Recursie met Rely-Guarantee Regels

Probleemstelling

De verificatie van concurrente programma's, in het bijzonder die met recursieve structuren en while-loops, staat voor aanzienlijke uitdagingen wanneer te maken wordt gekregen met interferentie van parallelle threads. Traditionele Hoare-stijl verificatieregels voor loops vertrouwen op invarianten en variant-expressies om correctheid en terminatie te bewijzen. Echter, in een concurrente setting kan interferentie loop-invarianten ongeldig maken, variant-expressies vergroten, of de evaluatie van loop-guards verstoren, waardoor standaard sequentiële regels ongeldig worden.

Bovendien gaan veel bestaande Rely-Guarantee (RG) benaderingen ervan uit dat de evaluatie van expressies atomair is. Deze aanname weerspiegelt niet de realiteit van implementaties van programmeertalen, waarbij expressies mogelijk meerdere toegangen naar gedeelde variabelen bevatten die onderbroken kunnen worden door de overgangen van de omgeving. Deze atomiciteitsaanname verbreekt de formele redeneerketen voor complexe expressies en beperkt de toepasbaarheid van de verificatieregels.

Methodologie

De auteurs ontwikkelen een framework voor het redeneren over recursieve programma's en while-loops binnen een Rely-Guarantee context, gebruikmakend van een breed-spectrum taal gebaseerd op een volledige distributieve rooster van commando's. De methodologie is gestoeld op de volgende kerncomponenten:

Aczel Trace Semantiek: Het semantische model gebruikt verzamelingen van Aczel-traces, die sequenties van programma- ( $\pi$ ) en omgeving- ( $\epsilon$ ) transities vastleggen. Dit maakt een compositionele behandeling van interferentie mogelijk zonder de atomiciteit van expressie-evaluatie of assignment-commando's te veronderstellen.
Rely-Guarantee Condities: Het framework gebruikt rely-condities ( $r$ ) om het gedrag van de omgeving te beperken en guarantee-condities ( $g$ ) om het gedrag van het programma te beperken. De guarantee van een thread moet de rely-conditie van alle parallelle threads impliceren.
Vaste-punt Theorie (Fixed-Point Theory): Recursieve programma's worden gedefinieerd als vaste punten over een rooster van commando's. De auteurs ontwikkelen wetten voor het redeneren over deze vaste punten, specifiek gebruikmakend van welgevormde inductie met variant-expressies en relaties om terminatie te bewijzen.
Vroege Terminatie (Early Termination): Een centrale methodologische innovatie is de ontwikkeling van "vroege terminatie"-versies van wetten voor zowel recursie als loops. In tegenstelling tot standaard benaderingen die vereisen dat de variant strikt wordt verminderd door de functiebody voordat er recursieve aanroepen plaatsvinden, staan deze wetten toe dat de functiebody óf de variant vermindert, óf een conditie vaststelt (een basisgeval) die garandeert dat er geen verdere recursieve aanroepen worden gemaakt. Dit is cruciaal voor concurrency, waar interferentie de variant op een manier kan verminderen die een verdere reductie door de functiebody onmogelijk maakt, maar toch terminatie waarborgt.
Niet-atomaire Expressie-evaluatie: De benadering behandelt expliciet de niet-atomaire evaluatie van expressies. Het gebruikt een compositionele methode om postcondities voor complexe expressies vast te stellen door hun sub-expressies te analyseren, waardoor de noodzaak voor syntactische restricties zoals de "single critical reference" uit atomaire-aanname-theorieën wordt vermeden.

Belangrijkste Bijdragen

Het artikel presenteert verschillende specifieke bijdragen aan de theorie van concurrente programmaverificatie:

Algemene Verfijningsregels voor Recursie: Stelling 5 ("recursion-early") biedt een regel voor het introduceren van recursie die interferentie accommodeert. Het gebruikt een welgevormde relatie en een variant-expressie, waardoor terminatie bewezen kan worden zelfs als de variant wordt verminderd door de omgeving in plaats van door de functiebody, mits een basisgeval wordt vastgesteld.
Algemene Verfijningsregels voor While Loops: Stelling 6 ("intro-while") leidt een wet af voor het introduceren van while-loops gebaseerd op de recursie-wet. Het bevat een "vroege terminatie"-conditie ( $p_X$ ) die de loop toestaat te stoppen als de guard ongeldig wordt door interferentie, zelfs als de loopbody de variant niet strikt heeft verlaagd.
Afhandeling van Niet-atomaire Expressies: Het framework biedt inferentieregels (bijv. Stelling 2 voor conditionalen, Stelling 3 voor functieaanroepen) die compositioneel redeneren over expressies en guards onder interferentie mogelijk maken zonder de evaluatie van expressies als atomair te veronderstellen.
Formele Verificatie: Alle lemma's en stellingen gepresenteerd in het artikel zijn mechanisch geverifieerd met de Isabelle/HOL theorem prover.
Eerlijke Terminatie (Fair Termination): Het artikel behandelt eerlijke terminatie door een commando fair te definiëren dat oneindige opeenvolgende sequenties van omgeving-transities verbiedt, en toont aan hoe te bewijzen dat een commando slechts een eindig aantal transities uitvoert onder eerlijke executie.

Resultaten en Voorbeelden

Het artikel demonstreert het nut van de ontwikkelde wetten via twee primaire voorbeelden:

Parallel Recursieve Zoekopdracht: Een recursief zoekalgoritme wordt ontwikkeld om een waarde $i$ in een bereik $[0, N)$ te vinden die aan een predicaat $P$ voldoet. De implementatie gebruikt een divide-and-conquer strategie met parallelle recursieve aanroepen. Het bewijs maakt gebruik van de "recursion-early" wet om het geval af te handelen waarin een concurrente thread al een oplossing heeft gevonden (het instellen van een found flag), waardoor de recursieve aanroepen vroegtijdig kunnen stoppen zonder verdere verwerking.
Atomaire Update met CAS: Een voorbeeld van het implementeren van een atomaire specificatie om een variabele $m$ te updaten naar $\min(m, lo)$ met behulp van een Compare-And-Swap (CAS) instructie. De loop probeert de CAS herhaaldelijk uit te voeren. De "vroege terminatie"-versie van de loop-wet is hier essentieel: als interferentie $m$ verlaagt onder $lo$ tussen de guard-check en de uitvoering van de CAS, kan de CAS er niet in slagen om $m$ (de variant) te verlagen. Echter, de loop termineert omdat de guard ($lo < m$) onwaar wordt. De standaard loop-wet zou falen in het bewijzen van terminatie in dit scenario, maar de voorgestelde wet slaagt door de vroege exit-conditie te herkennen.

Betekenis en Claims

De auteurs claimen dat hun werk algemene, mechanisch geverifieerde verfijningsregels biedt voor het redeneren over recursie en loops in aanwezigheid van concurrency. De significantie van dit werk ligt in:

Verwijderen van Atomiciteitsaannames: Door niet te veronderstellen dat expressie-evaluatie atomair is, zijn de regels toepasbaar op een breder scala aan realistische programmeerscenario's en voorkomen ze het verbreken van de formele redeneerketen die optreedt in theorieën die op atomiciteit vertrouwen.
Afhandeling van Interferentie in Terminatiebewijzen: De "vroege terminatie"-wetten pakken een specifiek gat aan in concurrente verificatie, waar interferentie standaard terminatie-argumenten ongeldig kan maken. Dit maakt de verificatie mogelijk van programma's waarbij de acties van de omgeving bijdragen aan de terminatieconditie.
Compositionele Ontwikkeling: De benadering ondersteunt de compositionele ontwikkeling van gedeelde-variabele concurrente programma's, waardoor threads onafhankelijk van elkaar ontworpen en geverifieerd kunnen worden op basis van hun rely en guarantee condities.
Formele Rigor: De resultaten zijn niet louter theoretische voorstellen, maar zijn geformaliseerd en geverifieerd binnen de Isabelle/HOL theorem prover, wat hun logische juistheid garandeert.

Het artikel positioneert zich als een uitbreiding van eerder algebraïsch Rely-Guarantee onderzoek, specifiek gericht op de complexiteiten die worden geïntroduceerd door recursie, loops en niet-atomaire expressie-evaluatie in concurrente systemen. Het claimt niet andere logica's zoals Concurrent Separation Logic (CSL) te vervangen, maar biedt een alternatieve compositionele methode, waarbij expliciet wordt opgemerkt dat hoewel CSL ondersteuning biedt voor redeneren over race-vrijheid, RG is ontworpen voor de ontwikkeling van "racy" programma's (programma's waarbij races worden beheerd via rely/guarantee condities).