When Does a Bit Matter? Techniques for Verifying the Correctness of Assembly Languages and Floating-Point Programs
Loading...
Date
2021-09-13
Authors
Pollard, Samuel
Journal Title
Journal ISSN
Volume Title
Publisher
University of Oregon
Abstract
This dissertation is about verifying the correctness of low-level computer programs.This is challenging because low-level programs by definition cannot use many
useful abstractions of computer science. Features of high-level languages such
as type systems or abstraction over binary representation of data provide
rich information about the purpose of a computer program, which verification
techniques or programmers can use as evidence of correctness.
Sometimes, however, using these abstractions is impossible. For example,compilers use binary and assembly-level representations and sometimes
performance constraints demand hand-written assembly. With numerical
programs, floating-point arithmetic only approximates real arithmetic.
Floating-point issues are compounded by parallel computing, where a
large space of solutions are acceptable.
To reconcile this lack of abstraction, we apply high-level reasoning techniquesto help verify correctness on three different low-level programming models
computer scientists use. First, we implement a binary analysis tool to
formalize assembly languages and instruction set architectures to facilitate
verification of binaries. We then look at floating-point arithmetic as it applies
to parallel reductions. This expands the notion of reductions to one which
permits the many different solutions allowed by the Message Passing Interface
(MPI) standard. Last, we refine floating-point error analysis of numerical
kernels to quantify the tradeoff between accuracy and performance. These
enhancements beyond traditional definitions of correctness help programmers
understand when, and precisely how, a computer program's behavior is correct.
Description
Keywords
binary analysis, floating-point arithmetic, formal methods, high-performance computing, parallel programming, static analysis