Mechanized Code Proofs Based on a Formal Microprocessor Specification

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

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.