DECLARE-STOBJS

declaring a formal parameter name to be a single-threaded object 
Major Section:  STOBJ

When a defun uses one of its formals as a single-threaded object (stobj), the defun must include a declaration that the formal it to be so used. An exception is the formal ``state,'' which if not declared as explained below, may still be used provided an appropriate global ``declaration'' is issued: see set-state-ok.

If the formal in question is counters then an appropriate declaration is 

(declare (xargs :stobjs counters))
or, more generally, 
(declare (xargs :stobjs (... counters ...)))
where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the names have previously been defined as single-threaded objects with defstobj.

The obvious question then arises: Why does ACL2 insist that you declare stobj names before using them in defuns if you can only declare names that have already been defined with defstobj? What would go wrong if a formal were treated as a single-threaded object if and only if it had already been so defined?

Suppose that one user, say Jones, creates a book in which counters is defined as a single-threaded object. Suppose another user, Smith, creates a book in which counters is used as an ordinary formal parameter. Finally, suppose a third user, Brown, wishes to use both books. If Brown includes Jones' book first and then Smith's, then Smith's function treats counters as single-threaded. But if Brown includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to insure that the definition is processed the same way no matter what the context.












































































STOBJ-EXAMPLE-1

an example of the use of single-threaded objects 
Major Section:  STOBJ

Suppose we want to sweep a tree and (1) count the number of interior nodes, (2) count the number of tips and (3) keep a record of every tip we encounter that is an integer. We could use a single-threaded object as our ``accumulator''. Such an object would have three fields, one holding the number of nodes seen so far, one holding the number of tips, and one holding all the integer tips seen.

The following event declares counters to be a single-threaded object. 

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))
It has three fields, NodeCnt, TipCnt, and IntTipsSeen. (As always in ACL2, capitalization is irrelevant in simple symbol names, so the first name could be written nodecnt or NODECNT, etc.) Those are the name of the accessor functions for the object. The corresponding update functions are named update-NodeCnt, update-TipCnt and update-IntTipsSeen.

If you do not like the default function names chosen above, there is a feature in the defstobj event that allows you to specify other names.

If you want to see the ACL2 definitions of all the functions defined by this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level ``global variable'' counters in the ACL2 read-eval-print loop we get: 

ACL2 !>counters
<counters>
Note that the value printed is ``<counters>''. Actually, the value of counters is (0 0 NIL). But ACL2 always prints single-threaded objects in this non-informative way because they are usually so big that to do otherwise would be unpleasant.

Had you tried to evaluate the ``global variable'' counters before declaring it a single-threaded object, ACL2 would have complained that it does not support global variables. So a lesson here is that once you have declared a new single-threaded object your top-level forms can reference it. In versions of ACL2 prior to Version 2.4 the only variable enjoying this status was STATE. single-threaded objects are a straightforward generalization of the long-implemented von Neumann state feature of ACL2.

We can access the fields of counters as with: 

ACL2 !>(NodeCnt counters)
0
ACL2 !>(IntTipsSeen counters)  
NIL
and we can set the fields of counters as with: 
ACL2 !>(update-NodeCnt 3 counters)
<counters>
ACL2 !>(NodeCnt counters)
3
Observe that when we evaluate an expression that returns a counter object, that object becomes the ``current value'' of counters.

Here is a function that ``converts'' the counters object to its ``ordinary'' representation: 

(defun show-counters (counters)
  (declare (xargs :stobjs (counters)))
  (list (NodeCnt counters)
        (TipCnt counters)
        (IntTipsSeen counters)))
Observe that we must declare, at the top of the defun, that we mean to use the formal parameter counters as a single-threaded object! If we did not make this declaration, the body of show-counters would be processed as though counters were an ordinary object. An error would be caused because the accessors used above cannot be applied to anything but the single-threaded object counters. If you want to know why we insist on this declaration, see declare-stobjs.

When show-counters is admitted, the following message is printed: 

Since SHOW-COUNTERS is non-recursive, its admission is trivial.  We
observe that the type of SHOW-COUNTERS is described by the theorem
(AND (CONSP (SHOW-COUNTERS COUNTERS))
     (TRUE-LISTP (SHOW-COUNTERS COUNTERS))).
We used primitive type reasoning.


(SHOW-COUNTERS COUNTERS) => *.

The last line of the message is the ``signature'' of show-counters and conveys the information that the first argument is the single-threaded object counters and the only result is an ordinary object.

Here is an example of show-counters being called: 

ACL2 !>(show-counters counters)
(3 0 NIL)
This is what we would see had we set the NodeCnt field of the initial value of counters to 3, as we did earlier in this example.

