STOBJ

single-threaded objects or ``von Neumann bottlenecks'' 
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.

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:

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

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

* The accessors and updaters have a formal parameter named OBJ, thus, those functions can only be applied to the current object.

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

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

* If a function calls an OBJ updater, it must return an OBJ object.

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

To start the stobj tour, see stobj-example-1.