Collaborative Research: FMitF : Track I: Specifying, Synthesizing, and Verifying Heterogeneous Coherence Protocols

About This Grant

Computers, be it those in mobile phones or servers, are increasingly being designed with heterogeneous processors and memory that is shared across all of these processors. The heterogeneity enables greater performance, with different processors tailored for specific purposes (e.g., graphics), and the shared memory facilitates easier programming. These processors are already being used to support critical computational tasks, including artificial intelligence (AI), robotics, and medical research. While these processors offer great potential, they pose two problems. First, it is difficult to understand how to compose them. Specifically, different types of processors use different communication protocols, and composing these protocols is complicated. Second, it is also challenging to verify that the processors will behave correctly in all situations. The composed protocols have a vast number of possible interactions, and verification techniques do not scale up to meet this challenge. This project addresses both challenges by developing a systematic way to compose processor protocols and a new, scalable technique for verification of these processors. These contributions can offer many benefits, including shorter time to market, confidence that processors will behave as expected, and a lower barrier to entry for startups and researchers seeking to create new processors. By providing a foundation for the correct design of heterogeneous shared memory processors, the project will help to enable the coming generation of high-performance computing systems. These systems will sustain American economic competitiveness, supporting breakthroughs in AI, medicine, science, defense, and many other fields that will enhance the lives of all Americans. This project will make three important contributions to the theory and practice of processor design and verification. First, it will provide, for the first time, a mathematical foundation for defining and reasoning about the interaction of programs sharing memory in a heterogeneous system. This understanding will be crucial for designing the coming wave of heterogeneous systems-on-chip that will drive system performance for consumers and industry in the era of AI. Second, the work will provide an understanding of the large design space of heterogeneous coherence protocols and the first automated tools for correctly synthesizing the protocol converters needed to connect diverse local and global protocols. Third, the project will develop the first compositional approach for verifying heterogeneous coherence protocols and the first application of translation validation to cache coherence protocols. It will integrate verification as part of the protocol design flow, enabling designers to realize cost-effective proofs, and provide an exemplar for making formal methods practical in systems design. 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.