NWO TOP C1 grant for Jan Friso Groote, Tim Willemse, and Anton Wijs
Prof.dr.ir. Jan Friso Groote, dr.ir. Tim Willemse, and dr.ing. Anton Wijs received an NWO TOP C1 grant for the project “Accelerated Verification and Verified Acceleration”. In collaboration with the University of Amsterdam (prof.dr. Rob van Nieuwpoort) and VU Amsterdam (dr. Pieter Hijma), three PhD candidates are being appointed to study the integration of two individually successful techniques: stepwise refinement for performance, and model checking. In this research project, the two different approaches are combined to examine how “verification can be accelerated” and how “acceleration can be verified”.
It is not that long ago that computers had one single-core processor which only processed computational instructions in a serial manner. Over the years, these single-core processors have been increasingly replaced by multi-core and many-core processors such as GPU’s. While these new processors offer increased computational power, parallel computing may also be a source of problems. Many popular programming languages are not designed with concurrency in mind, and therefore it is extremely difficult to orchestrate correct behavior of the software in parallel execution, while at the same time optimizing the overall performance of the software.
Stepwise refinement for performance
Dr. Pieter Hijma has been working on a technique to refine software step by step to increase performance on many-core architectures. With this technique, a parallel system is initially programmed at a high level of abstraction and gradually tailored to the strength and specific properties of the hardware. The question remains whether we can guarantee these refinements are not changing the functionality of the software.
In that area lies the expertise of the group of prof. Jan Friso Groote at the Eindhoven University of Technology, where the only Dutch full-fledged model checker has been developed. A model checker checks whether correctness properties hold true when evaluated against all possible executions of a program. In case of an unsuccessful run, the model checker will indicate where exactly the problem is. While improving the quality of the software, model checking is computationally very intensive.
Accelerated Verification and Verified Acceleration
Combining stepwise refinement and model checking brings major advantages for both fields. Model checking the stepwise refinements ensures that no unintended changes in software behavior occur while tuning the software for many-core processors (verified acceleration). At the same time model checking will profit from using stepwise refinement to better utilize the many-core processors for its computations, making it possible to analyze more complicated models faster (accelerated verification).