Technieuws

Europese miljoenensubsidie voor Twentse verificatie multithreaded software

Pieter Edelman
Leestijd: 2 minuten

De European Research Council kent 1,3 miljoen euro toe aan UT-onderzoeker Marieke Huisman voor een project rond formele verificatie van multithreaded software. Met het geld moeten twee promovendi en twee postdocs aan de slag gaan. ’Ik heb een achtergrond in verificatie van sequentiële programma‘s‘, vertelt Huisman. ’De volgende stap is om te laten zien dat dat ook werkt voor multithreaded software.‘ Het project zal nieuwe theorie ontwikkelen, maar Huisman benadrukt dat het vooral ook praktische resultaten moet opleveren in de vorm van tools.

Het Vercors-project (Verification of Concurrent Data Structures) bouwt voort op eerder onderzoek waarbij verificatie is toegepast op een van de manieren waarop threads in Java data kunnen vergrendelen. Vergrendeling van specifieke datastructuren is een essentieel onderdeel bij de ontwikkeling van multithreaded software. Zo is het zaak te voorkomen dat twee threads tegelijkertijd dezelfde variabele proberen te beschrijven, of dat de ene thread een variabele inleest voordat de andere de juiste waarde heeft geschreven. Door een lock op een variabele te zetten, claimt een thread deze voor zichzelf totdat hij er klaar mee is. Zolang kunnen andere threads niet of beperkt bij de variabele.

’In het project willen we daar veel verder in gaan‘, vertelt Huisman. ’Over reentrant locks kunnen we nu redeneren, maar je hebt ook andere synchronisatiemethodes. We willen onze theorie daarnaar uitbreiden.‘ Ook gaat het project kijken of de theorie is toe te passen op C. ’Dat is wel een uitdaging. C heeft een veel onduidelijkere semantiek. Daar willen we wel naar kijken.‘ De focus ligt echter op Java.

This article is exclusively available to premium members of Bits&Chips. Already a premium member? Please log in. Not yet a premium member? Become one and enjoy all the benefits.

Login

Related content