HPC Software Verification in Action: A Case Study with Tensor Transposition
Authors: Erdal Mutlu (Pacific Northwest National Laboratory)
Abstract: As HPC platforms get increasingly complex, the complexity of software optimized for these platforms has also increased. There is a pressing need to ensure correctness of scientific applications to enhance our confidence in the results they produce. In this paper, we focus on checking the correctness of libraries providing a small but important functionality---tensor transposition---used in computational chemistry applications. While several correctness tools have been developed and deployed, there are several practical challenges in using them to verify production HPC software. We present our experiences using two tools---CIVL and CodeThorn---in checking the correctness of two index permutation libraries. We observe that, with some effort, the tools we evaluated can handle kernels from production codes. We present observations that will aid library writers to write code that can be checked with these tools.
Archive Materials
Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing
Back to Full Workshop Archive Listing