store seen set count in a single global that does not get reallocated
Previously we were storing the seen set count (the number of states actually in
the seen set) in a struct member accessed via local_seen->count. This had a few
downsides:
1. Every time the seen set was expanded, the location of this count was moved
to the newly allocated struct and the value had to be copied over.
Determining when was a safe point to perform this copy was a fine art that
was perhaps not immediately obvious from the code.
2. Storing the count in the set struct made the struct one word larger than it
needed to be.
3. Referencing the count through local_seen->count meant we were always taking
a performance hit of a thread-local reference unless the compiler was
clever enough to see through this access (unlikely).
The motivation for storing the count in this struct to begin with was a thought
that the count could be lazy and lag behind the precise, global count. However
this doesn't work easily when we need to make expansion decisions based on
occupancy.
This change should decrease memory usage (probably not noticeable) and decrease
runtime (probably noticeable on large models).
parent
02d2803e
Please register or sign in to comment