University of Twente Student Theses
Deductive verification for SYCL
Wittingen, E.M. (2024) Deductive verification for SYCL.
|
PDF
1MB |
| Abstract: | SYCL is a software development framework with which programs can be developed for heterogeneous computing systems. It uses the concept of kernels, where a kernel executes code inside it in parallel, and different kernels can be executed concurrently on multiple computing units. These concurrent executions mean that the set of possible program behaviours can be of considerable size, which makes it easy to overlook problems. To solve this, formal verification can be performed to ensure a program's correctness. However, there do not seem to exist any formal verification tools for SYCL programs. In this thesis, it is investigated how the deductive verification toolset VerCors could be extended to formally verify a subset of programs written in SYCL. This subset consists of programs that can contain two kinds of kernel definitions, data sharing between devices and the host, and declarations of data in various address spaces. For each feature in this subset, this thesis shows how its semantics are encoded into VerCors, and what considerations had to be made to facilitate the construction and soundness of these encodings. Finally, the efforts taken to ensure the soundness of the encoding and the usefulness of the supported SYCL subset are discussed. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/97976 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page