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.
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.
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 insure 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:
OBJ is a top-level global variable that contains the current
* If a function uses the formal parameter
OBJ, the only
``actual expression'' that can be passed into that slot is
thus, such functions can only operate on the current object.
* The accessors and updaters have a formal parameter named
thus, those functions can only be applied to the current object.
* 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.
* 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
* If a function calls an
OBJ updater, it must return
* When a top-level expression involving
OBJ returns an
object, 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.
We recommend that you next see stobj-example-1