Open zapashcanon opened 2 months ago
We can probably benefit a lot from this due to the principle of locality. However, I'm also concerned that you might spend more time merging memories than simply traversing the tree. But we should definitely experiment with this!
I would like to see the numbers from #433 in Test-Comp first. It would be interesting to see the time improvement for searching for a value in the memory tree.
For the record, we will need to change the data field from being mutable to a reference (to be able to re-use our parent data and add our data on top of it when compacting), we could probably optimize the option ref
by using something similar to @chambart's nullable-array, see the discussion in #433.
However, I'm also concerned that you might spend more time merging memories than simply traversing the tree
We could change the data structure for something that can be easily merged
Here's a potential optimization.
The idea is to add a
is_half_done : bool ref
to eachSymbolic_memory.t
, initially set to false.Once the status of a task is
Now
orStop
, we set this boolean to true in its parent.Then, on every read or every write (it can also be done less often, I have to think about it), we check if our parent has
is_half_done
set to true. If this is the case, it means no one else is going to access it, so we can merge ourselves with the parent. This is done by merging the two data fields (start with the parent and add our data afterward), and then, we can throw away the parent and use our grand-parent as our new parent.The new invariant is that each node of the tree has either its two children still working either it is going to disappear soon.
cc @filipeom, I'm not sure if this is going to improve anything in practice but it would be a nice experiment I believe.