From 2ddd413befca353c76374ac8c6486d11986bd800 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 May 2017 14:44:17 -0700 Subject: [PATCH] fix(library/parray): reroot split optimization is incorrect when ThreadSafe == true --- src/library/parray.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/library/parray.h b/src/library/parray.h index a5be838753..a626e2a86b 100644 --- a/src/library/parray.h +++ b/src/library/parray.h @@ -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];);