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

该项目正在开发一个严格的统计框架，用于计算机处理器的实验评估。 一个新的处理器设计的评估涉及到许多实验，在这些实验中，处理器在不同的硬件配置和不同的软件上运行。目前的技术水平是执行一些这样的实验，并提出结果，但这种方法不提供统计保证;没有约束的概率，随后的实验将显示非常不同的结果。 该项目正在调整和加强一种称为统计模型检查（SMC）的严格统计技术，该技术用于需要更强保证的其他领域，如网络物理系统（例如，植入式医疗器械）。 利用本项目正在开发的新增强的SMC，不仅可以提供统计保证，而且还可以评估当前方法无法分析的系统属性（例如，取决于多个实验之间的差异的安全超属性）。 对SMC的增强是必要的，以适应计算机体系结构研究，并首次实现对重要问题的严格分析，如非常罕见的事件的影响和处理器在最坏情况下的行为。 该项目的基础设施将公开提供，因此学术界和工业界的计算机架构师可以从中受益，最终结果是更好的处理器设计，架构师和社会可以更有信心。该项目涉及本科研究助理通过杜克的数据+和代码+程序，两个完善的大学范围内的夏季推广计划具有特殊的多样性。 该项目的研究也被纳入一个新的交叉上市（ECE和CompSci）类计算机系统的实验评估。 PI和co-PI将在一个主要的计算机架构会议上为计算机架构师开发并展示SMC教程。 该项目的结果和框架将通过PI和co-PI的广泛行业联系转移到industrial.This项目开创了在计算机架构中使用统计模型检查（SMC），从而使建筑师能够对他们的实验结果与统计严谨性的原因。 该项目为建筑师提供了一个新的框架进行实验评估。 框架开发的一部分涉及表达属性和超属性的开发，这些属性允许架构师评估他们目前没有考虑的条件和情况。 该项目使用SMC通过一种新的事件注入方法来缓解如何评估罕见事件影响的长期问题。该项目还使用SMC和机器学习来提供第一个统计上严格的方案，用于识别使用机制时的最坏情况（例如，该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.