Northeastern University
Sign Up
Free Event

Title: Stabilizing Numeric Programs Against Platform Uncertainties

Speaker: Yijia Gu, PhD Candidate, College of Computer and Information Science at Northeastern University

Location: Northeastern University, 440 Huntington Avenue, West Village H, 3rd Floor, Room #366, Boston, Massachusetts 02115

Abstract

Floating-Point Arithmetic (FPA) is a loosely standardized approximation of real arithmetic available on many computers today.  The use of approximation incurs commonly underestimated risks for the reliability of numerical software.  These risks include not only inaccurate computations due to rounding errors, but also reproducibility issues caused by the relatively large degree of freedom for FPA implementers offered by the IEEE 754 standard.  The lack of result reproducibility has become more critical with the emergence of heterogeneous computing, e.g. using OpenCL.  If left untreated, it can seriously interfere with program portability.

In this thesis, we investigate reproducibility problems due to platform uncertainties, including non-reproducible control flow and invariants that hold on some platforms but not others.  We also provide locally fine-grained provenance information to help users repair reproducibility issues.

Specifically, we propose a framework that, for a given numerical program and user-input constraints, will first attempt to prove that the program meets user-defined reproducible specifications.  If the prove attempt fails, our framework will generate counterexample inputs that witness the violation of these specifications.  For these counterexamples, users can utilize our provenance analysis module to trace the violation back to prior statements in the source code that are ultimately responsible for the lack of reproducibility.  These statements are candidates for stabilization, which happens by disambiguating the arithmetic using expression rewriting and statement level control pragmas.

The above framework will be applied to solve reproducibility issues among CPU and GPU versions of kernel support vector machines (SVMs).

About the Speaker

Yijia Gu is a PhD student in the Formal Methods program at Northeastern University’s College of Computer and Information Science, advised by Professor Thomas Wahl. Yijia’s research focuses on verifying numerical programs to ensure that devices and programs are performing properly and effectively, and aims to form his own verification and development techniques to help future developers.  Before joining the PhD program at Northeastern, Yijia earned a bachelor’s degree from Zhejiang University in China.

Committee 

Professor Thomas Wahl, Assistant Professor, College of Computer and Information Science at Northeastern University (Advisor)
Professor Jan-Willem van de Meent, Assistant Professor, College of Computer and Information Science at Northeastern University
Professor Miriam Leeser, Interim Chair and Professor, Affiliated Faculty, College of Engineering at Northeastern University
Professor Xiangyu Zhang, University Scholar, Professor, Department of Computer Science at Purdue University

Event Details

0 people are interested in this event

User Activity

No recent activity