Jared Davis
Record-like STOBJs
October 20, 2011

Abstract:

I will describe a way to model a processor's state that may allow for both
good execution efficiency and good reasoning efficiency.

The state is implemented as a STOBJ so it can be accessed efficiently and
updated destructively, without lots of consing just to build the new state
object.  This seems good since a processor model that runs quickly may be
more useful.

The state is reasoned about as if it were a "record" in the sense of the
misc/records book.  Well, it is not exactly a record since there are a new
pair of get/set functions instead of G and S, but the new functions have the
same five "record theorems."

Using misc/records in processor modeling seems to be pretty popular, see
for instance the compositional cutpoint techniques developed by John
Matthews, J Moore, Sandip Ray, and Daron Vroon; the "wormhole abstraction"
of Dave Greve; the work of Eric Smith for automated cutpoint-based proofs;
J's recent seminar talk; etc.