Operate on a global single-threaded object
See stobj for an introduction to single-threaded objects. Also see defstobj for additional background.
The
Example Forms: ; Read-only form (length 3) (with-global-stobj st ;; body: (fld st)) ; Updating form (length 4; (returns state)) (with-global-stobj st ; bound stobj (st) ; output signature of body ;; body: (update-fld x st)) ; Updating form (length 4; returns (mv * * state st2)) (with-global-stobj st ; bound stobj (nil st nil state st2) ; output signature of body ;; body: (let* ((st (update-fld x st)) (st2 (update-fld2 x st2))) (mv (fld st) st (fld st2) state st2)))
In the forms above, we call
ACL2 !>:trans1 (with-global-stobj st (fld st)) (LET ((ST (READ-USER-STOBJ-ALIST 'ST STATE))) (FLD ST)) ACL2 !>:trans1 (with-global-stobj st (st) (update-fld x st)) (LET ((ST (READ-USER-STOBJ-ALIST 'ST STATE))) (LET ((ST (UPDATE-FLD X ST))) (WRITE-USER-STOBJ-ALIST 'ST ST STATE))) ACL2 !>:trans1 (with-global-stobj st (nil st nil state st2) (let* ((st (update-fld x st)) (st2 (update-fld2 x st2))) (mv (fld st) st (fld st2) state st2))) (LET ((ST (READ-USER-STOBJ-ALIST 'ST STATE))) (MV-LET ({WGS}0 ST {WGS}1 STATE ST2) (LET* ((ST (UPDATE-FLD X ST)) (ST2 (UPDATE-FLD2 X ST2))) (MV (FLD ST) ST (FLD ST2) STATE ST2)) (LET ((STATE (WRITE-USER-STOBJ-ALIST 'ST ST STATE))) (MV? {WGS}0 {WGS}1 STATE ST2)))) ACL2 !>
The first illustrates that in the read-only form, the bound stobj, which is
Note that ACL2 expects you to use
(defun-nx read-user-stobj-alist (st state) (declare (xargs :guard (symbolp st) :stobjs state)) (cdr (assoc-eq st (user-stobj-alist1 state)))) (defun-nx write-user-stobj-alist (st val state) (declare (xargs :guard (symbolp st) :stobjs state)) (update-user-stobj-alist1 (put-assoc-eq st val (user-stobj-alist1 state)) state))
This topic is intended to be sufficient preparation for the use of
As noted above, examples may be found in community-book file
Let us start by introducing a couple of stobjs.
(defstobj st fld) (defstobj st2 fld2 :congruent-to st)
Calls of
(with-global-stobj st (fld st))
One solution may be to use top-level.
(top-level (with-global-stobj st (fld st)))
Normally, however,
(defun rd0 (state) (declare (xargs :stobjs state)) (with-global-stobj st (fld st))) (defun wr0 (x state) (declare (xargs :stobjs state)) (with-global-stobj st (st) (update-fld x st)))
Let's see these in action, first writing and then reading.
ACL2 !>(wr0 2 state) <state> ACL2 !>(rd0 state) 2 ACL2 !>(fld st) 2 ACL2 !>
We can use various stobj operations, even the rather fancy swap-stobjs, in the body of a
(update-fld 1 st) (update-fld 2 st2) (defun f3 (st2 state) (declare (xargs :stobjs (st2 state))) (with-global-stobj st (st2 st) (swap-stobjs st2 st))) (f3 st2 state) (assert-event (and (equal (fld st) 2) (equal (fld st2) 1)))
The following function writes to both
(defun write-global-st-st2 (fld fld2 state) (declare (xargs :stobjs state)) (with-global-stobj st (st state) (let ((st (update-fld fld st))) (with-global-stobj st2 (st st2) (let ((st2 (update-fld fld2 st2))) (mv st st2))))))
Let's check that this works as expected.
ACL2 !>(write-global-st-st2 'a 'b state) <state> ACL2 !>(fld st) A ACL2 !>(fld st2) B ACL2 !>
We can also read both fields.
(defun read-global-st-st2 (state) (declare (xargs :stobjs state)) (with-global-stobj st (with-global-stobj st2 (list (fld st) (fld st2)))))
Then, continuing with the session above:
ACL2 !>(read-global-st-st2 state) (A B) ACL2 !>
We can reason about
(defthm rd0-of-wr0 (equal (rd0 (wr0 val state)) val))
This fails to prove, but each of the two checkpoints has a term of the form
(defthm assoc-equal-put-assoc-equal (equal (assoc-equal key (put-assoc-equal key val alist)) (cons key val)))
This lemma proves automatically, after which
This section provides a reference for
General Forms: ; Read-only form (length 3): (with-global-stobj st form) ; Updating form (length 4): (with-global-stobj st lst form)
where
In each General Form above,
For the read-only form, the bound stobj (which is
For the updating form, the values actually returned are obtained by
removing
(defun f0 (st2 state) (declare (xargs :stobjs (st2 state))) (with-global-stobj st (st st2 nil state) (mv st st2 nil state)))
In this case,
ACL2 !>:trans1 (with-global-stobj st (st st2 nil state) (mv st st2 nil state)) (LET ((ST (READ-USER-STOBJ-ALIST 'ST STATE))) (MV-LET (ST ST2 {WGS}0 STATE) (MV ST ST2 NIL STATE) (LET ((STATE (WRITE-USER-STOBJ-ALIST 'ST ST STATE))) (MV? ST2 {WGS}0 STATE)))) ACL2 !>
Evaluation of an updating
ACL2 !>:trans1 (with-global-stobj st (st st2 nil) (mv st st2 nil)) (LET ((ST (READ-USER-STOBJ-ALIST 'ST STATE))) (MV-LET (ST ST2 {WGS}0) (MV ST ST2 NIL) (LET ((STATE (WRITE-USER-STOBJ-ALIST 'ST ST STATE))) (MV? ST2 {WGS}0 STATE)))) ACL2 !>
Note that because
For the examples in this section, we continue to assume that the following defstobj events have been evaluated.
(defstobj st fld) (defstobj st2 fld2 :congruent-to st)
Consider the following definition.
(defun foo (st state) (declare (xargs :stobjs (st state))) (let ((state (with-global-stobj st (st) (update-fld 3 st)))) (mv (fld st) state)))
ACL2 admits that form, but causes an error with the following call of
ACL2 !>(foo st state) ACL2 Error in TOP-LEVEL: Illegal top-level form, (FOO ST STATE). The stobj ST occurs free, yet may be bound by an updating WITH-GLOBAL- STOBJ form, as the top-level form calls FOO, which makes an updating WITH-GLOBAL-STOBJ call that binds ST. See :DOC with-global-stobj. ACL2 !>
Let us see why this call must be illegal; then we'll study the error
message. The
(thm (implies (stp st) (equal (mv-nth 0 (foo st state)) (fld st))))
What we are seeing is a violation of single-threadedness.
Now let's look at the error message above. It explains that ``the stobj ST
occurs free'' in
By contrast, there is no such problem if we replace
ACL2 !>(foo st2 state) (NIL <state>) ACL2 !>(fld st2) NIL ACL2 !>(fld st) 3 ACL2 !>
In this case there is no aliasing problem. The formal parameter
Note that the aliasing problem can be buried through a chain of function
calls, as we now illustrate. Function
(defun foo2-sub (val state) (declare (xargs :stobjs state)) (with-global-stobj st (st) (update-fld val st))) (defun foo2 (val st state) (declare (xargs :stobjs (st state))) (let ((state (foo2-sub val state))) (mv (fld st) state val)))
The error message is essentially the same, except that the chain of calls
is shown that leads to the problematic updating
ACL2 !>(foo2 3 st state) ACL2 Error in TOP-LEVEL: Illegal top-level form, (FOO2 3 ST STATE). The stobj ST occurs free, yet may be bound by an updating WITH-GLOBAL- STOBJ form, as the top-level form calls FOO2, which calls FOO2-SUB, which makes an updating WITH-GLOBAL-STOBJ call that binds ST. See :DOC with-global-stobj. ACL2 !>(foo2 4 st2 state) (NIL <state> 4) ACL2 !>(fld st2) NIL ACL2 !>(fld st) 4 ACL2 !>
So far we have seen just one aliasing problem, i.e., between a free stobj
in a top-level form and a subsidiary updating
(defun g2 (val st state) (declare (xargs :stobjs (st state))) (let ((st (update-fld val st))) (let ((f (with-global-stobj st (fld st)))) (mv f (fld st) st state)))) (g2 nil st state)
As before, the definition is fine, but the ensuing top-level call is not.
And as before, if we replace the top-level stobj occurrence by one that is
congruent to
Note that there is no aliasing problem when there is no update of the
stobj, either in the top-level form or in the subsidiary
(defun g1 (st state) (declare (xargs :stobjs (st state))) (let ((f (with-global-stobj st (fld st)))) (mv f state (fld st)))) (g1 st state)
So far we have seen two similar error cases due to aliasing: both are
top-level calls involving a stobj occurrence that has an occurrence below
bound by
Our restrictions that prevent aliasing are syntactic ones, sufficient to
prevent the invocations described above. They are implemented by searching
for calls of
Finally, we note that the syntactic restrictions extend to guards.
Consider again the function
(defun rd0 (state) (declare (xargs :stobjs state)) (with-global-stobj st (fld st))) (defun call-rd0-in-guard (state) (declare (xargs :stobjs state :guard (rd0 state)) (ignore state)) 17)
Then as before, it is an error for a top-level form to update
ACL2 !>(let ((st (update-fld 3 st))) (mv st (call-rd0-in-guard state))) ACL2 Error in TOP-LEVEL: Illegal top-level form, (LET ((ST (UPDATE-FLD 3 ST))) (LIST ST (CALL-RD0-IN-GUARD STATE))). The stobj ST is returned by evaluation of that form, yet is bound by a WITH-GLOBAL-STOBJ form, as the top-level form calls CALL-RD0-IN-GUARD, which calls RD0, which makes a WITH-GLOBAL-STOBJ call that binds ST. See :DOC with-global-stobj. ACL2 !>
Consider the following constrained function introduction.
(encapsulate (((crn0 state) => *)) (local (defun crn0 (state) (declare (xargs :stobjs state)) (state-p state))))
If we try to attach
ACL2 !>(defattach crn0 rd0) ACL2 Error in ( DEFATTACH CRN0 RD0): The attachment of RD0 to CRN0 restricts stobjs bound by WITH-GLOBAL-STOBJ under calls of RD0, according to the :GLOBAL-STOBJS keyword (default nil) in the signature introducing CRN0. But this restriction is violated for stobj ST: the attempt is to attach RD0, which makes a WITH-GLOBAL-STOBJ call that binds ST, yet that stobj is not specified by the :GLOBAL-STOBJS keyword of CRN0. See :DOC with-global-stobj. Summary Form: ( DEFATTACH CRN0 RD0) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error [Failure] in ( DEFATTACH CRN0 RD0): See :DOC failure. ******** FAILED ******** ACL2 !>
The solution is to note, in the signature of the constrained function, that
it may lead to a
(encapsulate (((crn1 state) => * :global-stobjs ((st) . nil))) (local (defun crn1 (state) (declare (xargs :stobjs state)) (state-p state))))
Then the form
The requirement is thus as follows. Consider attachment of