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:20260522T150125Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T090500
DTEND;TZID=America/Chicago:20181112T100000
UID:submissions.supercomputing.org_SC18_sess150_pec338@linklings.com
SUMMARY:Making Formal Methods for HPC Disappear
DESCRIPTION:Ganesh L. Gopalakrishnan (University of Utah)\n\nFormal method
 s include rigorous specification methods that can render language standard
 s reliable and unambiguous. They also include rigorous testing methods tha
 t target well-specified coverage criteria, and formal concepts that help g
 uide debugging tool implementations. Those who say formal methods don’t ap
 ply to HPC probably misunderstand formal methods to be some esoteric diver
 sion, and not as a software productivity booster in the sense we describe.
 \n\nUndoubtedly, HPC correctness is far too complex: there are the acciden
 tally flipping bits, unpredictable floating point rounding, threads that i
 ncur a data race, and capricious compilers whose optimizations change resu
 lts. All these can severely impact overall productivity. Formal approaches
  are possible for many of these pursuits, while for others they may emerge
  if one persists, and if there is a community invested in developing them 
 in the long run. A worthwhile direction is to invest in formal methods bas
 ed pedagogy: not only does this help buy us some time to develop useful fo
 rmal methods for HPC, but it also gives some hope to save future generatio
 ns from today’s debugging drudgery. Today’s parallel computing education s
 till only gives lip service to correctness - let alone formal.\n\nMy talk 
 will try and present examples of all of this. We will present examples whe
 re formal ideas did transition to production-level data race checking tool
 s. I will also present examples where we finished production-level tools f
 or floating-point non-reproducibility in the field, and hope to backfill t
 he formalism eventually.\n\nEventually, as Rushby says, Formal Methods mus
 t “disappear” - be incorporated into standard practice and we don’t see th
 em.\n\nTag: Applications, Correctness, Debugging, Floating Point, MPI, Ope
 nMP, Runtime Systems, Tools, Verification\n\nRegistration Category: Worksh
 op Reg Pass\n\nSession Chairs: Ignacio Laguna (Lawrence Livermore National
  Laboratory (LLNL)) and Cindy Rubio-González (University of California, Da
 vis)\n\n
END:VEVENT
END:VCALENDAR