Commit f40e6efc authored by Etienne Renault's avatar Etienne Renault

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.
parent acff9698
// -*- 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();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment