SET-ABSSTOBJ-DEBUG

obtain debugging information upon atomicity violation for an abstract stobj 
Major Section:  SWITCHES-PARAMETERS-AND-MODES

This documentation topic assumes familiarity with abstract stobjs. See defabsstobj.

Below we explain what is meant by an error message such as the following.

ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
for an abstract stobj!  See :DOC set-absstobj-debug, and PROCEED AT
YOUR OWN RISK.

The use of (set-absstobj-debug t) will make this error message more informative, as follows, at the cost of slower execution -- but in practice, the slowdown may be negligible (more on that below).

ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
for an abstract stobj!  See :DOC set-absstobj-debug, and PROCEED AT
YOUR OWN RISK.  Evaluation was aborted under a call of abstract stobj
export UPDATE-FLD-NIL-BAD.

You may be best off starting a new ACL2 session if you see one of the errors above. But you can continue at your own risk. With a trust tag (see defttag), you can even fool ACL2 into thinking nothing is wrong, and perhaps you can fix up the abstract stobj so that indeed, nothing really is wrong. See the community book books/misc/defabsstobj-example-4.lisp for how to do that. That book also documents the :always keyword and a special value for the first argument, :RESET.

Examples:
(set-absstobj-debug t)                 ; obtain extra debug info, as above
(set-absstobj-debug t :event-p t)      ; same as above
(set-absstobj-debug t
                    :on-skip-proofs t) ; as above, but even in include-book
(set-absstobj-debug t :event-p nil)    ; returns one value, not error triple
(set-absstobj-debug nil)               ; avoid extra debug info (default)

General Form:
(set-absstobj-debug val
                    :event-p        event-p        ; default t
                    :always         always         ; default nil
                    :on-skip-proofs on-skip-proofs ; default nil
                    )
where the keyword arguments are optional with defaults as indicated above, and all supplied arguments are evaluated except for on-skip-proofsp, which must be Boolean (if supplied). Keyword arguments are discussed at the end of this topic.

Recall (see defabsstobj) that for any exported function whose :EXEC function might (according to ACL2's heuristics) modify the concrete stobj non-atomically, one must specify :PROTECT t. This results in extra code generated for the exported function, which provides a check that atomicity was not actually violated by a call of the exported function. The extra code might slow down execution, but perhaps only negligibly in typical cases. If you can tolerate a bit extra slow-down, then evaluate the form (set-absstobj-debug t). Subsequent such errors will provide additional information, as in the example displayed earlier in this documentation topic.

Finally we document the keyword arguments, other than :ALWAYS, which is discussed in a book as mentioned above. When the value of :EVENT-P is true, which it is by default, the call of set-absstobj-debug will expand to an event. That event is a call of value-triple. In that case, :ON-SKIP-PROOFS is passed to that call so that set-absstobj-debug has an effect even when proofs are being skipped, as during include-book. That behavior is the default; that is, :ON-SKIP-PROOFS is nil by default. Also see value-triple. The value of keyword :ON-SKIP-PROOFS must always be either t or nil, but other than that, it is ignored when EVENT-P is nil.