Skip navigation
Please use this identifier to cite or link to this item:
Title: Instruction-Level Abstraction for Program Compilation and Verification in Accelerator-rich Platforms
Authors: Huang, Bo-Yuan
Advisors: Malik, Sharad
Contributors: Electrical Engineering Department
Keywords: abstraction
Subjects: Electrical engineering
Computer engineering
Issue Date: 2022
Publisher: Princeton, NJ : Princeton University
Abstract: Modern computing platforms are becoming increasingly accelerator-rich to meet the demanding power-performance requirements for various emerging applications. Application-specific accelerators provide efficiency in computation; however, the heterogeneity of hardware components and the complexity of software/hardware interaction bring new challenges in developing and deploying such accelerator-rich platforms. In the days of microprocessors, the instruction-set architecture (ISA) provided a natural specification/abstraction of the hardware. Top-down, it provided a specification for functional verification of microprocessor implementation. Bottom-up, it provided an abstraction of the microprocessor that defined the operational semantics of the instructions. Hence, the ISA successfully served as the software/hardware interface and enabled a clean separation between software and hardware development tasks. However, such a uniform and meaningful interface between the software program and hardware accelerators is lacking. Specifically, for program developers, the lack of abstraction of hardware accelerators limits the development of accelerator-interacting software programs. Such a limitation is felt in both the compilation and correctness verification of the programs. This limits system integration verification at an early stage (before the hardware is taped out). This thesis addresses the development challenges in modern accelerator-rich computing platforms, focusing on correct program development, based on the recently proposed Instruction-Level Abstraction (ILA) model. It first introduces the ILA formal model as a uniform software/hardware interface for accelerators and processors and describes the ILAng platform for modeling and verification using ILAs. This thesis then demonstrates how the ILA provides for correct software development in accelerator-rich platforms from two perspectives. First, it shows the use of ILAs for correct program compilation through an end-to-end compilation flow that effectively and correctly maps applications operations to accelerator operations. Second, it presents an ILA-based software/hardware co-verification methodology for checking system-level properties, with a deep dive into security verification of modern System-on-Chip (SoC) designs. In summary, this thesis presents the ILA formal model as a uniform interface between software programs and hardware accelerators. With the instruction-level interface, the ILA allows the specification of mappings between compiler intrinsics and accelerator operations. This enables utilizing standard compilation flows for programs that interact with accelerators and provides formally verifiable compilation. The verification of accelerator code, thus far, is typically done through manual ad hoc testing. Furthermore, as a verified abstraction of accelerators, the ILA captures the operational semantics of hardware at the architecture level. This enables utilizing existing software verification techniques for scalable software/hardware co-verification and the correctness validation of system-level properties. Overall, this thesis demonstrates using ILAs for addressing the challenges of correct software development in modern accelerator-rich platforms.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Electrical Engineering

Files in This Item:
File Description SizeFormat 
Huang_princeton_0181D_13965.pdf954.9 kBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.