<span class="var-sub_title">Verifying Qthreads: Is Model Checking Viable for User Level Tasking Runtimes?</span> SC18 Proceedings

The International Conference for High Performance Computing, Networking, Storage, and Analysis

2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018)


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