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

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.