• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
          • Ttag-bitset-members
            • Bignum-extract
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-union
        • Bitset-memberp
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bitset-members

Ttag-bitset-members

Notes about the optimization of bitset-members.

Signature

(ttag-bitset-members x) → *

Arguments

x — Guard (natp x).

The basic version of bitset-members calls bits-between, which repeatedly indexes into the bitset using logbitp.

We found this wasn't very efficient in 64-bit CCL, and have developed an alternate implementation that uses:

1. bits-0-31, a partially unrolled version of bits-between that is specialized for 32-bit numbers, and
2. bignum-extract, a function for extracting a 32-bit chunk from a bignum in a particularly efficient way on 64-bit CCL.

Basic performance testing suggests that ttag-bitset-members is almost 5x faster than a regular version. Here's the testing code I used:

(include-book "bitsets")
(include-book "centaur/aig/random-sim" :dir :system)
(include-book "centaur/misc/memory-mgmt" :dir :system)
(include-book "std/util/defconsts" :dir :system)

 (acl2::set-max-mem ;; newline to fool dependency scanner
   (* 30 (expt 2 30)))

 (acl2::defconsts (*random-data* state)
   (acl2::random-list 100000 (ash 1 5000) state))

(defund bitset-members-list (x)
  (if (atom x)
      nil
    (cons (bitset-members (car x))
          (bitset-members-list (cdr x)))))

(defund ttag-bitset-members-list (x)
  (if (atom x)
      nil
    (cons (ttag-bitset-members (car x))
          (ttag-bitset-members-list (cdr x)))))

(progn$
 (gc$)
 (time$ (bitset-members-list *random-data*)
        :msg "Unoptimized Original: ~st sec, ~sa bytes~%")
 (gc$)
 (time$ (ttag-bitset-members-list *random-data*)
        :msg "Unoptimized TTAG: ~st sec, ~sa bytes~%")
 nil)

(include-book "bitsets-opt")

(progn$
 (gc$)
 (time$ (bitset-members-list *random-data*)
        :msg "Optimized Original: ~st sec, ~sa bytes~%")
 (gc$)
 (time$ (ttag-bitset-members-list *random-data*)
        :msg "Optimized TTAG: ~st sec, ~sa bytes~%")
 nil)

And the results (on compute-1-3):

Unoptimized Original: 12.80 sec, 4,001,843,488 bytes
Unoptimized TTAG: 8.27 sec, 9,118,511,648 bytes
Optimized Original: 4.05 sec, 4,001,843,488 bytes
Optimized TTAG: 4.01 sec, 4,001,843,488 bytes

Definitions and Theorems

Function: ttag-bitset-members-aux

(defun ttag-bitset-members-aux (slice x acc)
  (declare (xargs :guard (and (natp slice) (integerp x))))
  (if (zp slice)
      (bits-0-31 (ash slice 5)
                 (bignum-extract x slice)
                 acc)
    (ttag-bitset-members-aux
         (the (integer 0 *) (- (lnfix slice) 1))
         x
         (bits-0-31 (the (integer 0 *) (ash slice 5))
                    (bignum-extract x slice)
                    acc))))

Theorem: ttag-bitset-members-aux-redef

(defthm ttag-bitset-members-aux-redef
  (implies (and (natp slice) (integerp x))
           (equal (ttag-bitset-members-aux slice x acc)
                  (append (bits-between 0 (* (+ 1 slice) 32) x)
                          acc))))

Function: ttag-bitset-members

(defun ttag-bitset-members (x)
 (declare (xargs :guard (natp x)))
 (let ((__function__ 'ttag-bitset-members))
  (declare (ignorable __function__))
  (mbe
    :logic (bitset-members x)
    :exec (ttag-bitset-members-aux (the (integer 0 *)
                                        (ash (integer-length x) -5))
                                   x nil))))

Subtopics

Bignum-extract

Extract a particular 32-bit slice of an integer.