Mechanized Code Proofs Based on a Formal Microprocessor Specification

基于正式微处理器规范的机械化代码证明

• 批准号: 9017499
• 负责人: Robert Boyer
• 金额: $ 13.98万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-05-15 至 1993-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9017499&HistoricalAwards=false
• 关键词: Mechanized; Code; Proofs; Based; Formal

The propose is to build an experimental software system to test the feasibility of mathematically formalizing physically realizable microprocessor architectures and to test the feasibility of mechanically checking the correctness of system software written in microprocessor machine language for such microprocessors. Although in principle such formalization and checking are possible, they are widely suspected to be practically infeasible. However, a few recent experiments do demonstrate that a new approach of directly formalizing a machine architecture as a mathematical function in a mechanized logic offers promise. A substantial fraction of a commonly used processor has been formalized and several machine code programs have been rigorously checked mechanically. The initial prototype of the system will be used (a) to test the feasibility of proofs of compiler correctness and (b) to explore the development of a formalized programming environment for system software, with focus on such issues as formalizing memory management and rigorously demonstrating performance figures. The experiment will involve formalizing, in a mechanized logic, the user instruction set of several commonly-used microprocessors, and will also involve formalizing the semantics of some system traps. The work will explore new areas in formalization, including cache consistency, memory protection, and interrupts. The machine architecture issues of proving correct high level language compilers. will also be explored.

建议建立一个实验软件系统，以测试数学形式化物理可实现的微处理器体系结构的可行性，并测试机械检查用微处理器机器语言编写的系统软件的正确性的可行性。虽然原则上这种形式化和检查是可能的，但人们普遍怀疑它们实际上是不可行的。然而，最近的一些实验确实表明，将机器架构直接形式化为机械化逻辑中的数学函数的新方法提供了希望。一个常用处理器的很大一部分已经被形式化，一些机器代码程序已经被严格地机械检查过。该系统的初始原型将用于(a)测试编译器正确性证明的可行性，以及(b)探索系统软件的形式化编程环境的开发，重点是形式化内存管理和严格展示性能数据等问题。实验将包括以机械化的逻辑形式化几个常用微处理器的用户指令集，还将包括形式化一些系统陷阱的语义。这项工作将探索形式化的新领域，包括缓存一致性、内存保护和中断。证明正确的高级语言编译器的机器架构问题。也将被探索。