max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/parray): reroot split optimization is incorrect when ThreadSafe == true

Browse source
This commit is contained in:
Leonardo de Moura 2017-05-08 14:44:17 -07:00
parent 970529a8e9
commit 2ddd413bef
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/parray.h
View file

@ -319,12 +319,19 @@ class parray {
lean_assert(r->kind() != Root);
cell_buffer cs;
cell * c = collect_cells(r, cs);
if (should_split(c->size(), cs.size()) &&
if (!ThreadSafe &&
/* Should we keep this optimization? */
should_split(c->size(), cs.size()) &&
should_split(get_size(c, cs), cs.size())) {
/* Split the path r -> ... -> m_1 -> m_2 -> ... -> c in two
1) r <- ... <- m_1
2) m_2 -> ... -> c
This operation is not safe when ThreadSafe == true.
In ThreadSafe mode, each cell contains a reference to
the mutex stored in the Root cell, but we don't know
all cells that point to a Root cell.
*/
unsigned midx = cs.size() / 2;
DEBUG_CODE(cell * m = cs[midx];);