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

计算机除了在我们的日常生活中扮演着通常的角色外，还扮演着隐形的安全关键角色。它们可以防止汽车的刹车卡住，让我们的飞机在密集的空中交通和大风暴中飞行，管理我们的电力和供水系统，甚至控制患者的心跳。不幸的是，仍然很难建立计算机系统，对于计算机系统，人们可以肯定地说这种操作的可靠性。该项目试图改变设计和分析关键计算机系统的方式。创建的技术将通过开放资源库提供和访问，这些技术的开发将为本科生和研究生提供大量培训机会，最令人兴奋的想法将被用于帮助接触到新一代工程师，最终将有助于发展一个拥有实施安全可靠系统所需技能和工具的全国嵌入式系统工程师社区。为了实现更强大的计算机控制系统的愿景，我们需要新的方法来创建它们，包括硬件和软件。传统的计算机硬件是不惜一切代价追求速度和效率的，但我们通常有足够的速度和效率来完成一项工作。相反，我们需要的是在保持相当高效的同时，也更容易理解和推理的系统。在强大的计算理论(如波长演算)的基础上，可以创建一种新的计算机系统，其中它所采取的每个动作都直接对应于一组易于处理的方程。这个项目没有尝试手工求解得到的方程式，而是重新考虑了计算机处理器的设计方式，以便它们与最先进的计算机自动化定理证明器完美协调地工作。为了证明这种方法对现实世界的问题实际上是有用的，研究人员正在围绕这种方法构建一个全新的计算机系统，其中包含所需的所有硬件设计、计算机语言和类似操作系统的软件。

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.