The International Conference for High Performance Computing, Networking, Storage, and Analysis
The International Conference for High Performance Computing, Networking, Storage, and Analysis
Verifying Qthreads: Is Model Checking Viable for User Level Tasking Runtimes?
Authors: Noah Evans (Sandia National Laboratories)
Abstract: This paper describes a formal specification and verification of an HPC runtime through the design, implemen- tation and evaluation of a model checked implementation of the Qthreads many task runtime. We implement our model in Promela by doing a function to function translation of Qthreads’ C implementation to Promela code. This translation works around the differences in modeling and implementation languages by translating C’s rich pointer semantics, functions and non-local gotos to Promela’s comparatively simple semantics. We then evaluate our implementation to show that it is both tractable and useful, exhaustively searching the state-space for counterexamples in reasonable time on modern architectures and use it to a lingering concurrency error in the Qthreads runtime.
Archive Materials
Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing
Back to Full Workshop Archive Listing