Collaborative Research: FMitF: Track I: Synthetic Compilation for Embedded Systems

嵌入式系统在现代计算应用中发挥着越来越重要的作用。这些系统通过开发具有特定领域加速指令的自定义硬件，将机器学习和密码学等密集型工作负载融入小功率信封中。这种定制的处理器只有在伴随着可以利用其新颖功能的定制编译器时才有用。如今，这些编译器必须为每个定制的嵌入式系统重新开发，但编译器开发是容易出错的，并且存在生成的代码的正确性问题或性能差的风险。这个项目将开发一个新的框架，用于快速开发定制的嵌入式系统编译器，这些编译器被验证是正确的，并生成高性能的代码。该框架将开发和扩展使用程序合成的技术，以促进灵活硬件目标的编译。它将开发新的方法来提高大型编译问题的可伸缩性，并自动化为给定的编译设置推断规则的过程。由此产生的框架将有利于嵌入式系统设计人员加快他们的开发周期，并增加信心的正确性广泛分布的嵌入式应用程序。该项目的成果将通过开放源代码软件和出版物分享，并将用于扩大本科系统课程，以涵盖基于合成的技术。技术方法将涉及开发Ember，这是一个用于快速生成经过验证的高性能编译器的工具包。Ember将解决三个研究挑战：（1）一种新的规范语言，用于定制嵌入式处理器ISA，它捕获足够的细节来指导基于合成的编译器，同时仍然使规范工作易于处理;（2）通过使用输入程序和合成引擎本身的分解来扩展合成辅助编译的范围;以及（3）通过从处理器的伊萨规范自动推断和验证合适的重写系统来推进等式饱和的使用以发现有效的数据移动模式。Ember工具包将使用计算机视觉和增强现实中的应用作为驱动示例，以展示灵活性和端到端效率。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Embedded systems play an increasingly critical role in modern computing applications. These systems fit intensive workloads like machine learning and cryptography into small power envelopes by developing custom hardware with domain-specific accelerated instructions. Such customized processors are only useful when accompanied by custom compilers that can harness their novel functionality. Today, these compilers must be developed anew for each customized embedded system, but compiler development is error-prone and risks correctness issues or poor performance of the generated code. This project will develop a new framework for rapidly developing custom embedded-system compilers that are verified to be correct and generate high-performance code. The framework will develop and extend techniques that use program synthesis to facilitate compilation for flexible hardware targets. It will develop new approaches to improve scalability to large compilation problems and to automate the process of inferring rules for a given compilation setting. The resulting framework will benefit embedded system designers by accelerating their development cycle and increasing confidence in the correctness of widely distributed embedded applications. This project's results will be shared through open-source software and publications and will be used to expand undergraduate systems classes to cover synthesis-based techniques.The technical approach will involve developing Ember, a toolkit for quickly producing verified, high-performance compilers. Ember will address three research challenges: (1) a new specification language for custom embedded processor ISAs that captures enough detail to guide synthesis-based compilers while still making the specification effort tractable; (2) expanding the scope of synthesis-aided compilation by using decomposition both of the input program and of the synthesis engine itself; and (3) advancing the use of equality saturation for discovering efficient data movement patterns by automatically inferring and verifying a suitable rewrite system from a processor's ISA specification. The Ember toolkit will use applications in computer vision and augmented reality as driving examples to demonstrate flexibility and end-to-end efficiency.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.