An Algorithm for Ensuring Fairness and Liveness in Non-deterministic Systems Based on Multiparty Interactions

摘要

Strong fairness is a notion we can use to ensure that an element that is enabled infinitely often in a non―deterministic programme, will eventually be selected for execution so that it can progress. Unfortunately, "eventually" is too weak to induce the intuitive idea of liveliness and leads to anomalies that are not desirable, namely fair finiteness and conspiracies. In this paper, we focus on non―deterministic programmes based on multiparty interactions and we present a new criteria for selecting interactions called strong k―fairness that improves on other proposals in that it addresses both anomalies simultaneously, and k may be set a priori to control its goodness. We also show our notion is feasible, and present an algorithm for scheduling interactions in a strongly k―fair manner using a theoretical framework to support the multiparty interaction model. Our algorithm does not require to transform the source code to the processes that compose the system; furthermore, it can deal with both terminating and non―terminating processes.