STOBJ

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 books/data-structures/structures.lisp. At the least, consider using (set-verify-guards-eagerness 0) to 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.

Some Related Topics

• DECLARE-STOBJS -- declaring a formal parameter name to be a single-threaded object

• DEFSTOBJ -- define a new single-threaded object

• RESIZE-LIST -- list resizer in support of stobjs

• STOBJ-EXAMPLE-1 -- an example of the use of single-threaded objects

• STOBJ-EXAMPLE-1-DEFUNS -- the defuns created by the counters stobj

• STOBJ-EXAMPLE-1-IMPLEMENTATION -- the implementation of the counters stobj

• STOBJ-EXAMPLE-1-PROOFS -- some proofs involving the counters stobj

• STOBJ-EXAMPLE-2 -- an example of the use of arrays in single-threaded objects

• STOBJ-EXAMPLE-3 -- another example of a single-threaded object

• WITH-LOCAL-STATE -- locally bind state

• WITH-LOCAL-STOBJ -- locally bind a single-threaded object

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 OBJ.

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).

o OBJ is a top-level global variable that contains the current object, obj.

o If a function uses the formal parameter OBJ, the only ``actual expression'' that can be passed into that slot is the variable OBJ, not 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 OBJ, thus, those functions can only be applied to the current object.

o The ACL2 primitives, such as CONS, CAR and 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 OBJ.

o If a function calls an OBJ updater, it must return an OBJ object (either as the sole value returned, or in (mv ... OBJ ...); see mv).

o When a top-level expression involving OBJ returns an OBJ object, that object becomes the new current value of OBJ.

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.

Defstobj and 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, st1, to be used in place of st1. Other 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.