| Correctheid in een gelijktijdig programma is aanzienlijk complexer dan in een opeenvolgend programma vanwege de toegevoegde dimensies van timing, interleaving en gedeelde bronnen. Een gelijktijdig programma wordt als correct beschouwd als het aan zijn specificatie voldoet *ongeacht de planning van de gelijktijdige threads of processen*. Dit betekent dat het programma de verwachte uitvoer produceert en het gewenste gedrag vertoont onder alle mogelijke uitvoeringsinterleavings.
Verschillende aspecten dragen bij aan de definitie van correctheid in een gelijktijdig programma:
* Veiligheid: Het programma komt nooit in een ongeldige toestand. Dit omvat het vermijden van problemen zoals:
* Dataraces: Meerdere threads die dezelfde gedeelde geheugenlocatie benaderen en wijzigen zonder de juiste synchronisatie, wat tot onvoorspelbare resultaten leidt.
* Pauzes: Twee of meer threads worden voor onbepaalde tijd geblokkeerd, in afwachting van elkaar om bronnen vrij te geven.
* Livelocks: Threads veranderen voortdurend van status als reactie op elkaar, maar geen enkele boekt vooruitgang.
* Verhongering: Aan een of meer threads wordt voortdurend de toegang tot een gedeelde bron ontzegd.
* Raceomstandigheden: De uitkomst hangt af van de onvoorspelbare volgorde waarin threads worden uitgevoerd.
* Levendigheid: Het programma boekt uiteindelijk vooruitgang en wordt beëindigd als dat zou moeten. Dit houdt onder meer in dat ervoor wordt gezorgd dat:
* Threads verwerven uiteindelijk de noodzakelijke hulpbronnen.
* Het programma bereikt uiteindelijk een eindstatus.
* Functionaliteit: Het programma produceert de juiste uitvoer en bereikt het beoogde doel. Dit is vergelijkbaar met sequentiële programma's, maar wordt gecompliceerd door de gelijktijdige uitvoering ervan. Het eindresultaat moet consistent zijn in alle mogelijke uitvoeringsscenario's.
Daarom impliceert het bewijzen van de juistheid van een gelijktijdig programma doorgaans het aantonen dat:
1. Alle mogelijke interleavings van threaduitvoeringen leiden tot een geldige eindstatus. Dit is ongelooflijk uitdagend en vaak onpraktisch om uitputtend te doen.
2. Het programma is vrij van veiligheidsschendingen (impasses, dataraces, enz.). Dit wordt vaak aangepakt door een zorgvuldig ontwerp en het gebruik van synchronisatiemechanismen (mutexen, semaforen, monitoren, enz.).
3. Het programma voldoet aan zijn levendigheidseigenschappen. Dit betekent dat je moet aantonen dat het programma uiteindelijk zijn taken zal voltooien en niet in een oneindige lus of impasse zal blijven steken.
Samenvattend betekent correctheid bij gelijktijdig programmeren het garanderen van voorspelbaar en betrouwbaar gedrag in alle mogelijke uitvoeringsschema's. Dit vereist nauwgezette aandacht voor synchronisatie, resourcebeheer en rigoureuze test- en verificatietechnieken. Voor rigoureuze verificatie kunnen formele methoden worden gebruikt, maar deze zijn vaak rekentechnisch duur en alleen toepasbaar op kleinere programma's. Daarom is meestal een combinatie van zorgvuldig ontwerp, testen en mogelijk formele verificatie vereist om de juistheid van een gelijktijdig programma te garanderen. |
