Analysis by proof and verification of an abstract algorithm for distributed irregular tree processing

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.