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

除了在我们日常生活中扮演的角色之外，计算机还扮演着无形的安全关键角色。它们能防止汽车刹车锁死，让我们的飞机在密集的空中交通和大风暴中飞行，管理我们的电力和水系统，甚至控制病人的心脏跳动。不幸的是，我们仍然很难制造出能够对这种操作的可靠性做出任何明确评价的计算机系统。这个项目试图改变关键计算机系统的设计和分析方式。所创造的技术将通过开放的存储库提供和访问，这些技术的发展将为本科生和研究生提供大量的培训机会，最令人兴奋的想法将被用于扩展工作，以帮助培养新一代的工程师，最终将有助于发展一个具有实现安全可靠系统所需的技能和工具的嵌入式系统工程师的国家社区。为了实现更强大的计算机控制系统的愿景，我们需要新的方法来创建它们，包括硬件和软件在一起。传统的计算机硬件是为了速度和效率而不惜一切代价，但我们通常有足够的速度和效率来完成一项工作。相反，我们需要的系统，在保持相当高效的同时，也更容易理解和推理。建立在强大的计算理论（如λ -calculus）之上，一个新的计算机系统可以被创造出来，在这个系统中，它所采取的每一个行动都直接对应于一组易于处理的方程。这个项目并没有尝试手工解出结果方程，而是从头开始重新考虑计算机处理器的设计方式，以便它们与最先进的计算机自动定理证明器完美协调地工作。为了证明这种方法在现实世界的问题上确实有用，研究人员正在围绕这种方法构建一个全新的计算机系统，包括所需的所有硬件设计、计算机语言和类似操作系统的软件。

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.