Drawing

Correctness 2017: First International Workshop on Software Correctness for HPC Applications

November 12, 2017 (9am - 12:30pm)

Colorado Convention Center, Room 501

Denver, Colorado, USA

Held in conjunction with SC17: The International Conference for High Performance Computing, Networking, Storage and Analysis
In cooperation with
SIGHPC

Ensuring correctness in high-performance computing (HPC) applications is one of the fundamental challenges that the HPC community faces today. While significant advances in verification, testing, and debugging have been made to isolate software errors (or defects) in the context of non-HPC software, several factors make achieving correctness in HPC applications and systems much more challenging than in general systems software—growing heterogeneity (architectures with CPUs, GPUs, and special purpose accelerators), massive scale computations (very high degree of concurrency), use of combined parallel programing models (e.g., MPI+X), new scalable numerical algorithms (e.g., to leverage reduced precision in floating-point arithmetic), and aggressive compiler optimizations/transformations are some of the challenges that make correctness harder in HPC. The following report lays out the key challenges and research areas of HPC correctness: DOE Report of the HPC Correctness Summit.

As the complexity of future architectures, algorithms, and applications in HPC increases, the ability to fully exploit exascale systems will be limited without correctness. With the continuous use of HPC software to advance scientific and technological capabilities, novel techniques and practical tools for software correctness in HPC are invaluable.

The goal of the Correctness Workshop is to bring together researchers and developers to present and discuss novel ideas to address the problem of correctness in HPC. The workshop will feature contributed papers and invited talks in this area.

Workshop Topics

Topics of interest include, but are not limited to:

Submissions and Format

Authors are invited to submit manuscripts in English structured as technical or experience papers not exceeding 6 pages of content. The 6-page limit includes figures, tables and appendices, but does not include references, for which there is no page limit. Submissions must use the ACM format (please use the sigconf format with default options).

Submitted papers must represent original unpublished research that is not currently under review for any other venue. Papers not following these guidelines will be rejected without review. Submissions received after the due date, exceeding length limit, or not appropriately structured may also not be considered. At least one author of an accepted paper must register for and attend the workshop. Authors may contact the workshop organizers for more information. Papers should be submitted electronically in EasyChair at: https://easychair.org/conferences/?conf=correctness2017.

Proceedings

The proceedings will be archived in both the ACM Digital Library and IEEE Xplore through SIGHPC.

Important Dates

Organizers

Ignacio Laguna, LLNL
Cindy Rubio-González, UC Davis

Program Committee

David Abramson, The University of Queensland, Australia
Eva Darulova, MPI-SWS, Germany
Alastair Donaldson, Imperial College London, UK
Ganesh Gopalakrishnan, University of Utah, USA
Paul Hovland, ANL, USA
Costin Iancu, LBNL, USA
Sriram Krishnamoorthy, PNNL, USA
David Lecomber, Allinea/ARM, UK
Richard Lethin, Reservoir Labs, Yale University, USA
Matthias Müller, RWTH Aachen University, Germany
Feng Qin, The Ohio State University, USA
Nathalie Revol, INRIA - ENS de Lyon, France
Kento Sato, Lawrence Livermore National Laboratory, USA
Koushik Sen, UC Berkeley, USA
Stephen Siegel, University of Delaware, USA
Armando Solar-Lezama, MIT, USA

Venue

Colorado Convention Center
700 14th St, Denver, CO 80202

Room 501

Program


Keynote Address

Stephen Siegel (University of Delaware)
Stephen-Siegel Stephen Siegel is an Associate Professor in the Department of Computer and Information Sciences and the Department of Mathematical Sciences at the University of Delaware. He received the Ph.D. in mathematics from the University of Chicago in 1993. As a working mathematician, first at Northwestern University and then at the University of Massachusetts Amherst, he worked in the areas of finite group theory, and the representation theory and cohomology of finite groups. Much of his work focused on computational issues in those fields. At UMass, his interests veered towards software engineering, and he worked as a software engineer and then research scientist in the Laboratory for Advanced Software Engineering Research, focusing in particular on formal verification of concurrent systems. He joined the University of Delaware in 2006 and started the Verified Software Laboratory (VSL), which researches new techniques for verifying and debugging parallel programs, especially programs used for computational science. The VSL has produced the symbolic execution and model checking platform CIVL, among other tools.


Schedule

Opening
09:00 - 09:10: Opening remarks
09:10 - 10:00: Keynote Address: A Verification Language for High Performance Computing, Stephen Siegel
Break
10:00 - 10:30: Break (coffee provided by SC17)
Applications & Algorithms Correctness
10:30 - 10:47: "Verifying Concurrency in an Adaptive Ocean Circulation Model", Alper Altuntas and John Baugh (slides)
10:47 - 11:04: "Quality Assurance and Error Identification for the Community Earth System Model", Allison Baker, Daniel Milroy, Dorit Hammerling and Haiying Xu (slides)
11:04 - 11:21: "A Family of Provably Correct Algorithms for Exact Triangle Counting", Matthew Lee and Tze Meng Low (slides)
Runtime Systems Correctness
11:21 - 11:38: "Verifying MPI applications with SimGridMC", The Anh Pham, Thierry Jéron and Martin Quinson (slides)
11:38 - 11:55: "Runtime Correctness Checking for Emerging Programming Paradigms", Joachim Protze, Christian Terboven, Matthias S. Müeller, Serge Petiton, Nahid Emad, Hitoshi Murai and Taisuke Boku (slides)
Code Generation & Code Equivalence Correctness
11:55 - 12:12: "Verifying the Floating-Point Computation Equivalence of Manually and Automatically Differentiated Code", Markus Schordan, Jan Hückelheim, Pei-Hung Lin and Harshitha Gopalakrishnan (slides)
12:12 - 12:29: "Towards Self-Verification in Finite Difference Code Generation", Jan Hückelheim, Ziqing Luo, Fabio Luporini, Navjot Kukreja, Michael Lange, Gerard Gorman, Stephen Siegel, Matthew Dwyer and Paul Hovland (slides)

Contact Information

Please address workshop questions to Ignacio Laguna (ilaguna@llnl.gov) and/or Cindy Rubio-González (crubio@ucdavis.edu).