https://gcc.gnu.org/bugzilla/show_bug.cgi?id=30920
Anton Lorenzen <anton.lorenzen at ed dot ac.uk> changed:
What |Removed |Added
----------------------------------------------------------------------------
CC| |anton.lorenzen at ed dot ac.uk
--- Comment #3 from Anton Lorenzen <anton.lorenzen at ed dot ac.uk> ---
Bumping this bug since it still applies: The splay tree implementations in
`typed-splay-tree.h` as well as `libiberty/splay-tree.c` and
`libgomp/splay-tree.c` do not implement the original algorithm of Sleater and
Tarjan. In contrast, the implementations in `splay-tree-utils.tcc` and
`bitmap.cc` seem to be correct.
It is unclear what (amortized) efficiency bounds apply to the incorrect
implementations. However, it seems likely that they should perform worse than
the textbook algorithm and they are mentioned in
https://gcc.gnu.org/wiki/Speedup_areas (although this could also be due the use
of function pointers for comparison, which in particular makes integer keys
much slower than necessary). While Ian Blanes comments earlier in this thread
that the previous implementation was even slower due to its recursive nature,
the correct implementations mentioned above are not recursive and should show
improved performance over the incorrect ones.
We re-discovered this bug after Gabriel Scherer pointed us to a Master Thesis
attempting to prove the former implementations above correct ("Formal
Verification of Pointer-Based Splay Trees in Iris"). It is unclear whether the
author of this thesis was aware that these implementations do not implement the
textbook algorithm. In contrast, we could prove the textbook implementation
correct
(https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf,
accepted at PLDI'24). I would be happy to contribute a patch replacing the
incorrect implementation by a correct one if there is demand for that.
