ViGARO: Verified Generation of Parallel Software
Summary of the project
The development of software targeted at modern parallel computing hardware, such as multi-core processors and graphics processing units (GPUs), requires expert knowledge about that hardware, and the produced software is often very complex, and therefore hard to reason about. However, the demand for parallel software increases, as it can push the computational boundaries in many fields of research significantly. To make the development of correctly functioning parallel software easier, the MDSE section at the TU/e conducts research on model-driven techniques, in which the intended functionality is first modelled using a domain-specific language (DSL). Next, it is mathematically proven, or formally verified, that such a model indeed describes the intended functionality, and once this is the case, software code is automatically generated via a model-to-code transformation. However, in order for this approach to be effective, it must also be mathematically proven that the transformation produces for any input model correct code that corresponds with the functionality described by that model. Together with Wijs, Zhang has conducted research on formally verifying that DSL concepts semantically correspond with the software constructs mapped to those concepts by a given model transformation. This represents the first step in proving that a model-to-code transformation is correct. Through her PhD research, Zhang has become an expert on both this step and the generation of parallel software.
For the next step, it must be verified that a transformation always combines software constructs into a complete program in line with how the corresponding DSL concepts are combined in the input model. How to do this is a big challenge. In the FMT group at UT, the group of Huisman performs research on the verification of software code. Specifically, they work on specifying the intended functionality and verifying that the code adheres to this. Expertise on program verification will be crucial to make the next step a success, but not sufficient, since verifying a program is conceptually different from verifying a transformation that produces programs as output.
To address this challenge in the ViGARO project, the experience on model transformations in the MDSE section, specifically of Wijs and Zhang, will be combined with the expertise on program verification in the group of Huisman. Only with the combined experience on these two topics will it be possible to effectively address the challenge; how to produce code and how to verify code are the two tightly-connected concerns. We will first investigate how transformations can best be expressed to formally reason about the transformation of combinations of DSL concepts into combinations of software constructs. After this, we will work on the development of an approach based on program verification to verify such transformation descriptions.