CAREER CPA-CSA: Correctness-Constrained Execution for Processor Designs

CAREER CPA-CSA：处理器设计的正确性约束执行

• 批准号: 0746425
• 负责人: Valeria Bertacco
• 金额: $ 40万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-02-01 至 2015-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0746425&HistoricalAwards=false
• 关键词: CAREER; CPA; CSA; Correctness; Constrained

The design complexity of current microprocessor systems is such that practically every system released to the market incorporates latent bugs. Manufacturers and design houses alike strive to validate and verify their designs as much as possible during system development, and then attempt to contain the impact of escaped bugs through publicly available errata reports. Some escaped bugs are innocuous, and can be easily overcome through a BIOS or OS update, but still others are potentially dangerous to the users of the system, or they might compromise its security and adversely affect its performance.This project focuses on developing integrated hardware and software solutions to guarantee that a processor chip operates correctly, even if its design is flawed. The key idea driving this research is to create two modes of operation for the processor: a complex high-performance mode to be used when executing within the portion of the system that has been verified at design time, and a simple low-performance mode guaranteed to be correct under all execution scenarios. By carefully selecting the appropriate mode of operation at runtime, it is possible to always execute correctly: in high-performance when the operation is one that has been verified at design-time or in low performance otherwise. In addition, because of the extreme simplicity of the low-performance mode, it is possible to guarantee that this mode of operation always provides correct results but at a performance price. Related research has shown that, in practice, the low-performance mode intervenes only in very rare occasions, making its performance impact negligible overall. The research challenges to be undertaken in this project include devising low-cost mechanisms to select execution between fast and correct mode, developing the simple mode of operation in such a way that can be fully verified, and developing techniques to efficiently encode the correct states of operation.

当前微处理器系统的设计复杂性是如此之高，以至于几乎每个发布到市场上的系统都包含潜在的缺陷。制造商和设计公司都努力在系统开发过程中尽可能多地验证和验证他们的设计，然后试图通过公开的勘误表报告来控制逃过的错误的影响。有些逃过的错误是无害的，可以通过BIOS或OS更新轻松克服，但仍有一些错误对系统用户具有潜在危险，或者它们可能损害其安全性并对其性能产生不利影响。这个项目的重点是开发集成的硬件和软件解决方案，以保证处理器芯片正确运行，即使它的设计是有缺陷的。推动这项研究的关键思想是为处理器创建两种操作模式：一种复杂的高性能模式，用于在设计时已经过验证的系统部分内执行，另一种简单的低性能模式保证在所有执行场景下都是正确的。通过在运行时仔细选择适当的操作模式，可以始终正确地执行：当操作是在设计时验证过的操作时，在高性能中执行，否则在低性能中执行。此外，由于低性能模式的极端简单性，可以保证这种操作模式总是提供正确的结果，但以性能为代价。相关研究表明，在实践中，低绩效模式只在非常罕见的情况下进行干预，其对整体性能的影响可以忽略不计。本项目面临的研究挑战包括：设计低成本的机制，在快速和正确模式之间选择执行；开发可完全验证的简单运行模式；开发有效编码正确运行状态的技术。