;; ========================== INTRODUCTION ===========================
farray: Field-addressable Arrays in ACL2
-- Nathan Wetzler
ACL2 Seminar
The University of Texas at Austin
January 27, 2015
;; ============================== GOALS ==============================
Part One. Describe the need for farray.
Part Two. Demonstrate farray implementation.
Auxilliary Goal: Feedback.
01/22
;; ===================================================================
;; ============================ PART ONE =============================
;; ===================================================================
Part One.
++ What are farrays?
++ Motivation
-- Lists
-- STOBJs
-- "Simple" Modifications
++ Proof Efficiency and Proof Convenience
++ Solutions
++ Conception
02/22
;; ======================== WHAT ARE FARRAYS? ========================
The farray data structure is an abstraction that provides access to multiple
array "fields" located in a single STOBJ array.
farrays are designed to maintain execution efficiency while providing better
proof efficiency and proof convenience than a typical multiple field STOBJ.
The idea was developed for and used during the construction of a fast(er) ACL2
model of a satisfiability proof checker.
03/22
;; =========================== MOTIVATION ============================
Why would someone want to use farrays when they have access to lists, records,
multiple-field STOBJs, abstract STOBJs, or any number of other data structures
available in the ACL2 system or its contributed books?
04/22
;; ============================== LISTS ==============================
Consider a state-based model constructed with lists:
(defun foo-model-listp (x) ; (x) object
(declare (xargs :guard t))
(and (true-listp x) ; using a true-list to represent state
(equal (len x) 3) ; 3 fields total
(integer-listp (nth 0 x)) ; field 1 is list of integers,
(equal (len (nth 0 x)) 10) ; and has length 10
(integerp (nth 1 x)) ; field 2 is scalar integer value
(integer-listp (nth 2 x)) ; field 3 is list of integers,
(equal (len (nth 2 x)) 5))) ; and has length 5
The function foo-model-listp recognizes an object that contains two sublists
and a scalar. Read and write functions could be defined for this model:
(defun field3-write-list (i v foo) ; (i)ndex, (v)alue, (foo) object
(declare (xargs :guard (and (foo-model-listp foo)
(integerp i)
(<= 0 i)
(< i 5)
(integerp v))))
(let* ((field3 (nth 2 foo)) ; get third field,
(new-field3 (update-nth i v field3)) ; write v @ position i,
(new-foo (update-nth 2 new-field3 foo))) ; write third field back
new-foo)) ; to foo, and return state
Every read and write takes a linear amount of time. If one intends to use this
model for execution, reads and writes to the state will be unbelievably slow.
05/22
;; ============================= STOBJS ==============================
ACL2 STOBJs (Single-Threaded OBJects) have the ability to interface with Lisp
arrays from ACL2, which improves the execution efficiency of ACL2 programs
using this data structure. Reasoning about STOBJs is relatively
straightforward because the logical model is constructed of lists. The cost of
the this approach is that STOBJs are syntactically limited so that updates to
the STOBJ are serialized (hence "single-threaded").
Consider this STOBJ definition designed to represent the same model described
by foo-model-listp:
(defstobj foo-model-stobj ; define new stobj called foo-model-stobj
(field1 :type (array integer (10)) ; field1 is array of 10 integers,
:initially 0) ; all initialized to 0
(field2 :type integer ; field2 is scalar integer,
:initially 0) ; initialized to 0
(field3 :type (array integer (5)) ; field3 is array of 5 integers,
:initially 0)) ; all initialized to 0
This STOBJ definition creates a recognizer and creator for the STOBJ. It also
creates a recognizer, an accessor, an updater, a length operator, and
optionally a resizer for each field in the STOBJ. The definition above creates
13 function definitions.
A theory needs to be constructed describing how each of these functions
interacts with each other function, a quadratic number of theorems.
06/22
;; ===================== "SIMPLE" MODIFICATIONS ======================
Suppose the foo-model-stobj is under active development. Perhaps a new field,
called field4, is added to the STOBJ.
(defstobj foo-model-stobj ; define new stobj called foo-model-stobj
(field1 :type (array integer (10)) ; field1 is array of 10 integers,
:initially 0) ; all initialized to 0
(field2 :type integer ; field2 is scalar integer,
:initially 0) ; initialized to 0
(field3 :type (array integer (5)) ; field3 is array of 5 integers,
:initially 0) ; all initialized to 0
(field4 :type (array integer (20)) ; field4 is array of 20 integers,
:initially 0)) ; all initialized to 0
This change adds 4 new functions associated with field4, but it also creates a
need for theorems relating field4 operations to every other field *and*
theorems relating every other field to field4.
This should be a relatively simple modification to the data structure, but the
user has manage a quadratic increase in both the amount of theorems that need
to be written and the certification time of the book containing this data
structure.
07/22
;; ============= PROOF EFFICIENCY AND PROOF CONVENIENCE ==============
These terms were introduced by J Moore and represent the problem with the
previous two methods:
Proof Efficiency -- The rate at which a proof can be checked
Proof Convenience -- The ease of expressing a proof and using those theorems
The list-based and STOBJ-based solutions have poor proof efficiency and poor
proof convenience.
Every read and write function will need a description of how it affects the
model and how it interacts with all other read and write functions. This leads
to a large number of theorems that need to be written and verified.
Verbose guard management to ensure state invariants are maintained.
08/22
;; ============================ SOLUTIONS ============================
A few solutions already exist for this problem.
-- defaggregate (found in "std/util/defaggregate.lisp") can be used to create
record-like structures that contain fields. The defaggregate event defines
creators, accessors, updaters, etc. and automatically proves some theorems
about the data structure. Execution efficiency is still limited by the
list-based implementation however (but there is some support for hons-ing).
-- Shilpi Goel uses extensive macros in the STOBJ-based X86 ISA model to
automatically generate theorems associated with fields in the STOBJ. This
method benefits from faster array access through STOBJs and removes the
tedium of writing theorems about STOBJ fields, thereby increasing proof
convenience. The problem is that these proofs still exist and can take
longer to verify for more complicated models.
None of these are a perfect fit for the problem, however.
09/22
;; =========================== CONCEPTION ============================
Warren Hunt remarked that one can write C-style programs where there is no
notion of memory other than as a single, flat array. Pointers can indicate the
start of a particular structure (like a struct or array), but the underlying
memory is still flat. This approach is transparent and relies on the user to
perform memory management. Hunt believed that this would be a good approach
for efficient coding in ACL2.
J Moore abstracted the notion of fields in his M1 model, creating parameterized
functions that read and write to any field (called "uniform access"). This
approach was for a list-based model of a machine state, and by proving only a
few theorems about the "uniform access" functions, Moore derived a theory for
any field in the model.
farrays are a combination of these two ideas and were guided by extensive work
on trying to implement efficient, verified programs in ACL2.
10/22
;; ===================================================================
;; ============================ PART TWO =============================
;; ===================================================================
Part Two.
++ farray Overview
++ field-table
++ farrayp Definition
++ Predicates and Operations
++ fread
++ fwrite
++ Theorems
++ field-memberp
++ Current and Future Work
-- fresize
-- farray-move
-- relative-to-absolute
-- Variable STOBJ and field
++ Uses
11/22
;; ========================= FARRAY OVERVIEW =========================
An farray structure is stored in a STOBJ named "st" (short for "STate") with
one array field named "mem" (short for "MEMory") of 60-bit signed-byte
integers.
(defstobj st ; new stobj st
(mem :type (array (signed-byte 60) ; one field named mem is array
(*init-mem-size*)) ; of 60-bit signed integers
:initially 0 ; all values are initially zero
:resizable t) ; and array is resizable
:inline t ; accessors/updaters are inlined
:renaming ((update-memi !memi) ; update-memi renamed to !memi
(mem-length mem-len))) ; mem-length renamed to mem-len
A start position indicates where the farray structure begins in mem. This
allows multiple farray structures and even nested farray structures.
The value at the start position is the number of fields in the farray.
A field is a number from 1 to n. Constants can be defined to add meaning to
each field number.
The location of each field will be stored in a field table.
Reads and writes to an index in a field will access the location of the field
and then compute the offset for the index. In other words, every access
involves indirection.
[[Image]]
12/22
;; =========================== FIELD-TABLE ===========================
The field-table stores the indices of all fields associated with the farray.
The predicate field-tablep ranges from index i to index end in mem and checks
the following properties for the value at index i:
-- An integer
-- Greater than or equal to 0
-- Less then the length of mem
-- Greater than end
-- Less than the value at index i+1
13/22
;; ======================== FARRAY DEFINITION ========================
The predicate farrayp contains all invariants for the farray data structure.
(defun farrayp (start st) ; (start), (st)ate
(declare (xargs :guard t
:stobjs (st)))
(and (stp st) ; valid STOBJ st
(integerp start) ; start is int
(<= 0 start) ; start non-negative
(< start (mem-len st)) ; start in range
(integerp (memi start st)) ; value at start is int
(<= 0 (memi start st)) ; value at start non-negative
(< (+ start (memi start st) 1) ; end is in range
(mem-len st))
(< (memi (+ start (memi start st) 1) st) ; value at end
(mem-len st)) ; is in range
(sb60p (mem-len st)) ; length of mem < 2^59
(field-tablep (+ start 1) ; field table from start+1
(+ start (memi start st) 1) ; to end position
st))) ; in st
14/22
;; ==================== PREDICATES AND OPERATIONS ====================
There are two predicates and two operators associated with farray:
(num-fields start st)
-- Returns number of fields.
(fieldp f start st)
-- Checks that f is an integer, greater than or equal to one, and less than
or equal to (num-fields start st).
(flength f start st)
-- Returns the length of the field, defined as the difference between the
field index for f and the field index for f+1.
(field-offsetp offset f start st)
-- Checks that offset is an integer, greater than or equal to zero, and
less than the length of the field f.
15/22
;; ============================== FREAD ==============================
The fread accessor reads values in a field of an farray. The correct index in
mem is calculated based on the farray start location and field table entry.
(defun fread (f offset start st) ; (f)ield, (offset), (start), (st)ate
(declare (xargs :guard (and (farrayp start st)
(fieldp f start st)
(field-offsetp offset f start st))
:stobjs (st)))
(memi (+ (memi (+ start f) st) ; Read the field index and add that
offset) ; to the offset to obtain a new index.
st)) ; Read that index in mem and return result.
Thus, an fread consists of two additions and two reads from mem.
This function can be inlined and properly typed for better execution
efficiency.
16/22
;; ============================= FWRITE ==============================
The fwrite updater writes a value to a field of an farray. The correct index
in st is calculated based on the farray start location and the field table
entry.
(defun fwrite (f offset v start st) ; (f)ield, (offset), (v)alue, (start),
; (st)ate
(declare (xargs :guard (and (farrayp start st)
(fieldp f start st)
(field-offsetp offset f start st)
(sb60p v))
:stobjs (st)))
(!memi (+ (memi (+ start f) st) ; Read the field index and add that to
offset) ; the offset to obtain a new index.
v ; Write the value v to that index
st)) ; in mem.
Thus, an fwrite consists of two additions, a read from mem, and a write to mem.
Again, this function can be inlined and properly typed for better execution
efficiency.
17/22
;; ============================ THEOREMS =============================
A few of the theorems about farray primitives:
-- fread always returns a signed-byte 60.
-- fwrite always returns an farrayp.
-- fwrite does not affect flength.
-- An fwrite followed by an fread results in the value written if the fields
and offsets are equal.
-- Two fwrites to the same field and offset are the same as one write.
-- An fwrite of the value already at the field and offset is the same as no
fwrite.
-- Two fwrites to distinct fields can be canonicalized.
-- Two fwrites to the same field with distinct offsets can be canonicalized.
-- The number of fields is not affected by fwrite.
-- fieldp is not affected by fwrite
-- field-offsetp is not affected by fwrite.
18/22
;; ========================== FIELD-MEMBERP ==========================
A field-memberp predicate is included in the farray book. This function checks
for membership of an element within a given range of a field. This is useful
when a certain range of a field corresponds to a list.
(field-memberp e top bottom f start st)
-- Check if the element e is within the offsets top and bottom of field f
for the farray that begins at start in st.
The interaction between field-memberp and fwrite is somewhat complicated, but
many theorems help resolve nested calls.
19/22
;; ===================== CURRENT AND FUTURE WORK =====================
The farray data structure can be greatly improved. A few ideas:
-- The length of each field is constant once an farray is defined. An fresize
function can be defined that would resize a field by modifying the
field-table and shifting data to new positions. This work has partially
been accomplished. The field-table adjustment function has been defined and
proven to maintain the farray invariant.
-- The location of the farray in is constant. An farray-move could be defined
that would shift the entire farray to a new start location.
-- All freads and fwrites require an extra mem access and some arithmetic. A
relative-to-absolute function (and absolute-to-relative function) can be
defined that would convert a field-offsetp to an absolute index in mem (and
vice versa). Accesses and updates to mem with an absolute address should
preserve the farray structure. Users could "drop" to absolute indices for
important functions.
-- The farray structure is limited to the STOBJ name "st" and the field name
"mem". One should be able to define farrays in such a way that they can be
used with other STOBJ names.
20/22
;; ============================== USES ===============================
The farray data structure is used to define assignments in a satisfiability
proof checker. This particular farray contains a field for the number of
variables, a stack of literals stored as an array field with an end location
field, and a lookup table array field indexed by literal.
The algorithm that uses farrays is proven equivalent to a list-based algorithm,
which has a proof of correctness.
21/22
;; =========================== CONCLUSION ============================
The farray data structure is an abstraction that provides access to multiple
array "fields" located in a single STOBJ array.
farrays are designed to maintain execution efficiency while providing better
proof efficiency and proof convenience than a typical multiple field STOBJ.
The idea was developed for and used during the construction of a fast(er) ACL2
model of a satisfiability proof checker.
22/22
;; ===================================================================