Thread Safety

[ssoelvsten]

In many contexts, BDD packages should be threadsafe such that they can be used as part of parallel algorithms. Luckily for us, the write-once/read-only design of Adiar's files makes thread-safety much easier (since we have no unique node table to lock). Yet, instead we have one global pool of M memory in TPIE that we are allowed to use. Hence, we need some kind of locking/scheduler to make sure every thread can claim a share of M "early". Otherwise, another thread can by accident overtake it and both ask TPIE for the same "free" memory.

Time-forward Processing : Memory Management

It is not possible for such a program to know early how many threads may exist before it starts its calculations. Hence, Adiar has to adapt on-the-fly to the number of concurrent calls.

• Add ADIAR_THREADSAFE to CMake (default: OFF). If on, then the logic for thread-safety below is included.
• Add memory_share class that uses RAII to claim a share of memory.
  • Claim up-to half of the unclaimed memory.
  • Claim at least the minimum amount of memory (128 MiB, or maybe a more sophisticated number?). If not currently available, then the thread has to wait for someone else to finish their calculations.
  • If the internal-memory cases use less than is claimed, then relinquish the unused amount early. Alternatively, first claim memory after all internal-memory calculations have been made.

Unique Node Table

With #444 and its dependent issues, we add a unique node table. With #696 , we also add memoisation caches. If these are done, then we also need to make these thread-safe. Below is a description of a place to start by using some compare-and-swap loops for a lock-free design. But, designing the node table properly is an entire project in itself.

1. Claim the next free node with a CAS. If in (2.) another thread ends up inserting the same node as this thread set out to do, then the claimed node is released by placing it back into the free chain with another CAS.
2. Insert this newly claimed node in its bucket. To this end, one can maintain the bucket sorted on the child(ren) ( Alternative Insertion Orders in Linear Bucket #728 ). This makes node placement deterministic. Hence, if two threads allocate the same node, the CAS of one of them fails. The failing thread can check whether the newly inserted node is the one it tried to allocate. If so, it can give back the node it claimed. Otherwise, it can try once more to insert the node.
3. The reference counter can also be updated with a CAS-loop.

The main source of contention above is claiming (and giving back) nodes from (and to) the free chain. Can one split the free chain up between the different threads/cpu cores?

Garbage Collection

Garbage collection requires one stops all concurrent computations. To this end we probably need to use a locks or semaphores on the node table and the memoisation caches ( #696 ). But, we only need to keep track of two things:

1. Is some BDD operation currently reading from the table?
2. Does some BDD operation waiting to start GC?

So, we might only need to interact with the locks at the start/end of the BDD operation (1.) or when the free chain is empty (2.). Furthermore, since our simplified table does not move nodes around during GC, some operations such as bdd_satcount can maybe run even while the GC is ongoing!

Furthermore, since the table is thread-safe, we can use tpie::jobs to parallelise the garbage collection!

[ssoelvsten]

While talking to Riko Jacob, it can be a bad idea to just naively split the amount of memory (as described above). Iterating on his point, we should consider to:

1. Have an upper bound on the number of concurrent jobs (set by the user / CPU specification). This could quite easily be integrated into the above solution by (1) making the minimum claimed memory be M/P where P being the maximum number of concurrent jobs and/or (2) make it also track the number of concurrently active jobs (with a semaphore).
2. Schedule/Throttle the concurrent jobs (in a FIFO fashion?)

Note, the memory_share class already almost acts as a semaphore (but one you can read and where the increment/decrement is not 1 but the amount of memory you want to use).