Presentation
Making Formal Methods for HPC Disappear
Presenter
Event Type
Workshop
W
Correctness
Debugging
Verification
TimeMonday, November 12th9:05am - 10am
LocationD171
DescriptionFormal methods include rigorous specification methods that can render language standards reliable and unambiguous. They also include rigorous testing methods that target well-specified coverage criteria, and formal concepts that help guide debugging tool implementations. Those who say formal methods don’t apply to HPC probably misunderstand formal methods to be some esoteric diversion, and not as a software productivity booster in the sense we describe.
Undoubtedly, 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 change results. 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 based pedagogy: not only does this help buy us some time to develop useful formal methods for HPC, but it also gives some hope to save future generations from today’s debugging drudgery. Today’s parallel computing education still only gives lip service to correctness - let alone formal.
My talk will try and present examples of all of this. We will present examples where formal ideas did transition to production-level data race checking tools. I will also present examples where we finished production-level tools for floating-point non-reproducibility in the field, and hope to backfill the formalism eventually.
Eventually, as Rushby says, Formal Methods must “disappear” - be incorporated into standard practice and we don’t see them.
Undoubtedly, 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 change results. 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 based pedagogy: not only does this help buy us some time to develop useful formal methods for HPC, but it also gives some hope to save future generations from today’s debugging drudgery. Today’s parallel computing education still only gives lip service to correctness - let alone formal.
My talk will try and present examples of all of this. We will present examples where formal ideas did transition to production-level data race checking tools. I will also present examples where we finished production-level tools for floating-point non-reproducibility in the field, and hope to backfill the formalism eventually.
Eventually, as Rushby says, Formal Methods must “disappear” - be incorporated into standard practice and we don’t see them.
Archive
