SHF: Medium: Provably Correct, Energy-Efficient Edge Computing

今天的通用处理器遵循冯·诺伊曼模型，即程序以指令序列的形式执行。然而，事实证明，这种串行执行太慢了。因此，处理器寻求能够安全地并行执行的指令，以提高性能。然而，在硬件上实现并行性是极其复杂的。这种复杂性导致处理器效率低下且不安全，导致行业转向专门为运行特定程序量身定做的硬件加速器。不幸的是，这些加速器既昂贵又受限。为了解决这些问题，该项目提出了后冯·诺伊曼数据流处理器，它显式地暴露了程序并行性，以显著简化硬件。通过新的编译软件和简化的并行硬件，该项目旨在显著提高能效和系统正确性。这些改进将超越冯·诺伊曼模型的限制，在提高性能、效率和安全性的同时促进创新。这项研究将由一个不同的团队进行，包括通过NSF本科生研究体验计划的本科生。此外，研究人员将开发一个推广计划，教育K-12教师和公众各种计算模型。该奖项的关键技术创新是程序的固有并行数据流表示和简单的数据流处理器的空间实现。此外，空间架构采用分层、模块化的方法，支持多维可伸缩性。简单性和模块化允许编译器、体系结构和硬件实现的易于处理的形式模型，使调查人员能够证明正确性和安全性。拟议的架构从一开始就构建了安全性，而不是像研究人员目前难以为冯·诺伊曼架构所做的那样，试图在事后证明安全性。模块化通过将程序分解成具有良好定义的接口的较小的、独立的单元来进一步实现可伸缩编译，每个单元都可以有效地编译到所提议的体系结构上，并且还通过将数据与其相应的计算放在一起来实现近数据计算，以克服不断上升的数据移动成本。由此产生的处理器设计有望成为第一个具有可证明的正确性和安全性的可扩展的通用架构。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Today’s general-purpose processors follow the von Neumann model, where programs execute as a sequence of instructions. However, this serial execution proves to be too slow. Processors thus seek instructions that can safely execute in parallel to enhance performance. Yet, implementing parallelism in hardware is extremely complicated. The complexity renders processors inefficient and insecure, leading the industry's shift toward specialized hardware accelerators tailored to run specific programs exceptionally well. Unfortunately, these accelerators are costly and restrictive. To address these issues, this project proposes post-von Neumann, dataflow processors, that explicitly expose program parallelism to dramatically simplify hardware. Through new compilation software and simplified parallel hardware, the project aims to significantly improve energy efficiency and system correctness. These advancements will transcend von Neumann model limitations, fostering innovation while enhancing performance, efficiency, and security. The research will be conducted by a diverse team, including undergraduates through the NSF Research Experiences for Undergraduates program. Moreover, the investigators will develop an outreach program to educate K-12 teachers and the public on various computing models.The key technical innovation of this award is the innately parallel dataflow representation of programs and a simple, spatial implementation of a dataflow processor. Moreover, the spatial architecture adopts a hierarchical, modular approach that enables scalability in multiple dimensions. Simplicity and modularity admit tractable formal models of the compiler, architecture, and hardware implementation, allowing investigators to prove correctness and security. The proposed architecture builds in security from the beginning, rather than trying to prove security after the fact, as researchers currently struggle to do for von Neumann architectures. Modularity further enables scalable compilation by breaking programs into smaller, independent units with a well-defined interface, each of which can be efficiently compiled onto the proposed architecture, and also enables near-data computation by co-locating data with its corresponding computation to overcome the rising cost of data movement. The resulting processor design promises to be the first a scalable, general-purpose architecture with provable correctness and security.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.