Project Details
Description
The development of complex hard- and software systems is error-prone and costly. One technique that can provide very valuable feedback on the correctness of system designs is model checking. It involves exhaustively analysing a system design to
determine whether it satisfies desirable functional properties. However, it is computationally very demanding. IC3 is currently a state-of-the-art symbolic model checking technique that can analyse large designs in reasonable time, but its limitations still mean that it is not used very commonly for the design of systems today. In this project, we will investigate whether graphics processing units (GPUs) can be employed for IC3.
GPUs offer great potential for parallel computation, while keeping power consumption low. However, not all types of computation can trivially be performed on GPUs, sometimes the algorithms need to be entirely redesigned.
IC3 uses SAT solving, or the solving of Boolean or propositional satisfiability problems, as a subroutine. In the GEARS project (NWO TOP c2 funded), we investigate how SAT solving can be accelerated using GPUs, specifically focussing on SAT problems that stem from model checking. Building on this, we investigate how IC3 can benefit from using GPUs. IC3 is reportedly parallelisable, but how GPUs can be used to do so most effectively is still an open question.
The project potentially has an enormous impact, since IC3 is currently state-of-the-art in symbolic model checking, and SAT solving is used in various model checking techniques.
determine whether it satisfies desirable functional properties. However, it is computationally very demanding. IC3 is currently a state-of-the-art symbolic model checking technique that can analyse large designs in reasonable time, but its limitations still mean that it is not used very commonly for the design of systems today. In this project, we will investigate whether graphics processing units (GPUs) can be employed for IC3.
GPUs offer great potential for parallel computation, while keeping power consumption low. However, not all types of computation can trivially be performed on GPUs, sometimes the algorithms need to be entirely redesigned.
IC3 uses SAT solving, or the solving of Boolean or propositional satisfiability problems, as a subroutine. In the GEARS project (NWO TOP c2 funded), we investigate how SAT solving can be accelerated using GPUs, specifically focussing on SAT problems that stem from model checking. Building on this, we investigate how IC3 can benefit from using GPUs. IC3 is reportedly parallelisable, but how GPUs can be used to do so most effectively is still an open question.
The project potentially has an enormous impact, since IC3 is currently state-of-the-art in symbolic model checking, and SAT solving is used in various model checking techniques.
Layman's description
Het ontwikkelen van complexe hard- en softwaresystemen is erg ingewikkeld en foutgevoelig. Eén techniek om een computer het ontwerp van een dergelijk systeem systematisch door te laten rekenen heet model checking. Daarbij wordt gecontroleerd of het ontwerp voldoet aan gewenste functionele eigenschappen. Het is echter nog niet vanzelfsprekend dat model checking gebruikt wordt tijdens de ontwikkeling van een complex systeem, aangezien het erg hoge gebruikseisen heeft; het vergt veel tijd
en computergeheugen.
In dit project onderzoeken we hoe een state-of-the-art model checking techniek, genaamd IC3, kan worden versneld door gebruik te maken van grafische processoren (GPUs). GPUs waren oorspronkelijk ontworpen voor het snel uitvoeren van videotaken, maar tegenwoordig kunnen deze ook ingezet worden voor andere, intensieve berekeningen. IC3 maakt intensief gebruik van methoden om het zogenaamde vervulbaarheidsprobleem op te lossen. In de eerste helft van het project zullen we ons dan ook richten op het oplossen van dergelijke problemen met GPUs. Nog niet eerder is er onderzocht of model checking problemen uitgedrukt als vervulbaarheidsproblemen en IC3 efficiënt opgelost kunnen worden met behulp van GPUs.
Het vervulbaarheidsprobleem is een zeer fundamenteel wiskundig probleem, dat ten grondslag ligt aan vele praktische beslissings- en optimalisatieproblemen in diverse gebieden van de informatica, zoals
kunstmatige intelligentie, operationeel onderzoek, het ontwerpen van hardware, en het verifiëren van hard- en software. Problemen als het plannen van taken en graafkleuringen
kunnen worden uitgedrukt als vervulbaarheidsproblemen. Het vervulbaarheidsprobleem heeft als invoer een logische propositie, en de vraag is of er een toekenning bestaat van `waar' of
`onwaar' aan de atomaire formules in de propositie, zodanig dat de propositie waar is. Bijvoorbeeld, de propositie ``(p1 of p2) en ((niet p1) of p3)'' is vervulbaar, want als we aan zowel p2 als p3 de waarde `waar' toekennen is de propositie waar. Er zijn geen methoden bekend om vervulbaarheidsproblemen efficiënt op te lossen, maar er zijn wel diverse methoden ontwikkeld die gebruik maken van heuristieken om problemen die in de praktijk voorkomen binnen redelijke tijd op te lossen.
In eerder werk heeft men al gekeken naar de potentie om GPUs in te zetten voor het versnellen van het oplossen van vervulbaarheidsproblemen. Echter, hierbij heeft men zich altijd gericht op vervulbaarheidsproblemen in het algemeen, en het is bekend dat wanneer men zich richt op specifieke varianten van dit probleem, zoals die problemen die voortkomen uit model checking, bepaalde heuristieken niet goed werken, en anderen juist wel. In dit project richten we ons specifiek op model checking problemen. Daarnaast is het bekend dat IC3 parallel uit te voeren is. Tijdens het uitvoeren van IC3 worden vele vervulbaarheidsproblemen gegenereerd, die onafhankelijk van elkaar opgelost kunnen worden. Dit biedt nog een extra mogelijkheid voor parallel rekenen. In tegenstelling tot multi-core processoren, die toestaan om enkele tientallen berekeningen parallel uit te voeren, kan men met GPUs vele duizenden berekeningen tegelijkertijd doen. Er is dan ook een
grote potentie voor het versnellen van model checking met GPUs.
en computergeheugen.
In dit project onderzoeken we hoe een state-of-the-art model checking techniek, genaamd IC3, kan worden versneld door gebruik te maken van grafische processoren (GPUs). GPUs waren oorspronkelijk ontworpen voor het snel uitvoeren van videotaken, maar tegenwoordig kunnen deze ook ingezet worden voor andere, intensieve berekeningen. IC3 maakt intensief gebruik van methoden om het zogenaamde vervulbaarheidsprobleem op te lossen. In de eerste helft van het project zullen we ons dan ook richten op het oplossen van dergelijke problemen met GPUs. Nog niet eerder is er onderzocht of model checking problemen uitgedrukt als vervulbaarheidsproblemen en IC3 efficiënt opgelost kunnen worden met behulp van GPUs.
Het vervulbaarheidsprobleem is een zeer fundamenteel wiskundig probleem, dat ten grondslag ligt aan vele praktische beslissings- en optimalisatieproblemen in diverse gebieden van de informatica, zoals
kunstmatige intelligentie, operationeel onderzoek, het ontwerpen van hardware, en het verifiëren van hard- en software. Problemen als het plannen van taken en graafkleuringen
kunnen worden uitgedrukt als vervulbaarheidsproblemen. Het vervulbaarheidsprobleem heeft als invoer een logische propositie, en de vraag is of er een toekenning bestaat van `waar' of
`onwaar' aan de atomaire formules in de propositie, zodanig dat de propositie waar is. Bijvoorbeeld, de propositie ``(p1 of p2) en ((niet p1) of p3)'' is vervulbaar, want als we aan zowel p2 als p3 de waarde `waar' toekennen is de propositie waar. Er zijn geen methoden bekend om vervulbaarheidsproblemen efficiënt op te lossen, maar er zijn wel diverse methoden ontwikkeld die gebruik maken van heuristieken om problemen die in de praktijk voorkomen binnen redelijke tijd op te lossen.
In eerder werk heeft men al gekeken naar de potentie om GPUs in te zetten voor het versnellen van het oplossen van vervulbaarheidsproblemen. Echter, hierbij heeft men zich altijd gericht op vervulbaarheidsproblemen in het algemeen, en het is bekend dat wanneer men zich richt op specifieke varianten van dit probleem, zoals die problemen die voortkomen uit model checking, bepaalde heuristieken niet goed werken, en anderen juist wel. In dit project richten we ons specifiek op model checking problemen. Daarnaast is het bekend dat IC3 parallel uit te voeren is. Tijdens het uitvoeren van IC3 worden vele vervulbaarheidsproblemen gegenereerd, die onafhankelijk van elkaar opgelost kunnen worden. Dit biedt nog een extra mogelijkheid voor parallel rekenen. In tegenstelling tot multi-core processoren, die toestaan om enkele tientallen berekeningen parallel uit te voeren, kan men met GPUs vele duizenden berekeningen tegelijkertijd doen. Er is dan ook een
grote potentie voor het versnellen van model checking met GPUs.
Short title | GPU Enabled Accelerated Reasoning about System designs |
---|---|
Acronym | GEARS |
Status | Finished |
Effective start/end date | 11/08/17 → 31/01/22 |