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:20181221T160727Z
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:Workshop\nCorrectness, Debugging, Runtime Systems, Verificatio
 n, Workshop Reg Pass\n\nVerifying Qthreads: Is Model Checking Viable for U
 ser Level Tasking Runtimes?\n\nEvans\n\nThis paper describes a formal spec
 ification and verification of an HPC runtime through the design, implemen-
  tation and evaluation of a model checked implementation of the Qthreads m
 any 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 la
 nguages by translating C’s rich pointer semantics, functions and non-local
  gotos to Promela’s comparatively simple semantics. We then evaluate our i
 mplementation to show that it is both tractable and useful, exhaustively s
 earching the state-space for counterexamples in reasonable time on modern 
 architectures and use it to a lingering concurrency error in the Qthreads 
 runtime.
URL:https://sc18.supercomputing.org/presentation/?id=ws_corr106&sess=sess1
 50
END:VEVENT
END:VCALENDAR