		Search-engine friendly clone of the ACL2 documentation.

Defabsstobj

Set-absstobj-debug

Get more information when atomic update fails for an abstract stobj

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

Below we explain what is meant by the following error message, and how to add information to the end of it.

ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
for an abstract stobj!
**PROCEED AT YOUR OWN RISK.**
To proceed, evaluate the following form.
:CONTINUE-FROM-ILLEGAL-STATE
See :DOC set-absstobj-debug.

Advanced users who are willing to risk unsound invariance violations to get a bit more speed may submit the following when there is an active trust tag (see defttag).

(set-absstobj-debug :ignore)

The rest of the session will then avoid the error message above because it avoids the abstract stobj invariance checking discussed below. BUT WITHOUT THIS CHECKING, YOUR SESSION COULD BE CORRUPTED! The discussion below assumes that you are not using the special argument :ignore for set-absstobj-debug.

The use of (set-absstobj-debug t) will make the error message above more informative, for example as follows, at the cost of slower execution — but in practice, the slowdown may be negligible (more on that below). Below, only the last two lines are new.

ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
for an abstract stobj!
**PROCEED AT YOUR OWN RISK.**
To proceed, evaluate the following form.
:CONTINUE-FROM-ILLEGAL-STATE
See :DOC set-absstobj-debug.
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-books file books/demos/defabsstobj-example-4-input.lsp for how to do that. (The corresponding output file books/demos/defabsstobj-example-4-log.txt may also be informative.)

Examples:
(set-absstobj-debug t)                 ; obtain extra debug info, as above
(set-absstobj-debug nil)               ; avoid extra debug info (default)
(set-absstobj-debug :ignore)           ; possibly unsound! -- see above

General Form:
(set-absstobj-debug val)

where val is evaluated.

Recall (see defabsstobj) that for any exported function whose :EXEC function might (according to ACL2's heuristics) modify the foundational 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.

Calls of set-absstobj-debug are legal event forms (e.g., for books).