The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/45d37292-cce5-4fb7-8d4e-a1b32cfa3028

Şakar, Ömer; Wittingen, Ellen; Huisman, Marieke (2024): Artifact for Paper: (Deductive verification of SYCL in VerCors). Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/45d37292-cce5-4fb7-8d4e-a1b32cfa3028.v1

Dataset

• Computer Software
• Information and Computing Sciences

Deductive Verification, heterogeneous computing, SYCL, VerCors

MPL 2.0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Ömer Şakar , Ellen Wittingen , Marieke Huisman

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.

• 2024-07-05 first online, published, posted

4TU.ResearchData

Dockerfile, *.txt, *.sh, *.pdf

• ChEOPS (NWO TTW grant 17249)

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT)