BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Chicago
X-LIC-LOCATION:America/Chicago
BEGIN:DAYLIGHT
TZOFFSETFROM:-0600
TZOFFSETTO:-0500
TZNAME:CDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0500
TZOFFSETTO:-0600
TZNAME:CST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260522T150119Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T113000
DTEND;TZID=America/Chicago:20181112T115000
UID:submissions.supercomputing.org_SC18_sess150_ws_corr106@linklings.com
SUMMARY:Verifying Qthreads: Is Model Checking Viable for User Level Taskin
 g Runtimes?
DESCRIPTION:Noah Evans (Sandia National Laboratories)\n\nThis paper descri
 bes 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 do
 ing a function to function translation of Qthreads’ C implementation to Pr
 omela code. This translation works around the differences in modeling and 
 implementation languages by translating C’s rich pointer semantics, functi
 ons and non-local gotos to Promela’s comparatively simple semantics. We th
 en evaluate our implementation to show that it is both tractable and usefu
 l, exhaustively searching the state-space for counterexamples in reasonabl
 e time on modern architectures and use it to a lingering concurrency error
  in the Qthreads runtime.\n\nTag: Applications, Correctness, Debugging, Fl
 oating Point, MPI, OpenMP, Runtime Systems, Tools, Verification\n\nRegistr
 ation Category: Workshop Reg Pass\n\nSession Chairs: Ignacio Laguna (Lawre
 nce Livermore National Laboratory (LLNL)) and Cindy Rubio-González (Univer
 sity of California, Davis)\n\n
END:VEVENT
END:VCALENDAR