KLOKKOS is a portmanteau of Klee and Kokkos, is a project to develop automated test generation for performance-portable programs - specifically Kokkos parallel programs - using Clang/LLVM and formal methods.
Kokkos is a C++ software library to write portable, high-performance parallel code. However, software developed in Kokkos often has maintainability challenges, since there are subtle differences between architectures that may not appear in traditional testing, or cannot be tested (e.g., predicted behavior on future architectures).
The KLOKKOS project is meant to provide a suite of test generation and validation tools to help increase maintainability and portability of Kokkos programs. This is accomplished via several methods:
Ultimately, this results in tools that can generate test cases for programs (that can indicate, e.g., subtle heterogeneity bugs or potentially data race bugs). Furthermore, these tools can be used to analyze existing Kokkos programs by indicating places where portability is not assured, through command-line based tools. This work can also help with documentation of Kokkos by adding many example programs, as well as specifications to consult to determine the correct behavior of a Kokkos program, even for architectures which have not yet been invented.
This repository contains many different projects. As such there is not yet one unified way to perform test generation or modeling, however during this project we have developed several different approaches, outlined below.
It has been convenient for us to outline useful examples demonstrating the most common classes of mistakes Kokkos developers tend to make in order to test the analysis capabilities of our tools. These consist of a collection of kernels that identify key features of Kokkos. These are common computations in real-world Kokkos applications that are bug-prone.
These consist of a canonical set of examples of typical portability mistakes encountered in a survey of the Kokkos examples above.
Source code snapshot of our modified (forked) KLEE version 2.3.
Because KOKKOS is so complex, we use a "mock" back-end that provides a bare functionality to simplify analysis, while still providing the key API functionality.
This is a very early first draft towards a formal specification in Coq. The main work is continuing elsewhere, in preparation for publication and will likely be pen-and-paper in addition to some Coq formalization. Stay tuned!
The KL part of KLOKKOS, this is a start at developing a KLEE plugin to do symbolic execution of Kokkos programs.
Another approach to analyze Kokkos programs is to translate them into a simpler representation. This is implemented as a Clang tool.
This work is funded by the Department of Energy Advanced Scientific Computing Research (ASCR) X-Stack Programming Environments For Scientific Computing project (DE-FOA-0002460).
Sandia National Laboratories is a multimission laboratory managed and operated by National Technology and Engineering Solutions of Sandia, LLC., a wholly owned subsidiary of Honeywell International, Inc., for the U.S. Department of Energy’s National Nuclear Security Administration under contract DE-NA-0003525.