Artifact for Article: Extending Deductive Verification of SYCL in VerCors with Sub-groups

Artifact for article "Extending Deductive Verification of SYCL in VerCors with Sub-groups" submitted to the STTT journal. 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 the described SYCL support) and documentation.

Abstract of Article: 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.

In this article, SYCL support is added to VerCors, a formal verification tool for concurrent software, by encoding SYCL constructs into VerCors' internal language COL. To the extent 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. Next, 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. Finally, we dicuss the encoding for sub-groups and sub-group-intrinsic functions. The usability of the added SYCL support and how it was evaluated are discussed as well.