• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
          • Name-database
          • Vl-gc
            • Set-vl-gc-threshold
            • Set-vl-gc-baseline
          • Symbol-list-names
          • Ints-from
          • Nats-from
          • Make-lookup-alist
          • Redundant-mergesort
          • Longest-common-prefix
          • Vl-remove-keys
          • Vl-plural-p
          • Vl-merge-contiguous-indices
          • Sum-nats
          • Vl-edition-p
          • Vl-maybe-integer-listp
          • Fast-memberp
          • Nat-listp
          • Max-nats
          • Longest-common-prefix-list
          • Character-list-listp
          • Vl-character-list-list-values-p
          • Remove-from-alist
          • Prefix-of-eachp
          • Vl-string-keys-p
          • Vl-maybe-nat-listp
          • Vl-string-list-values-p
          • String-list-listp
          • Vl-string-values-p
          • Explode-list
          • True-list-listp
          • Symbol-list-listp
          • All-have-len
          • Pos-listp
          • Min-nats
          • Debuggable-and
          • Vl-starname
          • Remove-equal-without-guard
          • String-fix
          • Anyp
          • Vl-maybe-string-list
          • Longer-than-p
          • Fast-alist-free-each-alist-val
          • Not*
          • Free-list-of-fast-alists
          • *nls*
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Utilities

Vl-gc

Maybe trigger a garbage collection.

Signature
(vl-gc) → nil

In the logic vl-gc just returns nil. On CCL, its raw Lisp definition, it may (or may not) trigger a garbage collection. On other Lisps, it just does nothing.

Throughout VL, we call vl-gc at "good" places to do garbage collection. We typically call it right after computations that allocate a lot of "temporary" memory—memory that will be garbage once the computation has finished. A GC at this time may be cheaper than a GC later, when we just happen to run out of memory, because GC costs are basically proportional to the number of live objects.

Running vl-gc only sometimes triggers a GC. Why? We sometimes use VL to process large designs (hundreds of thousands of lines of Verilog), and sometimes use it on much smaller designs. Depending on the kind of input, we probably want to use different GC strategies:

  • When we process large designs, each transformation naturally allocates more memory. Some transforms might allocate hundreds of megabytes or gigabytes of memory. In this case, we would like to GC more frequently in order to keep our memory usage down.
  • When we deal with small designs, nothing is very expensive. We probably have ample memory to process the whole design without any garbage collection. In this case, we would like to avoid GC altogether to maximize performance.

vl-gc is meant to work well with either scenario. Basically, after triggering a GC, vl-gc records how much memory are allocated. This gives us a rough baseline of how much memory the rest of the program is using. Then, each time vl-gc is called, it compares the current memory usage to this baseline. A GC is only triggered if the new memory usage exceeds the baseline by some threshold (e.g., 1 GB).

Here's how this works under either scenario.

  • When we process a large design, our transforms are consuming memory quite quickly, so the vl-gc calls throughout our program end up causing many GCs. These GCs occur at good places (the places where we called vl-gc, and keep our memory usage down, as desired.
  • When we process a small design, our transforms don't use much memory so when we call vl-gc, we haven't exceeded the threshold. So, we don't waste our time collecting this insignificant garbage, as desired.

Definitions and Theorems

Function: vl-gc

(defun vl-gc nil (declare (xargs :guard t))
       (let ((__function__ 'vl-gc))
            (declare (ignorable __function__))
            (raise "Under-the-hood definition not installed?")))

Subtopics

Set-vl-gc-threshold
Instruct vl-gc to trigger a garbage collection when the current memory usage exceeds the baseline by some amount.
Set-vl-gc-baseline
Resets the baseline for vl-gc to however much memory is currently allocated.