You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The idea is to add a is_half_done : bool ref to each Symbolic_memory.t, initially set to false.
Once the status of a task is Now or Stop, 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.
The text was updated successfully, but these errors were encountered:
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.
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.
The text was updated successfully, but these errors were encountered: