When Does a Bit Matter? Techniques for Verifying the Correctness of Assembly Languages and Floating-Point Programs
| dc.contributor.advisor | Norris, Boyana | |
| dc.contributor.author | Pollard, Samuel | |
| dc.date.accessioned | 2021-09-13T18:39:35Z | |
| dc.date.available | 2021-09-13T18:39:35Z | |
| dc.date.issued | 2021-09-13 | |
| dc.description.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. | en_US |
| dc.identifier.uri | https://hdl.handle.net/1794/26652 | |
| dc.language.iso | en_US | |
| dc.publisher | University of Oregon | |
| dc.rights | All Rights Reserved. | |
| dc.subject | binary analysis | en_US |
| dc.subject | floating-point arithmetic | en_US |
| dc.subject | formal methods | en_US |
| dc.subject | high-performance computing | en_US |
| dc.subject | parallel programming | en_US |
| dc.subject | static analysis | en_US |
| dc.title | When Does a Bit Matter? Techniques for Verifying the Correctness of Assembly Languages and Floating-Point Programs | |
| dc.type | Electronic Thesis or Dissertation | |
| thesis.degree.discipline | Department of Computer and Information Science | |
| thesis.degree.grantor | University of Oregon | |
| thesis.degree.level | doctoral | |
| thesis.degree.name | Ph.D. |
Files
Original bundle
1 - 1 of 1
Loading...
- Name:
- Pollard_oregon_0171A_13012.pdf
- Size:
- 1.8 MB
- Format:
- Adobe Portable Document Format