Skip to content

Use Generational Garbage Collection for Node Table #740

Description

@ssoelvsten

As mentioned by Samuel Pastva on an issue for the ruddy BDD package, the performance of garbage collection could benefit from being generational. Intuitively, it is most likely that the newest BDD nodes will be garbage collected. Hence, we should try and focus our efforts on these.

To do so, we keep need to track of the latest k nodes that have been created in a nursery; this can be done it two ways:

  1. We add a simple additional of vector of uids into the table. This requires an additional O(k) space. It may also introduce some cache issues as (1) we jump between the vector and the nodes and (2) the nodes in the nursery might not be adjacent.
  2. We could allocate two free lists into the table: one for the nursery and one for the rest. Upon garbage collection, these are then moved from one list to another. This only requires an O(1) additional space. Yet, it requires rehashing the entire nursery during GC.

Alternative(ish)

The table in #444 is immediately initialised to occupy a whole fraction of the entire memory M (~M/4, probably). To somewhat approximate a generational garbage collection, we could also GC prior to the node table being completely full. Depending on how many nodes were freed, we then increase (exponentially?) the threshold for the next GC.

This idea can also be combined with a nursery.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions