Wormhole-status
the two senses of a wormhole's status
As noted in the discussion of wormholes, every wormhole has a
current status, which is some ACL2 object whose shape is largely determined
by the author of the wormhole. That object is not stored in the ACL2 state.
When the wormhole is entered, its status is assigned to the state global
variable wormhole-status, making it visible. When the wormhole is
exited, the value of wormhole-status is transferred back to its
``hidden'' location outside of the state. Thus, the next time it is entered
the wormhole-status is the same as it was when it was last exited.
We call the ``hidden'' version of a wormhole's status the persistent
wormhole status or persistent-whs and the version occasionally
found in the state global wormhole-status as the ephemeral wormhole
status or ephemeral-whs. It is helpful to think of the
persistent-whs as the wormhole's status as stored in some distant location
and its ephemeral-whs as an easily accessible, nearby cache. When the two
locations hold the same value we say the wormhole is coherent.
The state global variable wormhole-status is untouchable: you can
read it but not directly write to it via assign or f-put-global. But you can write to the persistent-whs. That is what wormhole-eval does. So while a wormhole is coherent when you first enter it
it can become incoherent if you use wormhole-eval to change its
persistent-whs while inside the wormhole. And remember, the use of
wormhole-eval can be disguised via a function definition.
The following script illustrates this. First, create a wormhole named
demo whose data field is empty. We'll use it to accumulate items
without modifying state. We define (save x) to cons x onto the
data field of the demo wormhole. So execute these five commands at
the top-level of ACL2.
(wormhole-eval 'demo '(lambda nil '(:enter . nil)) nil)
(defun save (x)
(wormhole-eval
'demo
'(lambda (whs)(set-wormhole-data whs (cons x (wormhole-data whs))))
nil))
(save 'a)
(save 'b)
(save 'c)
Then inspect the persistent-whs of demo:
ACL2 !>(get-persistent-whs 'demo state)
(:ENTER C B A)
So save works as we planned. But now let's enter the demo
wormhole. Inside the wormhole we first inspect the ephemeral-whs (i.e.,
(@ wormhole-status), and the persistent-whs to confirm the wormhole is
coherent. Then we execute (save 'd) to add D to the accumulator.
Inspecting the persistent-whs shows that it worked. But the ephemeral-whs
did not change! The wormhole is now incoherent, thanks to the ``disguised''
use of wormhole-eval while in the wormhole.
ACL2 !>(wormhole 'demo '(lambda (whs) whs) nil '(quote (welcome!)))
Project-dir-alist:
((:SYSTEM . "/Users/moore/Desktop/v85k1/books/")).
Type :help for help.
Type (quit) to quit completely out of ACL2.
Wormhole ACL2 !>(WELCOME!)
Wormhole ACL2 !>(@ wormhole-status)
(:ENTER C B A)
Wormhole ACL2 !>(get-persistent-whs 'demo state)
(:ENTER C B A)
Wormhole ACL2 !>(save 'd)
NIL
Wormhole ACL2 !>(get-persistent-whs 'demo state)
(:ENTER D C B A)
Wormhole ACL2 !>(@ wormhole-status)
(:ENTER C B A)
Wormhole ACL2 !>:q
NIL
The :q above exits the wormhole. Now re-enter the wormhole and
inspect the ephemeral-whs and persistent-whs.
ACL2 !>(wormhole 'demo '(lambda (whs) whs) nil '(quote (welcome back!)))
Project-dir-alist:
((:SYSTEM . "/Users/moore/Desktop/v85k1/books/")).
Type :help for help.
Type (quit) to quit completely out of ACL2.
Wormhole ACL2 !>(WELCOME BACK!)
Wormhole ACL2 !>(@ wormhole-status)
(:ENTER C B A)
Wormhole ACL2 !>(get-persistent-whs 'demo state)
(:ENTER C B A)
Wormhole ACL2 !>(value :q)
NIL
The wormhole is coherent of course; wormholes are always coherent upon
entry. But notice the value of the data field! It doesn't list D!
That happened because when we exited the wormhole, the ephemeral-whs was
written back to the persistent-whs, and the ephemeral-whs of the incoherent
status did not contain D.
There are ways ensure that your wormholes remain coherent and they all
involve using the function sync-ephemeral-whs-with-persistent-whs,
which does what its name says. For example, we could have defined save
this way instead.
(defun save (x state)
(prog2$
(wormhole-eval
'demo
'(lambda (whs)(set-wormhole-data whs (cons x (wormhole-data whs))))
nil)
(sync-ephemeral-whs-with-persistent-whs 'demo state)))
But note that we must now provide state as an argument to all calls
of save and save must return state because read-ACL2-oracle was used to reach out to the persistent-whs to refresh
the ephemeral-whs. This means we can only call this version of save in
environments in which we have state and can return state.
Perhaps a better way preserve coherence is to keep save defined in
the earlier, state-less way but to call
sync-ephemeral-whs-with-persistent-whs from within the wormhole after we
call (save 'd). That is easy enough to do if you are in complete
control of the demo wormhole. Recall the specification of wormhole. If the entry lambda sets the wormhole-entry-code to
:enter, then ld is invoked but the first form executed by the
resulting read-eval-print loop is the form argument of wormhole.
We used the form argument in the script above to just print a greeting
but it can be an arbitrary form. If form returns (value nil) the
ld is exited without ever giving the user the opportunity to type and
evaluate an arbitrary form.
But if the demo wormhole allows a user to type and evaluate arbitrary
forms (including forms like wormhole-eval or the state-less
save), there is no way to ensure coherency. We admit this is an
unfortunate aspect of the current design.
The simplest way to avoid such problems is to use wormhole-eval
exclusively and avoid use of the interactive read-eval-print loop provided by
wormhole, except loops intended for experts. This is the approach
taken by such system utilities as accumulated-persistence and fc-report: wormhole-eval is used to collect data and either
wormhole-eval or a non-interactive wormhole is used to display
it.
