1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
NOTE: THIS IS LEGACY CODE. You probably want the new version
instead of this old version.
See :xdoc DEFRSTOBJ for information about the new version.
-------------------------------------------------------------------------------
Record-like STOBJs
Jared Davis
Centaur Technology
jared@centtech.com
-------------------------------------------------------------------------------
These books explain a way to model a processor's state that allows 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 a bunch of consing just to build the new state
object. This is good since it is nice for a processor model to execute
efficiently.
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 because you need a new
pair of get and set functions, but they are akin to records in that these
accessors have the same five theorems as in the misc/records book.)
This style of reasoning seems good. It has been used in the compositional
cutpoint techniques developed by John Matthews, J Moore, Sandip Ray, and Daron
Vroon, the "wormhole abstraction" of Dave Greve at Rockwell Collins, the work
of Eric Smith for automated cutpoint-based proofs, etc. There are probably
other people who are also using records, e.g., Rob Sumners.
There are a lot of things to note.
A consequence of looking at the state as a record is that you "lose" any type
information about the top-level fields. For instance, if you have a program
counter field that you introduce with:
(pc :type (unsigned-byte 64) :initially 0)
Then you will not know that (get :pc st) is always going to give you an
integer. I think this is an intrinsic problem with records, and nobody has yet
developed a record book that allows you to treat records whose fields have
different types. So practically speaking, you may need to do something like
fix the PC as you extract it. (Perhaps this defeats some of the advantages of
records?)
If a stobj only has non-array fields, then viewing it as a record is pretty
straightforward --- we basically have a key corresponding to each field. But
how do we handle array fields, which have their own collections of elements?
One approach might be to try to keep viewing the stobj as a flat record. For
instance, we might try to have the story be something like "arr[3] corresponds
to the field (:ARR . 3)" or similar. This is probably possible, but something
I didn't like about it was that it means we would also lose the type
information on the array elements.
Instead, I set things up so that the whole array looks like just one field in
the stobj. The array itself is represented as a typed record, with its own
get/set functions that satisfy the theorems of Greve and Wilding's typed
records book, i.e., the get-of-set theorm changes to return (fix val) instead
of just val, and we unconditionally have (typep (get addr arr)).
------------------------------------------------------------------------------
To get started using RSTOBJs, see basic-tests.lisp for examples of how to
define typed records and introduce machines with defrstobj.
Note that, at the moment, the defrstobj macro starts to get bogged down when
there are too many fields. The basic-tests.lisp file has a defrstobj with 30
fields, and it takes a couple of minutes already. We'll have to work on
improving this if we want to use defrstobj for more elaborate machine states.
If you want to understand how all of this actually works, you might start with
the demo files in the groundwork/ directory. These take an incremental
approach, first trying to handle the simplest kind of stobjs, and then
extending the idea to more complex stobjs. In particular:
1. demo1.lisp explains the main idea for a simple state that only has a
couple of unconstrained fields (not having to deal with arrays or type
restrictions makes the problem a bit easier).
2. demo2.lisp extends the idea to a stobj that has a field that is
constrained to be an integer. It seems pretty straightforward to put
simple type constraints on the fields.
3. demo3.lisp extends the idea to a stobj that has an array field (with
unconstrained elements). This is considerably more involved, but some of
the supporting definitions should be directly reusable.
4. demo4.lisp just cleans up demo3 and cuts down on the unnecessary theorems.
Extending the idea to arrays with types turned out to be pretty tricky. In
support of demo3/demo4, I developed the array-rec book. I tried to adapt Greve
and Wilding's implementation of typed records to get a typed version of this
book, and that effort is found in groundwork/typed-array-rec.lisp. But this
seemed to be basically unworkable.
Sol Swords and I then developed a new approach to typed records, which seems to
be a little nicer in that the "good" part of the record doesn't have to have
complex entries, but instead can just have good, well-formed elements.
I generalized our approach to arbitrary types and it was not difficult to adapt
the groundwork/array-rec book to the new typed record format. The result is
the typed-records book (and the def-typed-record book, which instantiates the
typed records for particular kinds of records).
5. demo5.lisp uses these new typed record stuff to redo demo4, but now with a
typed record instead of an untyped record as the logical representation of
the array.
After demo5, the only thing left to do is bundle up this approach into a nice
macro, so that we can introduce record-like stobjs at will. This is pretty
involved since stobjs have lots of options, e.g., we need to figure out how to
deal with type specifiers, etc. The end result is the defrstobj book.
-------------------------------------------------------------------------------
|
