alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

bloemen: PPOPP'16 is buggy

Browse source 
In PPOPP'16, the algorithm does not unlock
roots. This could lead to deadlock between
threads.

* spot/mc/bloemen.hh: here.
This commit is contained in:
Etienne Renault 2018-03-28 16:21:39 +02:00
parent 9827b1d096
commit ae101a509f
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
spot/mc/bloemen.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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 // Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -247,19 +247,22 @@ namespace spot
uf_element* a_list = lock_list(a); uf_element* a_list = lock_list(a);
if (a_list == nullptr) if (a_list == nullptr)
return; {
unlock_root(q);
return;
}
uf_element* b_list = lock_list(b); uf_element* b_list = lock_list(b);
if (b_list == nullptr) if (b_list == nullptr)
{ {
unlock_list(a_list); unlock_list(a_list);
unlock_root(q);
return; return;
} }
SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK); SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK); SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
// Swapping // Swapping
uf_element* a_next = a_list->next_.load(); uf_element* a_next = a_list->next_.load();
uf_element* b_next = b_list->next_.load(); uf_element* b_next = b_list->next_.load();