Artifact for paper (Deductive verification of SYCL in VerCors) submitted to SEFM '24 conference. For a full description on how to use the artifact, please see the README.md file. The artifact contains a docker image of the VerCors tool (with SYCL support) and documentation.
Abstract of Paper
SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.
In this paper, SYCL support is added to VerCors, a formal verification tool for concurrent software, by encoding SYCL constructs into VerCors’ internal language COL. To the extend of our knowledge, this is the first deductive verification tool for SYCL. We show how SYCL’s basic- and ND-range kernels are encoded, along with the encoding and challenges related to scheduling kernels and the execution order of those kernels. In addition, we discuss how SYCL’s buffers and data accessors are encoded, focusing on the challenges related to it, in particular enabling memory transfer between host and device. The usability of the added SYCL support and how it was evaluated are discussed as well.
%I 4TU.ResearchData