Presentation
Verifying Qthreads: Is Model Checking Viable for User Level Tasking Runtimes?
Author/Presenter
Event Type
Workshop
W
Correctness
Debugging
Runtime Systems
Verification
TimeMonday, November 12th11:30am - 11:50am
LocationD171
DescriptionThis 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
Author/Presenter