Compositional verification of parallel programs using epistemic logic and abstract assertional languages

Abstract

Het schrijven van foutenvrije computerprogramma's (software) blijkt nog steeds geen eenvoudige opgave. Incorrecte software kan aanleiding geven tot ongewenste, kostbare en soms zelfs levensbedreigende situaties. Parallelle programma's, dat wil zeggen programma's geschreven voor een systeem bestaande uit meerdere, tegelijkertijd opererende processoren, zijn in dit opzicht alleen maar lastiger: de interactie tussen de verschillende processoren compliceert de zaak. Het vastleggen van de eigenschappen waaraan een programma moet voldoen gebeurt door middel van het opstellen van een (formele) specicatie. Een van de methoden om te garanderen dat een programma voldoet aan zijn specicatie is het leveren van een (wiskundig) bewijs hiervan. Het formaat waarin zo'n be- wijs wordt gegeven alsmede de geldigheid van de atomaire bewijsstappen worden beschreven door zogenaamde programmalogica's, ofwel logica's waarin naast de gebruikelijke beweringen (bijvoorbeeld over variabelen) ook de syntax van de programmeertaal een rol speelt. Dit proefschrift richt zich op een specieke klasse van programmalogica's, ook wel Hoare-logica's genoemd naar een van de pioniers op het gebied. Globaal gezien bestaat het proefschrift uit twee delen. Het eerste deel start met een algemene inleiding in kennislogica. Kennislogica kan ruwweg worden beschouwd als eerste orde logica waaraan een modaliteit is toegevoegd die een (geformaliseerde notie van) kennis beschrijft. Het volgende hoofdstuk geeft een overzicht van een aantal manieren waarop dit kennisbegrip vormgegeven kan worden in de context van gedistribueerde, of pa- rallelle systemen. Door datgene wat een processor kan observeren met betrekking tot een complete executie van het gehele systeem van processoren te vari?eren, verkrijgen we een aantal noties van kennis (binnen een gedistribueerd systeem); binnen deze verschillende kennisnoties kunnen we dan een klassicering aanbren- gen met betrekking tot de kracht van die noties. Het laatste hoofdstuk van het eerste deel beschrijft een bewijssysteem met be- hulp waarvan beweringen met betrekking tot de kennis van processoren in een 191?192 SAMENVATTING gedistribueerd systeem kunnen worden afgeleid. Het bewijssysteem, overigens alle bewijssystemen in dit proefschrift, is compositioneel wat er in grote lijnen op neerkomt dat de correctheid van het complete parallelle programma kan worden afgeleid uit de correctheid van de afzonderlijke componenten. In het tweede deel beschouwen we bewijssystemen voor programma's waarin de communicatie tussen de verschillende componenten van een parallel systeem (de processen) niet gelijktijdig verloopt; dit heet ook wel asynchrone communicatie. De algemene doelstelling van dit tweede deel bestaat uit het minimalizeren van de assertietaal , de taal waarmee binnen het bewijssysteem beweringen over de processen (het programma) kunnen worden geformuleerd. Het bepalen van zulke minimale (abstracte) assertietalen biedt voordelen bij het top-down ontwerp van programma's. Het eerste hoofdstuk van het tweede deel laat zien dat het mogelijk is een com- positioneel bewijssysteem te baseren op een assertietaal die de beschrijving van processen alleen toelaat middels de beschrijving van de communicatie-acties per communicatie-kanaal. Hiervoor is het wel vereist dat de programmeertaal in es- sentie deterministisch is. Het volgende hoofdstuk beschrijft een case-study: de correctheid van een gedis- tribueerd algorithme voor het bepalen van de topologie van een netwerk wordt afgeleid. Hierbij maken we gebruik van het bewijssysteem uit hoofdstuk 6 en van PVS, een tool voor het interactief genereren en checken van bewijzen. Zo laten we enerzijds zien hoe de (beperkte) programmeertaal van hoofdstuk 6 toch interessante voorbeelden toestaat, terwijl anderzijds wordt ge?llustreerd hoe de essentie van het bewijs semi-automatisch kan worden afgeleid. Het gebruik van dergelijke tools heeft als voordeel dat triviale details automatisch kunnen worden afgehandeld, zodat de gebruiker zich kan concentreren op de daadwerkelijk lastige bewijsstappen. In het laatste hoofdstuk richten we ons op een niet-deterministische program- meertaal. Ook nu zijn we in staat de assertietaal te beperken ten opzichte van vergelijkbare bewijssystemen. We introduceren de notie van abstract history, die (samen met de communicatie-informatie per kanaal) een abstractie is van de ge- bruikelijke history (een beschrijving van een proces door middel van een volledige opsomming van zijn communicaties). Een bijkomend voordeel hiervan is dat het gedeelte van de logica waarin over deze abstracte histories, en dus over het communicatiegedrag van de processen geredeneerd wordt, beslisbaar is.