SHF: Small: Transforming Computer Architecture Evaluation with Statistical Model Checking

Duke University, Durham NC

Investigators

Abstract

This project is developing a statistically rigorous framework for the experimental evaluation of computer processors. The evaluation of a new processor design involves many experiments, in which the processor is simulated in different hardware configurations and with different software running on it. The current state of the art is to perform some number of these experiments and present the results, but this methodology provides no statistical guarantees; there is no bound on the probability that subsequent experiments would show very different results. This project is adapting and enhancing a rigorous statistical technique, called statistical model checking (SMC), that is used in other fields that have required stronger guarantees, like cyber-physical systems (e.g., implanted medical devices). With the newly enhanced SMC that this project is developing, it is possible to not only provide statistical guarantees, but it is also possible to evaluate system properties that are not analyzable with current methodologies (e.g., security hyper-properties that depend on the differences between multiple experiments). Enhancements to SMC are necessary to accommodate computer architecture research and to enable, for the first time, rigorous analysis of important issues, like the impact of very rare events and the processor’s behavior in worst-case scenarios. The project’s infrastructure will be made publicly available, so computer architects in academia and industry can benefit from it, with the ultimate result being better processor designs in which architects and society can be more confident. This project involves undergraduate research assistants through Duke’s Data+ and Code+ programs, two well-established university-wide summer outreach programs with exceptional diversity. The project’s research is also incorporated into a new cross-listed (ECE and CompSci) class in Experimental Evaluation of Computer Systems. The PI and co-PI will develop and present a tutorial on SMC for computer architects at a major computer architecture conference. The project’s results and framework will be transferred to industry via the extensive industry contacts of the PI and co-PI. This project pioneers the use of statistical model checking (SMC) in computer architecture, thus enabling architects to reason about their experimental results with statistical rigor. This project provides architects with a novel framework for performing experimental evaluations. Part of the development of the framework involves the development of expressive properties and hyper-properties that allow architects to evaluate conditions and situations they do not currently consider. This project uses SMC to mitigate the longstanding problem of how to evaluate the impact of rare events, through a new event injection methodology. This project also uses SMC and machine learning to provide the first statistically rigorous scheme for identifying the worst-case situation when using a mechanism (e.g., power management, computational sprinting). 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.