Topological Self-Stabilization with Name-Passing Process Calculi

TL;DR

This paper models a topological self-stabilization algorithm using an extended pi-calculus, proving its convergence properties and discussing the challenges in formal verification of such distributed systems.

Contribution

It introduces a formal pi-calculus-based model for a self-stabilizing overlay network algorithm and provides rigorous proofs of its convergence properties.

Findings

Proved closure and weak convergence for all initial configurations.

Established strong convergence in specific cases.

Discussed challenges and approaches for formal proof of convergence.

Abstract

Topological self-stabilization describes the ability of a distributed system to let the nodes themselves establish a meaningful overlay network. Independent from the initial network topology, the system converges to the desired topology via forwarding, inserting, and deleting links to neighboring nodes. Name-passing process calculi, like the pi-calculus, are a well-known and widely used method to model concurrent and distributed algorithms. The pi-calculus is designed to naturally express processes with a changing link infrastructure, as the communication between processes may carry information that can be used for a change in the linkage between the processes. We redesign a simple local linearization algorithm with asynchronous message-passing that was originally designed for a shared memory model. We use an extended localized pi-calculus, a variant of the pi-calculus, to model the algorithm. Subsequently, we formally prove the self-stabilizing properties closure, weak convergence for every arbitrary initial configuration, and strong convergence for two special cases. In our proofs we utilize rather an assertional reasoning than an action-based style. Furthermore, we describe the challenges in proving (strong) convergence in the general case. Additionally, we give strong arguments for strong convergence, supported by further proven lemmata, and discuss different approaches for a formal proof.