|
|
|---|
|
|
|
|---|
farray -- A data structure for a field-addressable array.
Stobjs provide constant time lookup for stobj fields/arrays in ACL2, as opposed to lists which require linear time lookup for nth/update-nth operations. If one wants to store multiple fields within a stobj, they need to prove theorems about how writes to each field interact with each other field. This leads to poor proof convenience and proof efficiency (I believe these terms were used by J Moore at some point in our discussions and I've latched onto it) because each field leads to a quadratic number of theorems.
Instead, a stobj st can be defined with just one field: an array for memory, or mem. This field can be subdivided further into other arrays and scalars. In this way, a single array in a stobj can simulate a stobj with multiple fields. To accomplish this, an offset table is defined that redirects reads and writes to the proper field/subarray. With the proper invariants, one can show that writes to any field do not interfere with other fields. Furthermore, the addition of a field to an farray structure does not create any extra proof effort. This solves the problem of quadratic blowup of theorems for stobj data structures. (This approach is a generalization of an abstraction J Moore used in the M1 model.) The only catch is that all arrays and scalars will share the same type (60-bit signed-integers in this definition).
This approach is somewhat analogous to memory usage in a traditional C or C-like language. In theory, farrays can be embedded; that is, a field of an farray may contain another farray. This could very well be similar in execution efficiency and proof efficiency to record-like stobjs (Jared Davis) or abstract stobjs (Shilpi Goel and Matt Kaufmann).
The layout of this book is as follows:
This material is further described in Nathan Wetzler's dissertation available as a preprint or on the UT Digital Repository.
A talk on farray was presented at the ACL2 Seminar and the slides and figure are available online.