Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add example usage of change-.... to fty::deftagsum documentation #446

Closed
ragerdl opened this issue Jul 9, 2015 · 0 comments
Closed

Add example usage of change-.... to fty::deftagsum documentation #446

ragerdl opened this issue Jul 9, 2015 · 0 comments

Comments

@ragerdl
Copy link
Member

ragerdl commented Jul 9, 2015

The usage of the change-... macros is pretty-straightforward, but adding it to the documentation would be nice.

MattKaufmann pushed a commit that referenced this issue Jun 10, 2023
…ard simplification.

Quoting :DOC note-8-6:

  (CCL only) [Stobj] array code now has a workaround for a CCL bug
  found by Yahya Sohail, in the case of reading a stobj array of
  integers where the element type includes at least one negative
  number and one non-fixnum.  This fix may slow down such stobj array
  reads a bit in CCL, in such cases; one measurement showed about 37%
  more time for such a read.  Thanks to Yahya for the bug report and
  to Warren Hunt for encouraging a workaround.

Thanks to Alessandro Coglio and Eric Smith for a discussion leading to
improvements in :DOC xargs and :DOC guard-simplification, regarding
simplification of guard proof obligations and legal values for
controlling that in various utilities.

The rest of this message is about the CCL bug workaround.

The CCL bug page is Clozure/ccl#446.

A pair of regression runs on the same machine, one without the fix and
one with the fix, showed no significant slowdown:

;;; without fix
156021.842u 3586.534s 5:53:12.65 753.1% 0+0k 2980480+9345808io 199pf+0w

;;; with fix
156317.165u 3357.513s 5:52:27.84 755.0% 0+0k 2284760+9073896io 4pf+0w

However there could be some slowdown with heavy use of stobj reads in
the case shown above.  (Maybe not; even if they slow down 37%, how
much of a computation is typically from such reads?)

Here is the example from Yahya Sohail.

(defstobj test-stobj
  (arr-field :type (array (signed-byte 64) (10))
             :initially 0))
(update-arr-fieldi 0 #x-7FFFFFFE47AFEF96 test-stobj)
(arr-fieldi 0 test-stobj)

Before the fix, the last form evaluates to the odd result of 537.
After the fix the result is as expected (the value that was just
written at index 0).

This CCL bug was apparently introduced sometime between 2015 and 2017.
A CCL developer has commented on it.  I expect to remove this special
code not long after it's fixed (which I hope is soon).
MattKaufmann pushed a commit that referenced this issue Jun 13, 2023
…hat have the fix for that bug.

If you use a git version of CCL with that bug fix (commit 6b1f1d3a30
or later; it's dated "Mon Jun 12 16:10:42 2023 -0400"), then ACL2 will
avoid working around that bug and you'll get the original, unimpeded
performance for stobj array reads.  For older CCL versions with the
bug, the workaround will continue to take effect.  Quoting a revised
version of the relevant release note that was recently added:

  (CCL only) [Stobj] array code now has a workaround for a {CCL bug |
  Clozure/ccl#446} found by Yahya Sohail,
  in the case of reading a stobj array of integers where the element
  type includes at least one negative number and one non-fixnum.
  That bug has been around since at least as far back as 2017, and
  was fixed on June 12, 2023.  For those using a CCL version with the
  bug, this fix may slow down such stobj array reads a bit in the
  case described above; one measurement showed about 37% more time
  for such a read.  Thanks to Yahya for the bug report, to Warren
  Hunt for encouraging a workaround, and to the CCL developers (in
  particular Gary Palter) for fixing the CCL bug.

Note: I successfully ran the usual fresh "make regression-everything"
twice: once using an older CCL with CCL bug #446, and once using the
latest CCL iwth the fix for that bug.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant