SHF: Small: Exploring Architectural Support for Full-Stack Equational Reasoning in Critical Embedded Systems

University Of California-Santa Barbara, Santa Barbara CA

Investigators

Abstract

In addition to their usual roles in our everyday lives computers also play invisible safety-critical roles. They prevent the brakes in cars from locking up, fly our airplanes through dense air traffic and around large storms, manage our electrical and water systems, and even control the beating of patients' hearts. Unfortunately, it still remains difficult to build computer systems for which one can say anything definitive about reliability of such operation. This project attempts to change the way in which critical computer systems are designed and analyzed. The technologies created will be available and accessible through open repositories, the development of those technologies will provide both undergraduate and graduate students numerous training opportunities, the most exciting ideas will be used in outreach efforts to help reach new generations of engineers, and in the end will help to develop a national community of embedded systems engineers with the skills and tools necessary to implement safe and reliable systems. To achieve this vision of more robust computer controlled systems we need new approaches to creating them that includes both the hardware and the software together. Traditional computer hardware is built for speed and efficiency at all costs, but often we have more than enough speed and efficiency to get a job done. Instead, we need systems that, while remaining quite efficient, also are far easier to understand and reason about. Building on top of powerful theories of computation (such as lambda-calculus) a new computer system, where every action it takes corresponds directly to a tractable set of equations, can be created. Rather than try and solve the resulting equations by hand, this project reconsiders the way computer processors are designed from the ground up so that they work in perfect harmony with state-of-the-art computer-automated theorem provers. To demonstrate that this approach is actually useful on real world problems the investigators are building a completely new computer system around this approach with all of the hardware design, computer languages, and operating system-like software needed.