Abstract:
In the domain of irregular tree processing, two level
load-balancing strategies are most commonly used. Static load
balancing is performed initially based on task estimates while
dynamic load balancing is performed during run-time to deal
with skewed load conditions. A particular variant of this strategy
based on a master-worker architecture has been implemented for
concept mining in the area of Formal Concept Analysis, [1]. It has
been equipped with an additional component for fault tolerance
in [2]. In this paper we propose an abstract algorithm for irregular
tree processing generalising the strategy used in [1] for concept
mining. We prove deadlock-freedom and termination correctness.
We investigate this algorithm further by creating PROMELA
models of increasing level of abstraction to be able to analyse
it with the SPIN model checker. For the most abstract and
compact model we verify that there is no loss or addition of work,
deadlock-freedom, termination, and the ability of workers to act
as stealers and as donors in the same run. Finally, this model is
extended by the features to adjust to fail-stop errors of workers
guided by the implementation of [2]. While the earlier properties
remain valid (modified wrt. failure of workers), adjustment to a
loss of workers is also verified.
