The block allocator has data races on the union type Entry<T> that do not seem to be solvable. The question is whether these are acceptable, or whether we enforce a full mutex on every allocation. The latter is also done in the mCRL2 toolset, and at least definitely correct.
The block allocator has data races on the union type
Entry<T>that do not seem to be solvable. The question is whether these are acceptable, or whether we enforce a full mutex on every allocation. The latter is also done in the mCRL2 toolset, and at least definitely correct.