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

SHF：中：可证明正确、节能的边缘计算

• 批准号: 2403144
• 负责人: Nathan Beckmann
• 金额: $ 113.9万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-10-01 至 2028-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2403144&HistoricalAwards=false
• 关键词: SHF; Medium; Provably; Correct; Energy

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.

当今的通用处理器遵循冯·诺依曼模型，其中程序作为指令序列执行，但是事实证明，这种串行执行速度太慢，因此处理器寻求可以安全地并行执行的指令以提高性能。硬件极其复杂，导致处理器效率低下且不安全，导致业界转向专门为运行特定程序而设计的加速器，但不幸的是，这些加速器成本高昂且受到限制。该项目提出了后冯诺依曼数据流处理器，通过新的编译软件和简化的并行硬件，显着地公开程序并行性，以显着提高能源效率和系统正确性，这些进步将超越冯诺依曼模型的限制。促进创新，同时提高绩效、效率和安全性。该研究将由一个多元化的团队进行，其中包括通过 NSF 本科生研究经验项目的本科生。此外，研究人员还将制定一项外展计划，以教育 K-12 教师和公众。关于各种该奖项的关键技术创新是程序固有的并行数据流表示和数据流处理器的简单空间实现，此外，空间架构采用分层、模块化方法，可实现多个维度的可扩展性。承认编译器、架构和硬件实现的易于处理的形式模型，使研究人员能够从一开始就证明所提出的架构的正确性和安全性，而不是像研究人员目前为 von 所做的那样试图在事后证明安全性。诺依曼架构通过将程序分解为具有明确定义的接口的更小的独立单元，进一步实现了可扩展编译，每个单元都可以有效地编译到所提出的架构上，并且还通过将数据与其对应的共置来实现近数据计算。由此产生的处理器设计有望成为第一个可扩展的通用架构，具有可证明的正确性和安全性。该奖项反映了 NSF 的法定使命，并通过使用该奖项的评估被认为值得支持。基金会的智力价值和更广泛的影响审查标准。