We next wish to define a function to reset the counters object. We could define it this way: 

(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (let ((counters (update-NodeCnt 0 counters)))
    (let ((counters (update-TipCnt 0 counters)))
      (update-IntTipsSeen nil counters))))
which ``successively'' sets the NodeCnt field to 0, then the TipCnt field to 0, and then the IntTipsSeen field to nil and returns the resulting object.

However, the nest of let expressions is tedious and we use this definition instead. This definition exploits a macro, here named ``seq'' (for ``sequentially'') which evaluates each of the forms given, binding their results successively to the stobj name given. 

(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (seq counters
       (update-NodeCnt 0 counters)
       (update-TipCnt 0 counters)
       (update-IntTipsSeen nil counters)))
This definition is syntactically identical to the one above, after macro expansion. Our definition of seq is shown below and is not part of native ACL2. 
(defmacro seq (stobj &rest rst)
  (cond ((endp rst) stobj)
        ((endp (cdr rst)) (car rst))
        (t `(let ((,stobj ,(car rst)))
             (seq ,stobj ,@(cdr rst))))))

The signature printed for reset-counters is 

(RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example. 

ACL2 !>(show-counters counters)
(3 0 NIL)
ACL2 !>(reset-counters counters)
<counters>
ACL2 !>(show-counters counters)
(0 0 NIL)

Here finally is a function that uses counters as a single-threaded accumulator to collect the desired information about the tree x. 

(defun sweep-tree (x counters)
  (declare (xargs :stobjs (counters)))
  (cond ((atom x)
         (seq counters
              (update-TipCnt (+ 1 (TipCnt counters)) counters)
              (if (integerp x)
                  (update-IntTipsSeen (cons x (IntTipsSeen counters))
                                  counters)
                counters)))
        (t (seq counters
                (update-NodeCnt (+ 1 (NodeCnt counters)) counters)
                (sweep-tree (car x) counters)
                (sweep-tree (cdr x) counters)))))
We can paraphrase this definition as follows. If x is an atom, then increment the TipCnt field of counters and then, if x is an integer, add x to the IntTipsSeen field, and return counters. On the other hand, if x is not an atom, then increment the NodeCnt field of counters, and then sweep the car of x and then sweep the cdr of x and return the result.

Here is an example of its execution. We have displayed the input tree in full dot notation so that the number of interior nodes is just the number of dots. 

ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3)
                     . (4 . (5 . d)))
                   counters)
<counters>
ACL2 !>(show-counters counters)
(7 8 (5 4 3 2 1))
ACL2 !>(reset-counters counters)
<counters>
ACL2 !>(show-counters counters)
(0 0 NIL)

The counters object has two integer fields and a field whose type is unrestricted. single-threaded objects support other types of fields, such as arrays. We deal with that in the stobj-example-2. But we recommend that you first consider the implementation issues for the counters example (in stobj-example-1-implementation) and then consider the proof issues (in stobj-example-1-proofs).












































































STOBJ-EXAMPLE-1-DEFUNS

the defuns created by the counters stobj 
Major Section:  STOBJ

Consider the event shown in stobj-example-1: 

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is not declared with the :stobjs xarg even though we insist that the argument be a stobj in calls of these functions. This ``mystery'' is explained below.

(defun NodeCntp (x)                 ;;; Recognizer for 1st field
  (declare (xargs :guard t))
  (integerp x))


(defun TipCntp (x)                  ;;; Recognizer for 2nd field
  (declare (xargs :guard t))
  (integerp x))


(defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
  (declare (xargs :guard t) (ignore x))
  t)


(defun countersp (counters)         ;;; Recognizer for object
  (declare (xargs :guard t))
  (and (true-listp counters)
       (= (length counters) 3)
       (NodeCntp (nth 0 counters))
       (TipCntp (nth 1 counters))
       (IntTipsSeenp (nth 2 counters))))


(defun NodeCnt (counters)           ;;; Accessor for 1st field
  (declare (xargs :guard (countersp counters)))
  (nth 0 counters))


(defun update-NodeCnt (v counters)  ;;; Updater for 1st field
  (declare (xargs :guard
                  (and (integerp v)
                       (countersp counters))))
  (update-nth 0 v counters))


(defun TipCnt (counters)            ;;; Accessor for 2nd field
  (declare (xargs :guard (countersp counters)))
  (nth 1 counters))


(defun update-TipCnt (v counters)   ;;; Updater for 2nd field
  (declare (xargs :guard
                  (and (integerp v)
                       (countersp counters))))
  (update-nth 1 v counters))


(defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
  (declare (xargs :guard (countersp counters)))
  (nth 2 counters))


(defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
  (declare (xargs :guard (countersp counters)))
  (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and then a recognizer for the counters object itself. Then, for each field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a counterp for their counter argument and an appropriate value for the new field values.

You can see all of the defuns added by a defstobj event by executing the event and then using the :pcb! command on the stobj name. E.g., 

ACL2 !>:pcb! counters
will print the defuns above.

We now clear up the ``mystery'' mentioned above. Note, for example in TipCnt, that the formal counters is used. From the discussion in stobj-example-1 it has been made clear that TipCnt can only be called on the counters object. And yet, in that same discussion it was said that an argument is so treated only if it it declared among the :stobjs in the definition of the function. So why doesn't TipCnt include something like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows. At the time TipCnt was defined, during the introduction of the counters stobj, the name ``counters'' was not yet a single-threaded object. The introduction of a new single-threaded object occurs in three steps: (1) The new primitive recognizers, accessors, and updaters are introduced as ``ordinary functions,'' producing their logical axiomatizations. (2) The executable counterparts are defined in raw Lisp to support destructive updating. (3) The new name is declared a single-threaded object to insure that all future use of these primitive respects the single-threadedness of the object. The functions defined as part of the introduction of a new single-threaded object are the only functions in the system that have undeclared stobj formals other than state.

You may return to stobj-example-1 here.












































































STOBJ-EXAMPLE-1-IMPLEMENTATION

the implementation of the counters stobj 
Major Section:  STOBJ

the event 

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))
discussed in stobj-example-1, creates a Common Lisp object to represent the current value of counters. That object is created by evaluating the following ``raw'' (non-ACL2) Common Lisp form: 
(list (make-array 1 :element-type 'integer
                  :initial-element '0)
      (make-array 1 :element-type 'integer
                  :initial-element '0)
      'nil)
and the value is stored in the Common Lisp global variable named *the-live-counters*.

Thus, the counters object is a list of length three. The first two elements are arrays of size 1 and are used to hold the NodeCnt and TipCnt fields. The third element is the IntTipsSeen field. The first two fields are represented by arrays so that we can implement the integer type specification efficiently. Generally, integers are ``boxed'' in Common Lisp. Creating a new integer requires creating a new box to put it in. But in some lisps the integers inside arrays of integers are not boxed.

The function update-NodeCnt is defined in raw Lisp as: 

(defun NodeCnt (counters)
  (the integer
       (cond ((eq counters *the-live-counters*)
              (aref (the (simple-array integer (1)) (car counters))
                    0))
             (t (nth 0 counters)))))
Observe that if NodeCnt is called on ``the live counters'' the function accesses the car, to get an array of size 1, and then uses aref to access the 0th element of that array.

The function update-NodeCnt is defined in raw Lisp as: 

(defun update-NodeCnt (v counters)
  (declare (type integer v))
  (cond ((eq counters *the-live-counters*)
         (setf (aref (the (simple-array integer (1)) (car counters))
                     0)
               (the integer v))
         counters)
        (t (update-nth 0 v counters))))
Note that when this function is called on the live counters it does not create a new list of length three, but ``smashes'' the existing one.

One way to see all the functions defined by a given defstobj is to evaluate the defstobj event and then evaluate, in the ACL2 loop, the expression (global-val 'cltl-command (w state)). That will print a lisp object that you can probably figure out.

We now recommend that you look at stobj-example-1-proofs.












































































STOBJ-EXAMPLE-1-PROOFS

the implementation of the counters stobj 
Major Section:  STOBJ

Consider again the event 

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))
discussed in stobj-example-1, followed by the definition 
(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (seq counters
       (update-NodeCnt 0 counters)
       (update-TipCnt 0 counters)
       (update-IntTipsSeen nil counters)))
which, because of the seq macro in stobj-example-1, is just syntactic sugar for 
(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (let ((counters (update-NodeCnt 0 counters)))
    (let ((counters (update-TipCnt 0 counters)))
      (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

(defthm reset-counters-is-constant
  (implies (countersp x)
           (equal (reset-counters x)
                  '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem is unusual in two respects.

First, it calls reset-counters on an argument other than the variable counters! That is allowed in theorems; logically speaking, the stobj functions are indistinguishable from ordinary functions. Their use is syntactically restricted only in defuns, which might be compiled and run in raw Lisp. Those restrictions allow us to implement stobj modification destructively. But logically speaking, reset-counters and other stobj ``modifying'' functions just create new objects, constructively.

Second, the theorem above explicitly provides the hypothesis that reset-counters is being applied to an object satisfying countersp. Such a hypothesis is not always required: reset-counters is total and will do something no matter what x is. But in this particular case, the result is not '(0 0 nil) unless x is, at least, a true-list of length three.

To make a long story short, to prove theorems about stobj functions you behave in exactly the way you would to prove the same theorems about the same functions defined without the stobj features.

How can we prove the above theorem? Unfolding the definition of reset-counters shows that (reset-counters x) is equal to 

(update-IntTipsSeen nil
  (update-TipCnt 0 
    (update-NodeCnt 0 x)))
which in turn is 
(update-nth 2 nil
 (update-nth 1 0
  (update-nth 0 0 x))).
Opening up the definition of update-nth reduces this to 
(list* 0 0 nil (cdddr x)).
This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is nil.

Unfortunately, that last fact requires a lemma. The most specific lemma we could provide is 

(defthm special-lemma-for-counters
  (implies (countersp x)
           (equal (cdddr x) nil)))
but if you try to prove that lemma you will find that it requires some reasoning about len and true-listp. Furthermore, the special lemma above is of interest only for counters.

The following lemma about len is the one we prefer. 

(defthm equal-len-n
  (implies (syntaxp (quotep n))
           (equal (equal (len x) n)
                  (if (integerp n)
                      (if (< n 0)
                          nil
                        (if (equal n 0)
                            (atom x)
                          (and (consp x)
                               (equal (len (cdr x)) (- n 1)))))
                    nil))))
This lemma will simplify any equality in which a len expression is equated to any explicitly given constant n, e.g., 3, reducing the equation to a conjunction of consp terms about the first n cdrs.

If the above lemma is available then ACL2 immediately proves 

(defthm reset-counters-is-constant
  (implies (countersp x)
           (equal (reset-counters x)
                  '(0 0 nil))))

The point is presumably well made: proving theorems about single- threaded object accessors and updaters is no different than proving theorems about other recursively defined functions on lists.

Another lemma that is useful in reasoning about single-threaded objects is 

(defthm update-nth-update-nth-diff
  (implies (not (equal (nfix i1) (nfix i2)))
           (equal (update-nth i1 v1 (update-nth i2 v2 l))
                  (update-nth i2 v2 (update-nth i1 v1 l))))
  :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))
This lemma is due to Matt Wilding.

We now recommend that you see stobj-example-2.












































































STOBJ-EXAMPLE-2

an example of the use of arrays in single-threaded objects 
Major Section:  STOBJ

The following event 

(defstobj ms
  (pcn  :type integer                  :initially 0)
  (mem  :type (array integer (100000)) :initially -1)
  (code :type t                        :initially nil))
introduces a single-threaded object named ms (which stands for ``machine state''). The object has three fields, a pcn or program counter, a mem or memory, and a code field.

The mem field is occupied by an object of type (array integer (100000)). Logically speaking, this is a list of length 100000, each element of which is an integer. But in the underlying implementation of the ms object, this field is occupied by a raw Lisp array of size 1000000.

You might expect the above defstobj to define the accessor function mem and the updater update-mem. That does not happen!.

The above event defines the accessor function memi and the updater update-memi. These functions do not access/update the mem field of the ms object; they access/update the individual elements of the array in that field.

In particular, the logical definitions of the two functions are: 

(defun memi (i ms)
  (declare (xargs :guard
                  (and (integerp i)
                       (<= 0 i)
                       (< i 100000)
                       (msp ms))))
  (nth i (nth 1 ms)))


(defun update-memi (i v ms)
  (declare (xargs :guard
                  (and (integerp i)
                       (<= 0 i)
                       (< i 100000)
                       (integerp v)
                       (msp ms))))
  (update-nth 1 (update-nth i v (nth 1 ms)) ms))

For example, to access thef 511th (0-based) memory location of the current ms you could evaluate: 

ACL2 !>(memi 511 ms)
-1
The answer is -1 initially, because that is the above-specified initial value of the elements of the mem array.

To set that element you could do 

ACL2 !>(update-memi 511 777 ms)
<ms>
ACL2 !>(memi 511 ms)
777

The raw Lisp implementing these two functions is shown below. 

(defun memi (i ms)
  (declare (type (integer 0 99999) i))
  (the integer
       (cond ((eq ms *the-live-ms*)
              (aref (the (simple-array integer (100000))
                         (car (cdr ms)))
                    (the (integer 0 99999) i)))
             (t (nth i (nth 1 ms))))))


(defun update-memi (i v ms)
  (declare (type (integer 0 99999) i)
           (type integer v))
  (cond ((eq ms *the-live-ms*)
         (setf (aref (the (simple-array integer (100000))
                          (car (cdr ms)))
                     (the (integer 0 99999) i))
               (the integer v))
         ms)
        (t (update-nth 1 (update-nth i v (nth 1 ms))
                    ms))))

If you want to see the raw Lisp supporting a defstobj, execute the defstobj and then evaluate the ACL2 form (global-val 'cltl-command (w state)). The s-expression printed will probably be self-explanatory given the examples here.

We now recommend that you read stobj-example-3.












































































STOBJ-EXAMPLE-3

another example of a single-threaded object 
Major Section:  STOBJ

The event 

(defstobj $s
  (x :type integer :initially 0)
  (a :type (array (integer 0 9) (3)) :initially 9))
introduces a stobj named $S. The stobj has two fields, X and A. The A field is an array. The X field contains an integer and is initially 0. The A field contains a list of three integers, each between 0 and 9, inclusively. Initially, each of the elements of the A field is 9.

This event introduces the following sequence of definitions: 

(DEFUN XP (X) ...)               ; recognizer for X field
(DEFUN AP1 (X N) ...)            ; aux fn for recogizer of A field
(DEFUN AP (X) ...)               ; recognizer of A field
(DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
(DEFUN X ($S) ...)               ; accessor for X field
(DEFUN UPDATE-X (V $S) ...)      ; updater for X field
(DEFUN AI (I $S) ...)            ; accessor for A field at index I
(DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Here is the definition of $SP: 

(DEFUN $SP ($S)
  (DECLARE (XARGS :GUARD T))
  (AND (TRUE-LISTP $S)
       (= (LENGTH $S) 2)
       (XP (NTH 0 $S))
       (AP (NTH 1 $S))))
This reveals that in order to satisfy $SP an object must be a true list of length 2 whose first element satisfies XP and whose second satisfies AP. By printing the definition of AP one learns that it requires its argument to be a list of length 3, each element of which is an integer between 0 and 9.

Here is the definition of UPDATE-AI, the updater for the A field at index I: 

(DEFUN UPDATE-AI (I V $S)
  (DECLARE (XARGS :GUARD
                  (AND (INTEGERP I)
                       (<= 0 I)
                       (< I 3)
                       (AND (INTEGERP V) (<= 0 V) (<= V 9))
                       (SP $S))))
  (UPDATE-NTH 1 (UPDATE-NTH I V (NTH 1 $S)) $S))
This may be a little surprising but should be perfectly clear.

First, ignore the guard, since it is irrelevant in the logic. Reading from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is array a of $S. (Recall that NTH is 0-based.) The next higher expression in the definition above, (UPDATE-NTH I V a), ``modifies'' a by setting its Ith element to V. Call this a'. The next higher expression, (UPDATE-NTH 1 a' $S), ``modifies'' $S by setting its 1st component to a'. Call this result $s'. Then $s' is the result returned by UPDATE-AI.

So the first useful observation is that from the perspective of the logic, the type ``restrictions'' on stobjs are irrelevant. They are ``enforced'' by ACL2's guard mechanism, not by the definitions of the updater functions.

As one might also imagine, the accessor functions do not really ``care,'' logically, whether they are applied to well-formed stobjs or not. For example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer. That is, 

(integerp (AI 2 $S))
is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level ACL2 command loop, because we insist that the current value of the stobj $S always satisfy $SP by enforcing the guards on the updaters whether guard checking is on or off (see set-guard-checking). But in a theorem $S is just another variable, implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when the variable $S is instantiated with, say, 

'(1 (0 1 TWO))
because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the symbol TWO. That is, 
(equal (AI 2 '(1 (0 1 TWO))) 'TWO)
is true.

However, 

(implies ($SP $S) (integerp (AI 2 $S)))
is a theorem. To prove it, you will have to prove a lemma about AP1. The following will do: 
(defthm ap1-nth
  (implies (and (AP1 x n)
                (integerp n)
                (integerp i)
                (<= 0 i)
                (< i n))
           (integerp (nth i x)))).

Similarly, 

(implies (and (integerp i)
              (<= 0 i)
              (< i 3)
              (integerp v)
              (<= 0 v)
              (<= v 9))
         ($SP (UPDATE-AI i v $S)))
is not a theorem until you add the additional hypothesis ($SP $S).

The moral here is that from the logical perspective, you must provide the hypotheses that, as a programmer, you think are implicit on the structure of your stobjs, and you must prove their invariance. This is a good area for further support, perhaps in the form of a library of macros.

This completes the tour through the documentation of stobjs. However, you may now wish to read the documentatin for the event that introduces a new single-threaded object, defstobj.