|
|
|---|
|
|
|
|---|
W.R. Bevier, W.A. Hunt, Jr., J S. Moore, and W.D. Young, Special
Issue on System Verification, Journal of Automated Reasoning,
5(4), pp. 409-530, 1989.
Relevance: Computational Logic Inc. (CLI) Verified
Stack — a seminal achievement in formal methods and operational
semantics
The Computational Logic, Inc (CLI) Verified Stack was reported in this Special Issue of the JAR.
The CLI stack was composed of four verified components: a gate-level design for a microprocessor (by Warren Hunt), an assembler/linker/loader that provided an execute-only, stack-based instruction set with subroutine call and return (Moore), a compiler for a small subset of a programming language related to Pascal (Bill Young, see bib::young88), and a simple operating system kernel (Bill Bevier; see bib::bevier87). All components were verified with Nqthm, so that a high-level program could be compiled, assembled, linked, loaded, and run on the gate-level machine with mathematical certainty that it behaved as specified by the semantics of the high-level programming language. All the models just mentioned involved operational-semantics and proofs in the style described in here. Indeed, this project basically convinced the community that this style of semantics was practical for both execution and verification of models.
The verification of the relations between each component — gates to machine code, machine code to assembly language, assembly language to high level language, operating system to assembly language — must be considered a “first” for relating practical machines of each kind. To the best of our knowledge, no one had ever verified a gate-level implementation of an ISA for a practical microprocessor before Hunt's 1985 work bib::hunt85. With the same caveat, no one had ever verified an assembler/linker/loader before Moore's 1988 Piton work (see bib::moore96 for a history) or verified an operating system kernel for a practical machine before Bevier's 1987 work. And while McCarthy and Painter verified (by a traditional “hand proof”) an expression compiler, which various formal methods researchers tackled in the 1970s (including Boyer and Moore in 1979 bib::bm79, where a history of the challenge is sketched), both the high- and low- level machines involved in that earlier “compiler” work were trivial compared to what Young dealt with in 1988. The messy reality of each component was fundamentally due to the requirement that each layer, starting at the gates, provide sufficient functionality to implement the higher layers.
In 1989, the “hardware” at the bottom of the CLI stack was a gate-level description of a machine called FM8502. The FM8502 was a 32-bit version of Hunt's earlier 16-bit FM8501; see bib::hunt85. Hunt designed and verified FM8502 to make Moore's job of writing an assembler a little easier. Moore, with Matt Kaufmann's help with some proofs, verified that the FM8502 code produced by the assembler/linker/loader implemented the semantics of the Piton assembly language. But the FM8502 could not be fabricated because its gate-level description was not compatible with commercial fabrication tools, e.g., there was unrealistic fan-out. But the 1989 CLI Verified Stack demonstrated that it was practical to prove that a gate-level design implemented a given instruction set architecture (ISA) and that the operational semantic approach allowed the mechanized proofs of formal relations between different abstraction hierarchies.
In 1991, Hunt and Bishop Brock designed a formal hardware description language (HDL) and used it to describe the FM9001 microprocessor which they then verified to implement its ISA; see bib::hb92. The FM9001 was fabricated. In 1991, Moore retargeted the code-generators in the 1989 assembler/linker/loader and re-verified that part of the stack, making it possible to port the rest of the verified stack to a fabricated, running machine; see bib::moore96.
In 1992, two other interesting projects related to Piton and FM9001 were completed. Art Flatau completed the implementation and Nqthm verification of a second compiler, one that compiled a small subset of the Nqthm functional programming language into Piton (see bib::flatau92).
At about the same time, Matt Wilding completed the implementation and verification of several real-time control programs in Piton and verified their functional correctness and resource bounds (instruction counts and stack sizes). See bib::wilding92 and bib::wilding93. One of the programs carried out a winning strategy for the game of Nim (if one exists from the given Nim starting state).
Wilding wrote (bib::wilding93, page 278) “An FM9001 was fabricated and runs a compiled version of the Nim program. The fabricated FM9001 microprocessor, the Piton compiler, and the Nim program were never tested in a conventional manner during development or after completion. Even so, each worked the first time and we would have been surprised if any had not.”