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.

当今的通用处理器遵循von Neumann模型，该程序作为指令顺序执行。但是，这种连续执行被证明太慢了。因此，处理器寻求可以平行执行以提高性能的说明。但是，在硬件中实现并行性非常复杂。复杂性使处理器效率低下且不安全，导致该行业朝着专门的硬件加速器量身定制的，以非常好的运行特定程序。不幸的是，这些加速器是昂贵且限制性的。为了解决这些问题，该项目提案在Neumann，DataFlow处理器后，明确暴露了程序并行性，以动态简化硬件。通过新的编译软件和简化的并行硬件，该项目旨在显着提高能源效率和系统正确性。这些进步将超越冯·诺伊曼（Von Neumann）模型限制，促进创新，同时提高性能，效率和安全性。这项研究将由一个多元化的团队进行，包括通过NSF研究经验的本科生计划。此外，调查人员将制定一项外展计划，以教育K-12教师和公众各种计算模型。该奖项的关键技术创新是程序的天生数据流表示以及数据流处理器的简单空间实现。此外，空间体系结构适应了层次结构的模块化方法，该方法可以在多个维度上可扩展。简单性和模块化可接受性可接受的编译器，体系结构和硬件实现的正式模型，使研究人员能够证明正确性和安全性。所提出的架构从一开始就建立在安全性的基础上，而不是在事实之后试图证明安全性，因为研究人员目前很难为冯·诺伊曼（Von Neumann）的体系结构做。模块化进一步可以通过将程序分解为具有明确定义的界面的较小的独立单元，可以有效地将程序汇编成较小的独立单元，可以有效地将其编译到所提出的体系结构上，还可以通过与相应的计算共同列入数据来克服数据流动成本上升的数据。由此产生的处理器设计有望成为具有可证明正确性和安全性的可扩展，通用体系结构。该奖项反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响审查标准，通过评估诚实地表示支持。