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

这个项目正在为计算机处理器的实验评估开发一个严格的统计框架。一种新的处理器设计的评估涉及到许多实验，在这些实验中，处理器被模拟在不同的硬件配置和不同的软件上运行。目前的技术水平是进行一些这样的实验并给出结果，但这种方法不能提供统计保证；以后的实验显示出截然不同的结果的可能性是没有界限的。该项目正在调整和加强一种称为统计模型检查（SMC）的严格统计技术，该技术已用于需要更强有力保障的其他领域，如网络物理系统（例如植入医疗设备）。有了这个项目正在开发的新增强的SMC，不仅可以提供统计保证，而且还可以评估当前方法无法分析的系统属性（例如，依赖于多个实验之间差异的安全超属性）。SMC的增强是必要的，以适应计算机体系结构的研究，并首次实现对重要问题的严格分析，如非常罕见事件的影响和处理器在最坏情况下的行为。该项目的基础设施将向公众开放，因此学术界和工业界的计算机架构师可以从中受益，最终的结果是更好的处理器设计，架构师和社会可以更有信心。该项目涉及杜克大学Data+和Code+项目的本科生研究助理，这两个项目在大学范围内建立了良好的暑期推广项目，具有卓越的多样性。该项目的研究也被纳入计算机系统实验评估的新交叉列表（ECE和CompSci）课程。PI和co-PI将在一个主要的计算机体系结构会议上为计算机架构师开发并发布SMC教程。该项目的成果和框架将通过PI和联合PI的广泛行业联系转移到工业界。该项目率先在计算机体系结构中使用统计模型检查（SMC），从而使架构师能够用统计严谨性来推断他们的实验结果。该项目为架构师提供了一个进行实验评估的新框架。该框架的部分开发涉及到表达属性和超属性的开发，这些属性允许建筑师评估他们目前没有考虑的条件和情况。该项目通过一种新的事件注入方法，使用SMC来缓解如何评估罕见事件影响的长期问题。该项目还使用SMC和机器学习来提供第一个统计上严格的方案，用于在使用机制（例如，电源管理，计算冲刺）时识别最坏情况。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.