Major Section: ACL2 Documentation
In ACL2, a ``single-threaded object'' is a data structure whose use is so syntactically restricted that only one instance of the object need ever exist and its fields can be updated by destructive assignments.
Note: Novices are advised to avoid using single-threaded objects, perhaps
instead using community book
the least, consider using
avoid guard verification.
The documentation in this section is laid out in the form of a tour that visits the documented topics in a reasonable order. We recommend that you follow the tour the first time you read about stobjs. The list of all stobj topics is shown below. The tour starts immediately afterwards. Also see defstobj and, for so-called abstract stobjs, see defabsstobj.
As noted, a ``single-threaded object'' is a data structure whose use is so syntactically restricted that only one instance of the object need ever exist. Updates to the object must be sequentialized. This allows us to update its fields with destructive assignments without wrecking the axiomatic semantics of update-by-copy. For this reason, single-threaded objects are sometimes called ``von Neumann bottlenecks.''
From the logical perspective, a single-threaded object is an ordinary ACL2 object, e.g., composed of integers and conses. Logically speaking, ordinary ACL2 functions are defined to allow the user to ``access'' and ``update'' its fields. Logically speaking, when fields in the object, obj, are ``updated'' with new values, a new object, obj', is constructed.
But suppose that by syntactic means we could ensure that there were no more
references to the ``old'' object, obj. Then we could create obj' by
destructively modifying the memory locations involved in the representation
of obj. The syntactic means is pretty simple but draconian: the only
reference to obj is in the variable named
The consequences of this simple rule are far-reaching and require some
getting used to. For example, if
OBJ has been declared as a
single-threaded object name, then the following consequences ensue (but see
the discussion of congruent stobjs below for a slight relaxation).
OBJ is a top-level global variable that contains the current object,
o If a function uses the formal parameter
OBJ, the only ``actual
expression'' that can be passed into that slot is the variable
merely a term that ``evaluates to an obj''; thus, such functions can only
operate on the current object. So for example, instead of
(FOO (UPDATE-FIELD1 3 ST)) write
(LET ((ST (UPDATE-FIELD1 3 ST))) (FOO ST)).
o The accessors and updaters have a formal parameter named
those functions can only be applied to the current object.
o The ACL2 primitives, such as
CDR, may not be
applied to the variable
OBJ. Thus, for example, obj may not be consed
into a list (which would create another pointer to it) or accessed or
copied via ``unapproved'' means.
o The updaters return a ``new
OBJ object'', i.e., obj'; thus, when
an updater is called, the only variable which can hold its result is
o If a function calls an
OBJ updater, it must return an
(either as the sole value returned, or in
(mv ... OBJ ...); see mv).
o When a top-level expression involving
OBJ returns an
that object becomes the new current value of
What makes ACL2 different from other functional languages supporting such operations (e.g., Haskell's ``monads'' and Clean's ``uniqueness type system'') is that ACL2 also gives single-threaded objects an explicit axiomatic semantics so that theorems can be proved about them. In particular, the syntactic restrictions noted above are enforced only when single-threaded objects are used in function definitions (which might be executed outside of the ACL2 read-eval-print loop in Common Lisp). The accessor and update functions for single-threaded objects may be used without restriction in formulas to be proved. Since function evaluation is sometimes necessary during proofs, ACL2 must be able to evaluate these functions on logical constants representing the object, even when the constant is not ``the current object.'' Thus, ACL2 supports both the efficient von Neumann semantics and the clean applicative semantics, and uses the first in contexts where execution speed is paramount and the second during proofs.
defabsstobj events introduce stobjs.
See defstobj for more details about stobjs. In particular, a relatively
advanced notion of ``congruent stobjs'' is discussed there. The idea is to
allow a stobj,
st2, of the same ``shape'' as a given stobj,
be used in place of
defstobj keywords allow inlining
and renaming of stobj accessors and updaters.
But we are getting ahead of ourselves. To start the stobj tour, see stobj-example-1.