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:20181112T090500
DTEND;TZID=America/Chicago:20181112T100000
UID:submissions.supercomputing.org_SC18_sess150_pec338@linklings.com
SUMMARY:Making Formal Methods for HPC Disappear
DESCRIPTION:Workshop\nCorrectness, Debugging, Verification, Workshop Reg P
 ass\n\nMaking Formal Methods for HPC Disappear\n\nGopalakrishnan\n\nFormal
  methods include rigorous specification methods that can render language s
 tandards reliable and unambiguous. They also include rigorous testing meth
 ods that target well-specified coverage criteria, and formal concepts that
  help guide debugging tool implementations. Those who say formal methods d
 on’t apply to HPC probably misunderstand formal methods to be some esoteri
 c diversion, and not as a software productivity booster in the sense we de
 scribe.\n\nUndoubtedly, HPC correctness is far too complex: there are the 
 accidentally flipping bits, unpredictable floating point rounding, threads
  that incur a data race, and capricious compilers whose optimizations chan
 ge results. All these can severely impact overall productivity. Formal app
 roaches are possible for many of these pursuits, while for others they may
  emerge if one persists, and if there is a community invested in developin
 g them in the long run. A worthwhile direction is to invest in formal meth
 ods based pedagogy: not only does this help buy us some time to develop us
 eful formal methods for HPC, but it also gives some hope to save future ge
 nerations from today’s debugging drudgery. Today’s parallel computing educ
 ation still only gives lip service to correctness - let alone formal.\n\nM
 y talk will try and present examples of all of this. We will present examp
 les where formal ideas did transition to production-level data race checki
 ng tools. I will also present examples where we finished production-level 
 tools for floating-point non-reproducibility in the field, and hope to bac
 kfill the formalism eventually.\n\nEventually, as Rushby says, Formal Meth
 ods must “disappear” - be incorporated into standard practice and we don’t
  see them.
URL:https://sc18.supercomputing.org/presentation/?id=pec338&sess=sess150
END:VEVENT
END:VCALENDAR