Stobj
Single-threaded objects or ``von Neumann bottlenecks''
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 std::defaggregate or community book
books/data-structures/structures.lisp. At the least, consider using
(set-verify-guards-eagerness 0) to avoid guard
verification.
This topic introduces the notion of a ``stobj'', or single-threaded object.
It concludes with a link to a tour that introduces the use of stobjs by way of
examples. We recommend that you follow that link the first time you read
about stobjs. Detailed reference documentation about stobjs may be found in
the subtopics listed at the end below; in particular 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 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 at the end of this topic for some relaxations).
- OBJ is a top-level global variable that contains the current object,
obj.
- If a function uses the formal parameter OBJ that is declared as a
stobj, 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)). And instead of (MV X (LET ((ST (UPDATE-FIELD1 3 ST))) (FOO
ST))) write (LET ((ST (UPDATE-FIELD1 3 ST))) (MV X ST)).
- The accessors and updaters have a formal parameter named OBJ, so by
the rule just above, those functions can only be applied to the current
object. The recognizer is the one exception to the rule: it may be applied
either the OBJ or to an ordinary (non-stobj) 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 (either as the sole value returned, or in (mv ... OBJ ...); see
mv).
- When a top-level expression involving OBJ returns an OBJ
object, that object becomes the new current value of OBJ.
There are other functional languages supporting single-threadedness, for
example Haskell's ``monads'' and Clean's ``uniqueness type system''. Of
course, ACL2 provides a theorem prover that can prove theorems that involve
such constructs.
Note that the syntactic restrictions noted above are enforced only when
single-threaded objects are encountered directly in the top-level loop or are
used in function definitions; 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, and a
:non-executable keyword can be used to defer or totally avoid creating a
“global” stobj for the given stobj name.
But we are getting ahead of ourselves. To start the stobj tour recommended
earlier in this topic, see stobj-example-1.
Subtopics
- Defstobj
- Define a new single-threaded object
- Defabsstobj
- Define a new abstract single-threaded object
- Stobj-table
- A stobj field mapping stobj names to stobjs
- Preservation-thms
- Automation for proving that stobj-modifying functions preserve
certain properties
- Nested-stobjs
- Using stobjs that contain stobjs
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs
with the reasoning efficiency of records. They are designed for modeling,
e.g., the state of a processor or virtual machine.
- With-global-stobj
- Operate on a global single-threaded object
- User-stobjs-modified-warnings
- Interactions of trans-eval with stobjs that violate
applicative semantics
- Stobj-example-1
- An example of the use of single-threaded objects
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs
with the reasoning efficiency of records. They are designed for modeling,
e.g., the state of a processor or virtual machine.
- Stobj-example-3
- Another example of a single-threaded object
- Stobj-example-1-proofs
- Some proofs involving the counters stobj
- With-local-stobj
- Locally bind a single-threaded object
- Stobj-example-1-defuns
- The defuns created by the counters stobj
- Declare-stobjs
- Declaring a formal parameter name to be a single-threaded object
- Trans-eval-and-stobjs
- How user-defined stobjs are handled by trans-eval
- With-local-state
- Locally bind state
- Stobj-example-2
- An example of the use of arrays in single-threaded objects
- Stobj-example-1-implementation
- The implementation of the counters stobj
- Add-global-stobj
- Add a global stobj with a given name
- Swap-stobjs
- Swap two congruent stobjs
- Resize-list
- List resizer in support of stobjs
- Nth-aliases-table
- A table used to associate names for nth/update-nth printing
- Def-stobj-frame
- Automatically, opportunistically generate nth/update-nth frame theorems for a function that accesses or updates a stobj.
- Trans-eval-and-locally-bound-stobjs
- Trans-eval deals in global stobjs.
- Std/stobjs
- A library for working with stobjs.
- Count-keys
- Count the number of keys in association list
- Update-nth-array
- Update a stobj array
- Remove-global-stobj
- Remove a global stobj with a given name
