1429440_76508562 (1)

Een softwarefout kan dodelijk zijn. En softwarefouten zitten soms op onverwachte plekken: snellere en geavanceerdere computers zijn bijvoorbeeld een belangrijke oorzaak. Marieke Huisman, onderzoeker aan de Universiteit Twente, helpt programmeurs zich tegen deze softwarefouten te beschermen. Als een ware wapensmid probeert zij hen het gereedschap te geven onbedoelde fouten uit hun code te verdrijven.

Honderd keer meer dan de veilige hoeveelheid: zo groot was de stralingsoverdosis die de Therac-25 toediende aan zes Amerikaanse en Canadese patiënten tussen 1985 en 1987. De Therac-25 was een medische stralingsmachine om kankerpatiënten mee te behandelen, maar na deze overdosis stierf de helft van de patiënten. In tegenstelling tot zijn voorgangers had de Therac-25 geen mechanische beveiliging om overdoses te voorkomen, maar alleen een beveiliging in de software. Door een fout in de parallelle software van de Therac-25 ging het in totaal zes keer mis. Bij drie van de ongevallen overleefde de patiënt het niet.

Twee tegelijk

Parallelle software is een flinke stap vooruit in de snelheid van een computer: daarmee kan een computer twee of meer acties tegelijkertijd uitvoeren. Voorheen ging bij software alles gewoon één voor één. Pas als de eerste regel code verwerkt was begon de computer aan de tweede, dan pas de derde, enzovoort. Software die zo werkt heet sequentiële software, en was vroeger de enige soort software in gebruik: tot 2001 hadden de meeste commerciële computers maar één processor.

Maar tegenwoordig zitten in eigenlijk alle computers minstens twee processors — dat worden ook wel multicore-computers genoemd. Dankzij extra processors kunnen computers makkelijk twee dingen tegelijk doen, of juist samen één opdracht sneller uitvoeren. “Ook telefoons zijn tegenwoordig allemaal multicore”, legt informaticus Marieke Huisman uit, “Als je een spelletje speelt, wil je niet een telefoontje missen.”

Huisman is hoofddocent Methode en Tools aan de Universiteit Twente. Sinds 2011 staat zij bovendien aan het hoofd van het project ‘Verification of concurrent data structures’ (VerCors). VerCors is een door de Europese gemeenschap gesubsidieerd initiatief om onderzoek te doen naar manieren om parallelle software betrouwbaarder te maken door gebruik van verificatieprogramma’s.

Racende Bytes

Dit onderzoek is nodig omdat met deze nieuwe multicore-computers er ook nieuwe problemen bij zijn gekomen. “Bepaalde acties kunnen tegelijkertijd gebeuren, terwijl die niet tegelijkertijd mogen gebeuren.” zegt Huisman. Wanneer dit toch gebeurt, heet dat een data race. Twee processors racen als het ware naar dezelfde plek in het geheugen om die als eerste aan te passen. Als dit dan in een andere volgorde gebeurt dan de programmeur had verwacht, kan dit fouten opleveren: “Stel bijvoorbeeld dat processor één iets wil delen door een getal in het geheugen en processor twee heeft dat net daarvoor in een 0 veranderd. Dan gaat het fout.”

Dit was ook wat er gebeurde bij de Therac-25. Het was voor het invoerstation mogelijk om dingen in het geheugen te wijzigen terwijl de software nog bezig was met een andere taak.

En dit soort kleine softwarefouten kunnen grote problemen opleveren. Naast problemen met bestralingsmachines, waren er in 2010 ook problemen met de remmen van de Toyota Prius. Door een softwarefout in het antiblokkeringssysteem werkten de remmen soms niet goed. Dat heeft uiteindelijk tot vier ongevallen geleid.

“Dit soort fouten kan bedrijven veel geld kosten, en soms zelfs levens,” zegt Huisman. “De schatting is dat als deze bedrijven betere technieken hadden om hun software te controleren, ze dat dan 40% van de kosten zou schelen. Kosten veroorzaakt door de herstelkosten van deze softwarefouten. Daar blijft gewoon geld liggen.”

Een helpende hand

Om programmeurs te helpen met parallelle software en data races werkt Huisman aan speciale verificatietools voor parallelle software. Een verificatietool wordt gebruikt om fouten en problemen in code op te sporen. Deze tools kijken naar specificaties die een programmeur moet toevoegen aan zijn code.

Specificaties zijn stukken tekst die niet direct onderdeel van de code zijn. Deze tekst beschrijft aannames van de programmeur over waar bepaalde onderdelen van het programma aan voldoen. Zo kan een programmeur met een specificatie zeggen: “Ik denk dat hier getal X nooit negatief kan zijn”. Een verificatietool voert dan logische berekeningen uit om te controleren of de geschreven code zich hier ook aan houdt, zonder dat de code ook echt wordt uitgevoerd. Mocht bijvoorbeeld getal X op een bepaalde manier toch negatief kunnen worden, dan slaat de tool alarm.

Dit soort verificatietools bestaan al voor sequentiële software en worden goed begrepen. Maar voor parallelle software zijn ze nog niet goed uitgezocht. Bij parallelle software moet er namelijk ook rekening worden gehouden met alle mogelijke volgordes waarin de code kan worden uitgevoerd. Vooral welke specificaties het beste werken bij parallelle software is iets waar Huisman mee bezig is: “Het is de kunst de juiste specificaties te vinden”, vertelt Huisman “als je die eenmaal hebt, weet je hoe je die goed met een tool kunt toepassen”.

Eén van technieken die Huisman verder aan haar tools probeert toe te voegen heet separation logic. Hierbij krijgen verschillende processen die de processors uitvoeren toestemming om bepaalde delen van het geheugen te veranderen of alleen te lezen. Door er voor te zorgen dat nooit meer dan één proces toestemming heeft een bepaalde plek in het geheugen aan te passen, worden sommige data races voorkomen.

Als dit soort tools waren gebruikt tijdens de ontwikkeling van de Therac-25, was een hoop leed ongetwijfeld voorkomen. De verificatietools hadden de mogelijke data races ontdekt, en de programmeurs hier voor gewaarschuwd.

Voorlopig hebben Huisman en haar team dus nog genoeg te doen, en is het onderzoek nog lang niet afgerond. Huisman heeft wel een duidelijk doel voor ogen: “Uiteindelijk wil ik dat iemand die programmeert, intuïtief met mijn technieken zijn of haar software kan controleren. Dat is voor mij de uitdaging”.

Rogier van de Blaak is student van de EC-master van de Faculteit Wiskunde & Natuurwetenschappen van de Rijkuniversiteit Groningen, en schreef dit interview als onderdeel van het vak Achtergrond Bèta-onderzoek.