From f40e6efc11a3ccd9513ef9832ec449a608f29dd9 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 28 Mar 2018 16:21:39 +0200 Subject: [PATCH] bloemen: PPOPP'16 is buggy In PPOPP'16, the algorithm does not unlock roots. This could lead to deadlock between threads. * spot/mc/bloemen.hh: here. --- spot/mc/bloemen.hh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/spot/mc/bloemen.hh b/spot/mc/bloemen.hh index e3564441a..40b7c2dd7 100644 --- a/spot/mc/bloemen.hh +++ b/spot/mc/bloemen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2017, 2018 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -247,19 +247,22 @@ namespace spot uf_element* a_list = lock_list(a); if (a_list == nullptr) - return; + { + unlock_root(q); + return; + } uf_element* b_list = lock_list(b); if (b_list == nullptr) { unlock_list(a_list); + unlock_root(q); return; } SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK); SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK); - // Swapping uf_element* a_next = a_list->next_.load(); uf_element* b_next = b_list->next_.load(); -- GitLab