|
|
|---|
|
|
|
|---|
A quick history of our style of modeling state machines
As informally explained in operational-semantics and illustrated in operational-semantics-1__simple-example and operational-semantics-3__annotated-bibliography, the common ACL2 style in which state machines are modeled involves representing the relevant part of the state as an ACL2 object, defining a single-step function for computing state transitions, and then defining a total recursive run function for iterating the step function until it “halts” or some specified number of steps has been taken.
This approach to operational semantics is different from “structural operational semantics” described by Plotkin in his 1981 paper “A Structural Approach to Operational Semantics” (see bib::plotkin04a). Plotkin formalized machines operationally but as inference rules (reminiscent of Hoare logic). See also bib::plotkin04b, where Plotkin elaborates on the origins of that approach. Furthermore, the origins paper appears in a two volume special issue of The Journal of Logic and Algebraic Programming which contains many other papers on structural operational semantics.
To distinguish the approach taken commonly in the ACL2 community from structural operational semantics we might call it “ACL2-style” operational semantics. But its only connection to ACL2 is that ACL2 happens to be the logic in which our models are expressed. Other settings supporting recursion and induction could also be used. Boyer and Moore used this approach in the 1970s, inspired in part by McCarthy's seminal papers (“Recursive Functions of Symbolic Expressions and Their Computation by Machine,” 1960, “A Basis for a Mathematical Theory of Computation,” 1963, and “Correctness of a Compiler for Arithmetic Expressions,” with James Painter, 1967). But we would be hard-pressed to attribute this style of operational semantics even to McCarthy. In the first place, mathematicians have used formal state machines at least since since Goedel's 1931 incompleteness paper: he modeled proofs as objects (specifically, integers) and defined a non-terminating function that stepped through all possible proofs looking for a particular proof. In the second place, machine designers and programmers have been writing software to emulate other machines for almost as long as computers have existed. ACL2 is just another programming language in which such software can be written — albeit one that comes with a logical foundation and theorem prover allowing one to reason about programs running on the machine or even properties of the machine itself.
In fact, such operational semantics models played an important role in the evolution of ACL2.
ACL2 evolved from earlier theorem provers by Boyer and Moore. Those
earlier provers were the Edinburgh Pure Lisp Theorem prover, aka PLTP (see
bib::bm73 and bib::moore73), (1971--73), Thm (1974--79), and
Nqthm (1980--95) (see bib::bm97). The dates are approximate. Boyer
and Moore began working on ACL2 on August 14, 1989 and the first ACL2
proof (associativity of
Boyer and Moore's first foray into operational semantics for a computing machine shows up in Chapter 17 of bib::bm79 where they used Thm to prove a version of the McCarthy-Painter theorem verifying an expression compiler for a simple machine bib::mp67.
At the time, Boyer and Moore were employed at SRI and were working
part-time on the Software Implemented Fault Tolerance (SIFT) project. Their
task was to verify that a certain small fragment of machine code for the
Bendix 930 (BDX930) flight-control computer implemented a simple time-sharing
system. (Personal aside by J Moore: Having such an ambitious goal, in 1979,
astounds me in 2024, but it was a side-effect of youthful energy combined
with naivete and the excitement (and hype?) of that early period in the
history of mechanized formal methods.) To attack the problem they formalized
the necessary subset of the BDX930 instruction set operationally. But Thm
was not able to process the “large” system of definitions (30
pages). The problem was, in part, due to the representation of logical
constants in Thm's implementation. E.g., the logical constant
(cons (add1 (zero)) (add1 (add1 (zero))))
So Thm was rewritten to represent the constant
(quote (1 . 2)).
This required a major rewrite (affecting virtually every routine in the
system that inspected terms) and was a significant step toward Nqthm. (Note:
another formalization problem pushed Boyer and Moore in the same direction:
the desire to support verified “metafunctions,” which required
the formalization in the logic of a weak interpreter,
The BDX930 model was admitted to the improved “Thm” (now more like Nqthm) but Boyer and Moore then realized that the machine code implemented a time-sharing system only if every SIFT process, when compiled from the native Pascal, respected a bevy of unstated invariants on the machine code. They wrote a “minority report” explaining this. That report was contained in Sections 14 and 15 of the SIFT final report for the period September 1978 to June 1982. Section 14 describes the problem and Section 15 lists the 30 page BDX930 model. See bib::bm80, which has the provocative title “WHY IT IS IMPOSSIBLE TO PROVE THAT THE BDX930 DISPATCHER IMPLEMENTS A TIME-SHARING SYSTEM.”
Boyer and Moore left SRI for the University of Texas at Austin in 1981 and
Nqthm was fully formed shortly thereafter. The combination of Nqthm and some
brilliant students led to a remarkable string of projects, including the
FM8501 (and later the FM9001), the Computational Logic, Inc., verified stack,
and the Motorola 68020 model and its use in the emulation and verification of
machine code produced from the Berkeley C String Library by
That spurred Boyer and Moore to abandon the home grown Lisp supported by Nqthm and build a theorem prover for a subset of Common Lisp: ACL2. That way, operational models were just Common Lisp functions and could be run at Common Lisp speeds.
Of course, pressure on Kaufmann and Moore to improve ACL2 to provide higher capacity and more efficiency to load and process models of commercial processors continues to this day. See Sections 8 and 9 of bib::hkms17. Among many other changes made in response to industrial requests, many of which relate to operational models, are such things the invention of guards as an extralogical device to ensure that compiled code complies with the axioms, support for inlining and other directives to the compiler, the mbt directive, performance improvements in certification and the inclusion of certified files into a session, congruent single-threaded objects, nested single-threaded objects, patterned congruence rules, and an attachment mechanism for stobjs so that different memory models can be executed. See stobjs.