extfieldsofstudy:
Computer Science
Mathematics

text:
Topological Self-Stabilization with Name-Passing Process Calculi

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.

Introduction
Undeniably, technology plays an increasing role in our society and everyday life. As hardware and software systems grow in scale and functionality, so does their complexity. An ever increasing complexity comes with an increasing likelihood of errors (Clarke and Wing, 1996). While most of the occurring errors are merely an annoyance, they can also lead to high financial losses (Mars Climate Orbiter Mishap Investigation Board et al., 1999) and in the worst case even to deaths (Leveson and Turner, 1993).
In almost no distributed system all components work correctly the entire time. Therefore fault tolerance is one of the main issues in distributed computing. One interesting and powerful specialization of nonmasking fault tolerance is self-stabilization (Gärtner, 1999). The approach of self-stabilizing systems was first introduced by Dijkstra (1974). According to Dolev (2000), the idea of a self-stabilizing system is that when started in an arbitrary state it always converges to a desired state. Therefore, a self-stabilizing system is able to automatically recover from any transient fault, like process crash with recovery and corrupted random access memory (RAM).
Topological self-stabilization describes a special subclass of self-stabilizing systems. The goal of topological self-stabilization is that the nodes themselves can establish a meaningful overlay network, independent from the initial network topology, via forwarding, inserting, and deleting links to neighboring nodes. Gall et al. (2014) introduce two variants of a self-stabilizing algorithm for graph linearization. The purpose of linearization is to build an ordered list of nodes according to their unique identifiers (ids). Therefore, whenever a node has two neighbors, both of which have a smaller (respectively a greater) id, it establishes a link between them and deletes its link to the smaller (resp. greater) one. The algorithm works only in a shared memory model as nodes access the variables of all neighbored nodes. However, the motivation for topological self-stabilization is to build robust open distributed systems, like peer-to-peer systems. Therefore, a shared memory model is not the most suitable one.
The goal of this master thesis is to redesign and model the algorithm for an asynchronous message-passing system rather than a shared memory model.
Faults can not only occur in the system itself, but also the design of algorithms. Furthermore, proofs for correctness can be faulty as well. In order to prevent a faulty design of an algorithm and to confirm the correctness of proofs the usage of formal methods is imperative.
The π-calculus is a well-known and widely used process calculus to model concurrent and distributed systems. According to Milner et al. (1992) it is designed to naturally express processes with a changing link infrastructure, as the communication between processes may carry information that lead to a change in the linkage of processes.
We model the algorithm of Gall et al. (2014) in a self-developed extension of the localized π-calculus, a variant of the π-calculus. We extended the calculus in a way similar to Wagner and Nestmann (2014). This allows us to explicitly keep track of the neighbors of each node and therefore of the topology of the system. Each node can receive messages from other nodes via a channel with the same name as its id. To enable a neighboring node to communicate with another neighbor it is sufficient to send it the corresponding id.
In order to assert the correctness of our algorithm we formally prove the self-stabilizing properties closure and weak convergence, utilizing rather assertional reasoning than an action-based style. Furthermore, we give strong arguments for strong convergence.
This thesis is organized as follows. We first introduce technical preliminaries for the better understanding of this work. This includes a short introduction of distributed algorithms and criteria for the differentiation between distributed systems. Afterwards, we describe the different forms of fault tolerance and introduce self-stabilization as a special case of nonmasking fault tolerance. We present the self-stabilizing properties closure and convergence, as well as a weaker variant. We then describe the special subclass of topological self-stabilization and the linearization problem. Subsequently, we introduce process calculi as a formalism for the description and analysis of properties in concurrent systems and the localized π-calculus as representative.
In Chapter 2, we first briefly describe the original shared memory model and the linearization algorithm of Gall et al. (2014) with the main proof ideas. Thereafter, we introduce an extended version of the localized π-calculus as basis for an asynchronous message-passing model. We then present our model with basic properties and the redesigned linearization algorithm.
Chapter 3 comprises the formal proofs of closure, strong convergence for two special cases, and weak convergence for arbitrary initial configurations together with all needed lemmata.
Chapter 4 describes the problems for a formal strong convergence proof in the general case. Nevertheless, we give strong arguments for strong convergence for every arbitrary initial configuration and introduce further proven and open lemmata with proof sketches that support this arguments and a formal proof. As a last point, we discuss several approaches for a formal proof of strong convergence.
Subsequently, we conclude with our contributions, a short comparison between the original algorithm and our redesigned one, and a summary of the obtained key findings. Additionally, we give a short overview of the related and the future work.

Technical Preliminaries
This chapter introduces important fundamentals required for a good understanding of this work. Therefore it serves the classification of the problem and the introduction of principles, concepts and notions.

Distributed Algorithms
In modern computer-based data processing a program is often executed by many different processes. In this context a process can refer to a computer as well as a processor or even a single thread that is executed on a processor (Guerraoui and Rodrigues, 2006). The fundamental problem in developing such a distributed program is that the different processes typically have to work together to solve a shared task.
Distributed algorithms are algorithms, that are designed to be executed on hardware consisting of several such connected processing units (Lynch, 1996). A distributed algorithm is therefore composed of different fragments that are executed concurrently and independent from each other, whereby each of this fragments only has access to limited information of the overall system.
The development of multiprocessor systems and multi-core processors as well as the emergence of global computer networks further increase the omnipresence of distributed algorithms.

Models of Distributed Algorithms
A large variety of concurrent algorithms for a wide range of applications is denoted as distributed algorithms. Originally, the term was only used for processes that are distributed over a large geographical area. Over time the usage of this term broadened, due to many similarities in various settings. Nowadays, it covers also algorithms executed within a local area network or even on a multiprocessor system with shared memory (Lynch, 1996).
Naturally, distributed algorithms differ in the task to be solved by the processes i. e., the problem. The diversity of distributed systems leads to a variety of algorithms solving the same problem.
To evaluate if a distributed algorithm solves a certain problem, it is necessary to possess knowledge about the system in which the algorithm is executed. Therefore hereafter we will present some common classifications for distributed systems and thus distributed algorithms (Guerraoui and Rodrigues, 2006;Lynch, 1996; Attiya and Welch, 2004).

Timing Model
One of the most important assumptions about a distributed system is the degree of synchronicity between its processes. Lynch (1996) and others distinguish between synchronous, asynchronous, and partially synchronous systems.
• Synchronous timing model: In the synchronous timing model it is assumed that all processes participating in the algorithm take steps simultaneously. This degree of synchronicity is hard to achieve with real world systems. Therefore, it is not considered a realistic assumption for many distributed systems. The advantage of this timing model is that problems can be solved with comparatively simple algorithms. This helps in development and understanding of solutions in more realistic models.
• Asynchronous timing model: In contrast in the asynchronous timing model we make no assumptions about the speed of the different processes. Every process executes the steps of the algorithm in its own tempo that may also vary over time. Therefore, the order of steps between process is not determined in general. Since no timing guarantees are given in this model, asynchronous algorithms are applicable to systems with arbitrary timing guarantees. However, in a completely asynchronous model not all problems are solvable at all.
• Partially synchronous timing model: The timing assumptions in the partially synchronous model are somewhere in the wide range between the synchronous and asynchronous model. In this model, for example, there could be lower or upper bounds on the speed of executing steps or delivering messages. The partially synchronous timing model is the most realistic. However, the correctness of the algorithm is heavily dependent on the observance of the timing assumptions.

Communication Model
Distributed algorithms require an interprocess communication mechanism due to the fact that always multiple processes are involved. Such a mechanism provides the essential possibility for information exchange between processes.

Models of Distributed Algorithms
A common abstraction of this interprocess communication is message passing, either via point-to-point or broadcast connections, shared memory, or remote procedure calls (Lynch, 1996).
• Point-to-Point Communication: For point-to-point communication it is assumed that two processes are connected via some kind of communication channel. In this model, the topology of connections, assumptions of the transmission time, and the reliability of the channels are of particular interest. The topology of the networks describes which process is able to communicate directly with whom. It can be represented as a directed graph, whereby processes are depicted as nodes and point-to-point-connections as edges. An edge (u, v) denotes that a process u can directly send a message to another process v (Lynch, 1996). In this model it is often assumed that between each pair of processes exists a bidirectional channel i. e., every process can send messages to every other process (Guerraoui and Rodrigues, 2006). In synchronous message passing, a message is sent and received simultaneously. Therefore, the transmission of the message is instantaneous as sender and receiver have to execute their corresponding steps at the same time. In contrast, during asynchronous message passing, the message transmission can take an arbitrary amount of time and the sender continues with the algorithm directly after sending the message. The reliability concerns the kinds of faults that can occur during the message transmission. This will be considered in more detail in Section 1. 2. 3.
• Broadcast-Communication: Broadcast communication is a special variant of message passing. Here it is assumed, that it is possible for a process to send a message to all other processes simultaneously. Just as in in point-to-point communication it can be distinguished between synchronous and asynchronous transmission and there are several degrees of reliability (Attiya and Welch, 2004).
• Shared Memory: In this model, processes communicate via so-called registers inside a shared memory. Processes have access through read and write operations to a shared memory cell. If a process writes a value in a specific register, it is possible for another process to directly read this value later. This kind of abstraction is suitable for physical shared memory of processes within a multiprocessor system, as well as for virtual shared memory where processes are geographically distributed and do not have actually access to the same hardware (Guerraoui and Rodrigues, 2006). Different variants of shared memory can also be distinguished by the number of processes that are allowed to access registers via read or write operations simultaneously.
• Remote Procedure Call: In this model, message exchange between processes is hidden. One process is able to make another process to execute a certain procedure. Parameters and return values of these procedures allow for an exchange of further information between the involved processes (Tanenbaum and van Steen, 2008).

Models of Faults
Hardly any (non-trivial) system can be considered fault free and components in real-life distributed systems i. e., processes and interprocess communication infrastructure, are often error-prone. Since distributed systems are widely used to assure fault tolerance, it is necessary to take faults into account and to make assumptions about the possible kinds of faults.
In the following, we give a brief overview about various fault models regarding processes and message transmission.
• Process faults: A process is seen as faulty if its behavior does not (any longer) correspond to its specification. Guerraoui and Rodrigues (2006) introduce for example four different models of process faults. Easiest to treat is the fault assumption that processes can crash i. e., a process fails and afterwards no further actions are exercised. However, until the moment of the fault it behaves according to its specification. This kind of fault is denoted as crash fault or fail-stop. Omission faults describe that a process fails to execute some actions like sending or receiving a messages. Another variant are crash-recovery faults. A crashed process recovers eventually and participates once again in the execution of the algorithm. However, this often goes hand in hand with partial or total loss of information. The most severe form of process faults are called Byzantine faults. In this model, faulty processes can execute arbitrary actions. Even actions outside of their specification.A process could, for example, send a wrong value to another process. This fault model covers also malicious behavior, since the arbitrary behavior is able to model even an outside attacker on the system.
• Transmission faults: Possible faults that can occur during the transmission of messages are loss (a message is send, but not delivered), duplication (a message is delivered more often than sent), corruption (another value is delivered than sent) and reordering of messages (messages are delivered out of order). Often, assumptions regarding the reliability of message transmission are made. Thereby different levels of reliability can be distinguished. According to Guerraoui and Rodrigues (2006) a fair-loss-point-to-point-connection, for example, guarantees that a infinitely often sent message will be delivered, a message that is infinitely often received, was sent infinitely often, and messages are never corrupted.

Fault tolerance
A fault, like the loss of a message, may cause an error, which is an internal system state that does not conform to the specification. An error in turn may further lead to a failure, meaning that the system deviates from its correctness specification (Gärtner, 1999). Fault tolerance describes the ability of a distributed system to continue to provide its service (possibly in a reduced manner) even in case of the appearance of faults in some of its components, instead of leading to a complete system failure (Tanenbaum and van Steen, 2008). When designing for a fault tolerance system, a first prerequisite is to specify the fault class that should be tolerated and afterwards enrich the system with components or concepts that provide protection against faults of the corresponding fault class (Gärtner, 1999). Therefore, the system behaves according to Gärtner (1999) in a well-defined manner once faults, from the considered fault class, occur.
In order to specify any useful behavior of a system Lamport (1977) distinguishes between two different necessary system properties. Namely safety and liveness. Informally, a safety property states that "something bad" never happens in the system. Whereas a liveness property claims that "something good" will eventually happen in every execution of the system. The following example illustrates the meaning of those two properties. A common application for a distributed algorithm is mutual exclusion i. e., an algorithm that ensures the requirement that no two concurrent processes are in their critical section at the same time. In this scenario, the safety property states that there is always at most one process in the critical section, while the liveness property claims that every process that requests to enter a critical section will eventually enter the critical section.
Gärtner (1999) identifies four forms of fault tolerance in dependence of whether safety or liveness properties are ensured by the algorithm in presence of faults.
live not live safe masking fail safe not safe nonmasking fault intolerant  3

.1 Fault Intolerance
Fault Intolerance means neither liveness nor safety is guaranteed in the presence of faults from a certain fault class. Therefore, the system does not offer any form of fault tolerance for this fault class and is the most trivial, weakest, cheapest, and undesirable form (Gärtner, 1999).

Masking
Masking fault tolerance is the other extreme case where both liveness and safety are ensured in case of faults (from a certain fault class). Therefore it is the most strict, and most desirable form of fault tolerance. With masking fault tolerance, the system is able to tolerate faults transparently, i. e., a user of the system cannot determine the occurrence of a fault (Gärtner, 1999). This can be necessary if even a temporary failure of the system would have unacceptable consequences such as the death of humans or unbearably high financial losses. Masking fault tolerance is indeed the most costly form as this can only be achieved through redundancy in time or space (Tanenbaum and van Steen, 2008;Gärtner, 1999). Redundancy in space means multiple instances of components. An example is triple modular redundancy (TMR). In TRM, there are three redundant components that deliver inputs to one voter. If at least two of these inputs are the same, the voter outputs that value. In this way, one faulty component can be masked whether it delivers an illegal input value or no input at all (Tanenbaum and van Steen, 2008). Nevertheless, if the voter or two of the components are erroneous, masking is not possible anymore. More generally speaking, masking fault tolerance is only successful if only a limited part of the components is erroneous. The amount of the erroneous components that can be tolerated depends on the fault model.

Fail Safe
Fail safe fault tolerance is one of the two intermediate combinations and guarantees safety but not liveness. The idea is to ensure a safe state in presence of a fault or error. As the system may ceases to show progress, the occurrence of a fault may be observable. (Gärtner, 1999). An example is a traffic light control, where in case of an error all traffic lights are switched to red.

Nonmasking
Nonmasking fault tolerance is the last combination. In presence of a fault, liveness is ensured but safety is not guaranteed. In effect, the user may experience a certain amount of incorrect system behavior (i. e., failures) (Gärtner, 1999). For example in a replicated database, a replication variable may not be up to date, but at least liveness is guaranteed in the way that reading and writing requests will always be granted.
Masking fault tolerance is only possible for certain fault classes and it is not realistic to predict all kinds of possible faults and take them into account. Nonmasking fault tolerance is strictly weaker than masking fault and can therefore be used in cases where masking fault tolerance can not be achieved because it is provably impossible or too costly (Gärtner, 1999). Selfstabilization is a specialization of nonmasking fault tolerance, where any kind of transient faults can be tolerated (Gärtner, 1999).

Self-Stabilization
The approach of self-stabilizing systems was first introduced by Dijkstra (1974) in the context of distributed systems. He defined that "we call the system self-stabilizing if and only if, regardless of the initial state [. . .], the system is guaranteed to find itself in a legitimate state after a finite number of moves." Since self-stabilization guarantees that a legal state is reached from every starting state, it is not necessary to initialize the system in a certain way. Furthermore, this leads to the ability to tolerate any transient fault since if no new faults occur for a sufficient period of time, the state after the end of the last fault could be considered as a new initial state and the system must recover.
According to Schneider (1993) self-stabilization provides an unified approach for tolerating arbitrary transient faults, including inconsistent initialization, mode change, transmission errors like loss, corruption, or reordering, process failures with recovery and even memory crash. A transient fault is any event that may changes the state of the system, but not its behavior. Therefore, the behavior (i. e., the program code) of the system is not violable. A self-stabilizing algorithm is able to handle any corruption of the random-access memory (RAM) content but not of the read-only memory (ROM) (Dolev, 2000). The property of self-stabilization models the ability of a system to recover from transient failures under the assumption that they cease to occur (Schneider, 1993;Dolev, 2000;Gärtner, 1999). Another characteristic of self-stabilizing algorithms is that they must not terminate (Schneider, 1993). This follows from the fact that the processes must continuously communicate with neighboring nodes. If the participating processes would have a terminated state, the state that all processes are in their terminated state would also be a possible initial configuration. Therefore the task is achieved with no communication at all, which is not possible with a distributed algorithm (Dolev, 2000). As a consequence, the participating processes can not know whether the system is stabilized (i. e., is in a correct configuration). Dolev (2000) defines a self-stabilizing system as follows:

Definition 1: Self-Stabilizing System
A self-stabilizing system can be started in any arbitrary configuration and will eventually exhibit a desired "legal" behavior. We define the desired legal behavior by a set of legal executions denoted LE. A set of legal executions is defined for a particular system and a particular task. Every system execution of a self-stabilizing system should have a suffix that appears in LE . A configuration c is safe with regard to a task LE and an algorithm if every fair execution of the algorithm that starts from c belongs to LE (closure property). An algorithm is self-stabilizing for a task LE if every fair execution of the algorithm reaches a safe configuration with relation to LE (convergence property).
In order to prove convergence a basic proof technique according to Dolev (2000) is a potential function. The idea is to define a function over the configuration set and prove that this function monotonically decreases (or increases) with every executed step. Additionally, it has to be shown that after the function reaches a certain threshold, the system is in a safe configuration. Another way to prove convergence are so-called convergence stairs. Here the algorithm converges to fulfill k > 1 predicates A 1 , A 2 , . . . , A k , such that, for every 1 ≤ i < k, A i +1 is a refinement of A i . Whereby a predicate A i +1 refines the predicate A i if A i holds whenever A i +1 holds. Then it must be shown whenever A i holds every execution reaches a configuration where A i +1 holds for all i . The last predicate A k defines a safe configuration. Since the closure property states that every step from a safe or correct configuration leads again to a correct configuration, closure is usually proven through invariants.
An easier to achieve and easier to prove property is weak stabilization. According to Gouda (1995) a system is weakly stabilizing if for every initial configuration there is an execution that reaches a safe or correct configuration. This property is called weak convergence and is related to probabilistic convergence. 1. Convergence: By local neighborhood changes (i. e., by creating, forwarding, and deleting links with neighboring nodes), the nodes will eventually form an overlay topology with desirable properties from any initial (and in our case: connected) topology. 2. Closure: The system will also stay in a correct configuration provided that no external topological changes occur.

Linearization
A desired network topology could be for example a chain. Given a fixed set of nodes V with unique identifiers (ids) and a total order ≤ on V the goal is to build an ordered list of the nodes according to their unique ids. Therefore, a topology is desired where only consecutive nodes are connected (whereby succ(v) defines the next to v).

Definition 7: Subterms
Let L = 〈P , � −→ 〉 be a process calculus and P ∈ P a process term. The set of subterms of P = op (x 1 , . . . , x n , P 1 , . . . , P m ) is defined as Note that every process term is its own subterm.
In the following, we will give an intuitive approach in understanding the behavior, i. e., the semantics, of processes respectively process terms in name-passing process calculi. The most important constant and basic process is the empty process, usually denoted by 0. This process does not show any behavior and cannot interact with its environment, therefore it can be seen as a deadlocked process. Otherwise processes are capable to perform actions of the forms: output, input, and internal. The (a)synchronous sending of a message with name y over channel x (usually written x � y � ) and receiving an arbitrary name over channel x (usually written x(a)) allow processes to interact with their environment. Internal actions (usually written τ) are typically caused by interaction, further details are unobservable for the environment. The input operator x(a) binds the variable a which is substituted through a corresponding output operator x � y � by the received name y during interaction. The most common and important operator to combine processes P,Q is the parallel composition (usually written P | Q). In parallel composition processes can execute actions independently of each other or interact with each other. Another possibility to bind a name is through a restriction operator (usually written (νx) P ). In (νx) P the scope of x is restricted to P . Whereby a scope defines an area in which a particular name is known and can be used. Therefore the components of P can use x to interact with one another but not with other processes outside the scope. However, the sending of x via some other name extends the scope of x by the receiving process. Furthermore, there is typically a way to introduce repetitive behavior, either by a replication operator (usually written !P ) or through recursion by process equations.
According to Peters et al. (2013) in process calculi intuitively, the degree of distributability corresponds to the number of parallel components that can act independently. Practical experience has shown that it is not possible to implement every π-calculus term, not even every asynchronous one, in an asynchronous setting while preserving its degree of distributability. One of the limiting factors for how suited a calculus is to model an asynchronous system, are synchronization patterns, especially the so-called synchronization pattern M. The synchronization pattern M is minimal in the sense that smaller patterns do not limit the distributability in the same way (van Glabbeek et al., 2008). Peters et al. (2013) proved that this pattern is present in the asynchronous π-calculus. One calculus that does not contain this pattern is according to Brodmann (2014) the localized π-calculus.

Localized Pi-Calculus
The localized π-calculus is a subcalculus of the asynchronous π-calculus that restricts how received names can further be used by processes. Intuitively, a process cannot receive messages over a previously received name, but send messages on the corresponding channel and communicate the name to other processes.
The grammar of the localized π-calculus according to Merro and Sangiorgi (1998) has operators of inaction, input prefix, asynchronous output, parallel composition, restriction, and replicated input: Definition 8: Syntax of the Localized π-Calculus P L : P : where in a(x) .P name x may not occur free in P in input position. The meaning and consequences of the restriction are described in Sangiorgi and Walker (2003) as follows. In the localized π-calculus, when a process receives a name, it can only use it for sending or send it to another process, which must itself respect the output-capability constraint. The output-capability constraint arises frequently in applications. For instance, a process is an operating system that is responsible for managing a printer can communicate to another process the capability to send a job to the printer, but not the capability to receive a job intended for the printer. A consequence of the output-capability constraint is that in a process (νx) P every possible input via x is visible in the syntax of P : no input can be created, either inside or outside P . In other words, every process that receives via a name is local to the process that created that name. This locality property of names gives the localized π-calculus its name.

Algorithm
In this chapter, we introduce two variants of a simple linearization algorithm from Gall et al. (2014) designed for a shared memory system. We first describe the characteristics of the system and the model used. Afterwards, we briefly present the algorithm and subsequently illustrate the proof idea to show that the algorithm is a linearization algorithm according to Definition 4. Gall et al. (2014) claim that the motivation for topological self-stabilization is, to build robust open distributed systems, like peer-to-peer systems. However, a shared memory model is not the most suitable one for this task. Therefore, we redesign the algorithm from Gall et al.
(2014) for a system with asynchronous message-passing. We describe an extended version of the localized π-calculus that is the foundation for our redesign. Thereafter we introduce our model and finally the redesigned algorithm.

Model for shared memory
First let us introduce the model as presented in Gall et al. (2014) to enable a clear understanding of the original algorithm.
A system consists of a fixed set V of n nodes, whereby each node has a unique integer identifier and nodes are compared by their corresponding id. A distributed algorithm is executed by each node in the network concurrently. The algorithm for each node is expressed by a set of variables and actions. An action has the form < name > : < guard > → < commands > where < name > is an action label, < guard > is a boolean predicate over the (local and shared) variables of the executing node and < commands > is a sequence of commands that may involve any local variables and shared variables of the node itself or its neighbors.
An action is enabled if and only if its guard is true. Every enabled action is passed to a scheduler. An action that is chosen and executed by the scheduler is called a step. The assignments of all local and shared variables define the global state of the system, i. e., a configuration. Each configuration represents a graph since only variables are considered that directly effect the topology. An execution is a sequence of configurations, such that each configuration c i + 1 is the topology resulting from executing step i , selected by the scheduler, on the previous configuration c i . A scheduler is treated as a global entity that decides which (independent) actions are executed in parallel to explore the complexity of the algorithms. Gall et al. (2014) introduce two variants of a linearization algorithm, named LIN all and LIN max . Both variants are based on the idea that whenever a node u has two neighbors v and w, both of which have a smaller (or both a greater) id, the node can establish a link between them and delete its link to the smaller (respectively greater) one w. Therefore there are just two simple linearization rules, left linearization and right linearization. The effects of linearization steps on the topology are depicted in Figure 2 The variants of the algorithm only differ in which linearization steps are enabled and therefore proposed to the scheduler. In LIN all , every node enables all possible linearization steps on each side. Therefore according to Gall et al. (2014):

Definition 9: LIN all
For every node u, there are the following rules for every pair of neighbors v and w:

Algorithm for shared memory
In LIN max , every node u only enables the linearization steps that acquaint the two furthest nodes on the corresponding side and therefore eliminates the longest edges to each side of u. Hence according to Gall et al. (2014):

Definition 10: LIN max
Every node u uses the following rules for every pair of neighbors v and w: Whereby u.L denotes the set of all left neighbors of u i. e., all neighbored nodes with a smaller id, and respectively u.R denotes all right neighbors of u i. e., all neighbors with a greater id.

Proof Idea
To prove that the algorithm is a linearization algorithm according to Definition 4, it has to be shown with Definition 2 that the closure and convergence properties are fulfilled. In the following, we will shortly picture the idea of the proofs and the main arguments from Gall et al. (2014).
In order to prove the closure property, Gall et al. (2014) show that there is a unique legal configuration. Further they show that any enabled linearization step, regardless of whether left or right linearization, is contradictory to this legal configuration and therefore all actions are disabled. Thus all neighborhoods and, by association, the linearized topology does not change. Accordingly, the system remains in a correct configuration in case no fault occurs.
To prove convergence Gall et al. (2014) introduce a potential function that sums up the length of all edges in the current topology. It holds that the only connected topology with minimal potential is the unique correct configuration. Further, they show that an initial connected topology always stays connected and that in every connected topology, that is not the legal configuration, there is an enabled left or right linearization step. Furthermore, it is shown that with every executed linearization step, the potential function decreases as the new established edge is always strictly shorter than the removed edge. Therefore, the topology converges to the correct configuration in a finite number of steps. Gall et al. (2014) state in their model that a shared variable e(u, v) can only be changed by u and v. However, in the algorithms the shared variables are written not only by the nodes themselves but also by their neighbors. Therefore, the algorithm only works in a setting where all nodes have write access to the whole memory, as the algorithm could be initialized with any topology and hence also with the fully meshed graph. Since this is a very restrictive model, especially in the context of peer-to-peer networks, we are interested in redesigning the algorithm for a setting with asynchronous message-passing.

Model for Asynchronous Message-Passing
In this section, we describe our model for a linearization algorithm in an asynchronous message-passing system. Furthermore, to lower the system assumptions as much as possible, we assume that the processes can only communicate via unidirectional channels. Similar to Gall et al. (2014), we assume that there are n processes in the system and every process has a unique id. To be as general as possible, we only assume that there is a total order on these ids without further specifying the type. Furthermore, we assume that every value in the system can be interpreted as the id of an existing process. Therefore the corruption of RAM and messages is only considered in the way, that the result is an arbitrary value that is still interpretable as an existing id. This could be implemented in a real system through a type check or similar mechanisms. If this is not possible, but illegal values can be detected, we can simply discard such values.
Assumption 1: Ids Every process has a unique constant id and every value in the system can be interpreted as the id of an existing process.

Definition 11: Process identifiers P
Let P be the (non-empty) finite set of unique identifiers of the processes in the system. Let ≤ be a total order on P . Let |P | = n ∈ N then there exists an index function (bijection) i : P → {1, . . . , n} and ∀p ∈ P .i (p) = |{q ∈ P |q ≤ p}| i. e., i (p) describes the position of p with respect to ≤.
We now define the predecessor and the successor of a process as respectively the next smaller and next greater process according to the total order (and ⊥ if there is none). We call such a pair of processes consecutive.

Definition 12: Predecessor pred and Successor succ
The predecessor and successor of a process p ∈ P are then defined as pred, succ : P → (P ∪ ⊥) with

Corollary 1: Predecessor pred and Successor succ
Hence ∀p ∈ P .succ(p) � = ⊥ =⇒ (succ(p) > p ∧ ∀q ∈ P .q > p =⇒ q ≥ succ(p)) and ∀p ∈ P .pred(p) � = ⊥ =⇒ (pred(p) < p ∧ ∀q ∈ P .q < p =⇒ q ≤ pred(p)) In this setting, the desired topology i. e., the overlay network that the processes (represented as nodes) shall establish, is an ordered doubly-linked list according to the total order on the ids (depicted in 2.2 for five nodes and labeled with the position of their id according to the total order). This means that every process has an unidirectional link (represented as edge) to its predecessor (with exception of the smallest process) and its successor (with exception of the greatest) and there are no other links. We call this topology the (directed) linear graph.
The undirected linear graph is the undirected variant of this desired topology. Therefore for every pair of consecutive processes at least one of them has a link to the other one.

Definition 14: Desired Topology Graph
The (directed) linear graph G LIN = (V, E ) is defined as The undirected linear graph UG LIN = (V, E ) is defined as UG LIN = undirected(G LIN ) i. e., The distance between two processes is the number of nodes between the processes according to the total order. Therefore, a process has a distance of zero to itself and the distance between a pair of consecutive processes is one.

Definition 15: Distance dist
The distance between two nodes p, q ∈ P is defined as dist : P × P → N with The length of an edge (regardless whether directed or undirected) is defined as the distance of the nodes it is connecting.

Definition 16: Length of Edges
Let G = (P , E ) be an arbitrary undirected graph and G � = (P , E � ) be an arbitrary directed graph.
The length of an edge e = {p, q} ∈ E respectively e = (p, q) ∈ E � is defined as The maximum distance between a pair of processes in the system is the distance of the smallest and the greatest process. This is obviously with the Definitions 15 and 11 n − 1. This is also the length of the longest possible edge, as the length of edges is defined as the distance between its end-points. We call this maximum distance maxdist.

Definition 17: Maximum Distance
The maximum distance for the set of process identifiers and therefore the length of the longest possible edge in the network topology is:

Extended Localized Pi-Calculus
To model the algorithm, we introduce an extension of the name-passing localized π-calculus. This extension is based on ideas similar to Wagner and Nestmann (2014). We call the calculus the extended localized π-calculus and denote it with eLπ = 〈P eL , � −→ 〉. This allows us to define a kind of standard form for a configuration of our algorithm. The local state of all processes and the messages in transit, and therefore the global state of the system, is directly accessible via the parameters of the corresponding process definition. This in turn allows state-based proofs, which is more traditional for distributed algorithms (Lynch, 1996), instead of the action-based style of process calculi. Since sets are only special cases with multiplicity one for all elements, we also use combinations of sets and multisets.

Notation: Multisets
We assume the existence of a countably infinite set A containing all channel names, function names, and variables.
where in c(X ) .P variable x as part of X may not occur free in P in input position. K (X ) denotes a parameterized process constant, which is defined with respect to a finite set of process equations D of the form {K j (X ) = P j } j ∈J . Since we use parameterized process constants, we exclude replication and use instead recursion via process definitions to model repetitive behavior.
Names received as an input and restricted names are bound names. The remaining names are free names. Accordingly, we assume three sets, the sets of names n(P) and its subsets of free names fn(P) and bound names bn(P), with each term P . To avoid name capture or clashes, i. e., to avoid confusion between free and bound names or different bound names, bound names can be mapped to fresh names by α-conversion. We write P ≡ α Q if P and Q differ only by α-conversion.
The substitution of value v for a variable pattern X in expression e or process P is written { v /X }e and { v /X }P respectively. Note that only data values can be substituted for names and that all variables of the pattern X must be free in P (while possibly applying α-conversion to avoid capture or name clashes).
Let �e� denote the evaluation of expression e which allows results in a data value, defined in the standard way.

Definition 19: Structural Congruence for the Localized π-Calculus
Now we present the structural congruence for the extended localized π-calculus. The definition is based on the structural congruence for the π- Calculus.
We are only interested in the interaction between the processes and not with any further environment. Therefore, we only present a reduction semantics for our extended localized π-calculus, based on the reduction semantics of the π-calculus.
Definition 20: Reduction Semantics of the extended Localized π-Calculus-� −→ We call a single application of this reduction semantics a step. We write P � −→ P � and we call P � a derivative of P and denote P � −→ if there is such a P � or P �� −→ if not. We write � =⇒ for the reflexive and transitive closure of � −→. We use execution to refer to a reduction starting from a particular term.
Every structural extension like function calls, if-then-else-statements, and let-in-statements are evaluated in the structural congruence. Therefore, the evaluation of these constructs is not considered a step on its own. Hence, internal computations are executed as parts of other steps.
As the state after every fault can be seen as a new initial state we assume that there are no faults. An infinite message delay can be seen as message loss. Therefore, every message that is sent is received after finite time. Since the message-passing model is asynchronous, there are no further assumptions regarding the delivering time of messages.

Assumption 2: No Message Loss
Every message is received after a finite but arbitrary number of steps.
Furthermore, we need an assumption of fairness, as otherwise nodes could starve. A process starves if it never executes a step. Furthermore, a subprocess of a node starves, for example, if the process is only consuming messages, but never tries to find a linearization steps itself. Therefore, without a fairness assumption, it is not possible to show any progress in the system.

Assumption 3: Fairness
Every continuously enabled subprocess will eventually (after an arbitrary but finite number of steps) execute a step.
The formal definitions are given in Section 2.3.

Linearization Algorithm for Asynchronous Message-Passing
The utilization of a calculus enables us to model the algorithm unambiguously and allows us to formally prove properties of the algorithm. Although in the calculus itself all channels are bidirectional, we only use them as previously stated in an unidirectional manner to lower the system requirements as much as possible. Together with the output-capability restriction of the localized π-calculus this helps us to ensure that every process can be implemented in an asynchronous setting on a different location. Therefore, the processes really are distributable.
In our algorithm, each node can receive messages from other nodes via a channel with the same name as its id. One could think of the ids as serving as the IP address of the corresponding process. To enable a neighbor to communicate with another process it is sufficient to send it the corresponding id. Therefore, the set A contains the ids of all processes in the system i. e., P ⊂ A. This simplifies the algorithm and the proof in the sense, that we do not need an additional mapping from the ids to a corresponding channel name of the process and vice versa.
We use function calls, if-then-else-statements, and let-in-statements to model internal or local computations. Since the evaluation of function calls, if-then-else-statements, and letin-statements are part of the structural congruence, internal computations are part of other steps. A process can receive a message in a step, add a previously received process id to its neighborhood, or perform some local computations and send messages to other processes.
Since in process calculi any kind of behavior is represented by communication, variables must also be modeled through messages. To model local variables we use restricted channels for every process. Each variable is therefore represented through a message in transit that can only be received by the corresponding process. The value of the variable is the value of this message whereby receiving the message corresponds to reading the variable and sending corresponds to writing. In our algorithm, every process p has one local variable nb p , describing the neighborhood of the process i. e., it contains all processes that p knows and therefore can send messages to.
Each process can be in one of two local states. In the state Alg � p, nb � the process p is able to receive a message from another process in the system. In the state Alg � � p, nb, x � the process p can add a previously received process id x to its current neighborhood nb. Thereby, a process blocks the reception of messages until the the previously received process id is added to the neighborhood. In both states, the process can additionally try to find a linearization step in its current neighborhood nb based on internal computations. If it finds no possible linearization step in its neighborhood, it sends keep-alive-messages to its current neighbors. This can only happen if it knows at most one smaller and one greater process. These keep-alive-messages are necessary to prevent deadlocks and also to reach the desired network topology in case only edges are missing in the current topology to form the desired topology.

Linearization Algorithm for Asynchronous Message-Passing
In the algorithm, LeftN : P × 2 P → 2 P calculates the left neighborhood of a process i. e., all neighbors with a smaller id and corresponding RightN : P × 2 P → 2 P the right neighborhood of a process i. e., all neighbors with a greater id. They are defined as follows: The function findLin : P × 2 P ×P → 2 P ×P calculates all possible linearization steps in the neighborhood of a process, based on the input sets.
The function select : 2 P ×P → (P × P ) returns one of these linearization steps whereby we denote with ε Hilbert's choice operator returning an arbitrary element. Therefore, this corresponds to the LIN all variant of the algorithm in Gall et al. (2014). With another selection it would equally possible to implement LIN max .

Definition 22: Subprocesses
For every process p ∈ P we denote Alg match � p � , Alg rec � p � , and Alg add � p, · � as subprocesses of p. Note that all subprocess are input guarded i. e., they are all waiting to receive a message.
The subprocess Alg rec � p � models the behavior that a process is able to receive a message from another process in the system. When it receives such a message with content x, it continues as subprocess Alg add � p, x � and the process itself changes therefore its local state. Alg add � p, x � reads the current value of the neighborhood of p and adds the received process id x to its neighborhood. Afterwards, the process is again able to receive a new message from another process.  The subprocess Alg match � p � defines the behavior, based on the internal computations of the function findLin � p, nb � , in case process p tries to find a linearization step in its neighborhood nb. If select returns a left linearization step the process behaves according the second case, in case of a right linearization step according to the third case. In both cases, p sends the further away process the id of the other process and deletes it from its neighborhood (as depicted in Figure 2.6). If there is no possible linearization step, select returns ⊥ and the process sends keep-alive-messages to its current neighbors. The other cases are only implemented to obtain a complete case distinction but are ruled out by definitions. In all cases, the process is directly able to try to find another linearization step.
So far, we have just defined a single process. As the system is composed of n such processes, we define now the global state of such a system. The global states that serve as starting points for the executions of our algorithm are called initial configurations. Later we show that every global state can serve as such a starting point.

Definition 23: Initial Configuration
Let P be the set of unique identifiers of the processes in the system, P, P � ⊆ P with P ∪ P � = P and P ∩ P � = �, i ni t : P → 2 P a function that defines for every process p ∈ P the neighborhood i. e., which process ids are known by p, Msgs ∈ N P ×P a multiset that describes the messages in transit and add : P � P a partial function with ∀p ∈ P � .∃q ∈ P .(p, q) ∈ add and ∀p ∈ P.∀q ∈ P .(p, q) ∉ add that describes the adding in progress i. e., where add(p) = q describes that p wants to add q to its neighborhood. Then an initial configuration of the algorithm is defined as the process term: The assumption 1 that only valid values are in the system, i. e., every value can be interpreted as the id of some existing node, is reflected in the types of the parameters. Furthermore, we always assume for every message (x, y) ∈ Msgs that x � = y and for every p ∈ P that p ∉ nb(p) and add(p) � = p. This is not a strong restriction as every process knows its own id and could easily hold its set of neighbors free from itself, and no process ever sends a message on a channel that carries the channel name itself. But active handling would only lead to more cases in the proofs and therefore increase the complexity, without any information gain.
In an initial configuration there is for every process p ∈ P exactly one nb p 〈·〉-message. This message can not be lost or duplicated through a previous fault, since as stated they only serve to model a variable. Since the program code can not get corrupted, a fault can lead to an arbitrary value of a variable but not to its disappearance or duplication. Thus, the value of this message can be an arbitrary set of P (without p itself), reflecting the arbitrary neighborhood of p as initial state. Therefore, these messages of all processes describe the initial network topology. We will formally define variants of the network topology of a configuration in Chapter 3.2. They differ in whether or not messages still in transit are also taken into account, i. e., whether a message in transit and adding in progress is represented as an edge or not. A configuration describes the global state of the system, consisting of the local state of all processes and the messages in transit.

Definition 24: Configuration
Let I be the set of all initial configurations. We call every process term C that can be reached from any arbitrary initial configuration, i. e., ∃I ∈ I .I � =⇒ C configuration (of the algorithm) or process term of the algorithm. We denote the set of all such configurations with T .

Definition 25: Reachability
We call a configuration C � reachable from a configuration C iff C � =⇒ C � . Further, we say a configuration with a predicate P is reached from configuration C iff in every execution there is a configuration C � with C � =⇒ C � and P holds for C � .

Definition 26: Enabled Subprocess
We call a subprocesses S of process p, with p ≡ Alg � p, · � or p ≡ Alg � � p, ·, · � , enabled in a configuration C iff p is a subterm of C and there is a subterm S � of C with S ≡ S � and if S = Alg rec � p � a message m as subterm of C else a message m as subterm of p with S | m � −→.
First of all, we show in Chapter 3 that for every configuration C there are such parameters, so that C is structural equivalent to Alg ges (·, ·, ·, ·, ·). We call Alg ges (·, ·, ·, ·, ·) the standard form of a configuration and use them as representatives of all structurally equivalent configurations. Furthermore, it then holds that every configuration is structurally equivalent to an initial configuration. This reflects the fact that every configuration can serve as a starting point of our algorithm, as it is represented by a structurally equivalent initial configuration.
We define the topology of a configuration in different variants. Afterwards, we show that if the initial topology is weakly connected, while taking the messages that are still in transit into account, the topology always stays weakly connected.
Subsequently we define correct configurations as configurations with the desired topology and show the uniqueness of such configurations up to structural equivalence and the number of messages in transit.
The algorithm never terminates, as required for self-stabilizing algorithms. If the desired network topology is reached, every process (with exception of the smallest and greatest process) knows exactly one smaller (its predecessor) and one greater process (its successor).
The processes continue to send keep-alive-messages to their desired neighbors. Since keepalive-messages are the only messages that are send in a correct configuration, the topology does not change anymore and therefore closure holds.
Keep-alive-messages are among others necessary to prove convergence, i. e., that a correct configuration is reached, in case that the current topology only lacks edges compared to the desired topology. Without these message the system would deadlock, as no linearization steps are possible in such a configuration. However, unfortunately such message can for example also reestablish edges that where already deleted through linearization steps. This leads to some obstacles and makes proving convergence much more difficult and challenging than in the shared memory model. Therefore, we formally prove convergence for some special cases and weak convergence in the general case i. e., for every arbitrary initial configuration there exist executions that reach a correct configuration.

Proof
In this chapter, we present the formal proofs of properties of our algorithm. We start with some basic properties and introduce afterwards the topology of a configuration in different variants. A correct configuration is a configuration whose topology forms the desired topology i. e., in our case the (directed) linear graph. Subsequently, we show that whenever such a configuration is reached, the system stays in such a configuration and therefore closure holds. Afterwards, we prove convergence in the cases that the topology either only lacks desired edges or only contains too many edges i. e., every desired edge is already established in the topology. Furthermore, we show weak convergence for the general case.

Basic Properties
In this section, we prove some basic properties for the algorithm to simplify further proofs.
First of all, we show that for every configuration C there are parameters with the same properties as in Definition 23, so that C is structurally equivalent to Alg ges (·, ·, ·, ·, ·). We call Alg ges (·, ·, ·, ·, ·) the standard form of a configuration and use it as representative of all structurally equivalent configurations. Therefore, every configuration is structurally equivalent to an initial configuration.

Lemma 1: Standardform
Starting from an arbitrary initial configuration according to Definition 23 the process term of the algorithm has always a form that is structurally equivalent to a term Alg ges � P, P � , nb, Msgs, add � whereby P, P � ⊆ P with P ∪ P � = P and P ∩ P � = �, nb : P → 2 P is a function that defines for every process p ∈ P the neighborhood i. e., which process ids are known by p, Msgs ∈ N P ×P is the multiset of messages in transit, add : P � P is a partial function with ∀p ∈ P � .∃q ∈ P .(p, q) ∈ add and ∀p ∈ P.∀q ∈ P .(p, q) ∉ add i. e., where add(p) = q describes that p is adding q to its neighborhood.

Proof:
We prove this by induction over the step semantics. The claim holds for any initial configuration according to Definition 23. Let Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm that is reachable from an initial configuration. Then according to the semantic as defined in Definition 20 there are only the following kinds of steps possible: First, a process tries to find a linearization step: Let p ∈ P be an arbitrary process then Now there are four possible cases dependent on select � findLin � p, nb(p) �� : • if there is no possible linearization step in the neighborhood of p i. e., select � findLin � p, nb(p) �� = ⊥ : • if select returns a left linearization step i. e., Let p ∈ P � be an arbitrary process that tries to find a linearization step, then similar to the last case it holds that exactly one of the following four steps is possible: Alg ges � P, P � , nb, Msgs, add Alg ges � P, P � , nb, Msgs, add � � −→ Alg ges � P, P � , nb, Msgs, add � Second, a process receives a message: Let p ∈ P be an arbitrary process and ∃q ∈ P .(p, q) ∈ Msgs then Alg ges � P, P � , nb, Msgs, add �

Notation: Configuration Components
Let A be an arbitrary configuration of the algorithm then there are parameters P, P � , nb, Msgs and add such that A ≡ Alg ges � P, P � , nb, Msgs, add � and we denote in the following :

Corollary 2: Steps
For every process term Alg ges � P, P � , nb, Msgs, add � there are always exactly the following steps (up to structural congruence) possible:

Corollary 3: Unique Neighborhood-messages
For every process p ∈ P there is always exactly one nb p 〈·〉 message in the system.
Since every process only receives messages from other processes in the system via a channel name that corresponds to its unique id and the nb p channels are restricted, the receiver of every message is uniquely determined.

Lemma 2: Unique Receiver
There are no two processes that could receive the same message and therefore the receiver of a message is determinable. Let Alg ges � P, P � , nb, Msgs, add � be a process term of the algorithm according to Lemma 1 then it holds that for all m ∈ Msgs there is exactly one p ∈ P that could receive m.

Proof:
According to the definition of the process term and therefore every message m ∈ Msgs has always the form j 〈k〉 with j , k ∈ P . As the process ids P are according to Assumption 1 unique and every process p ∈ P only receives messages on the channel name p (and nb p ), the claim holds.

✷
Every subprocess is input guarded and gets enabled by the existence of a corresponding message. Since there is for every process p always one nb p 〈·〉 and other messages cannot be received by other processes and messages not get lost, every enabled subprocess stays enabled until it executes a step.

Lemma 3: Subprocesses stay Enabled
Every subprocess that is enabled at some point stays enabled until it executed a step.

Proof:
We prove this by induction over the execution. Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. Let A � be an arbitrary configuration with A � −→ A � . We have to show that every subprocess that was enabled in A, with exception of the subprocess that executed the step, is still enabled in A � . According to Corollary 2 there are the following cases: • Every process p ∈ P can execute a step to find a linearization step in every configuration as P ∪P � = P , Alg match � p � is a subterm of both Alg � p, nb(p) � and Alg � � p, nb(p), add(p) � , and according to Corollary 3 there is always exactly one nb p -message. Therefore, the subprocess Alg match � p � is always enabled.
• Let p ∈ P be an arbitrary process and there is q ∈ P with (p, q) ∈ Msgs i. e., p could receive a message in A and therefore the subprocess Alg rec � p � is enabled.
If the executed step was a step where any process r ∈ P tried to find a match, then it holds according to Corollary 2 that P A � = P, P � A � = P � and Msgs A � = Msgs ∪ X with X ⊂ P × P . Therefore, it holds p ∈ P A � and (p, q) ∈ Msgs A � = Msgs ∪ X and the step that p can receive p � q � and therefore the subprocess Alg rec � p � is still enabled in A � .
If the executed step was a step where a process r ∈ P received a message r 〈s〉 with s ∈ P , then there are two cases. If r = p then the subprocess Alg rec � p � executed the step. Otherwise it holds that r � = p and according to Corollary 2 that P A � = P \ {r }, P � A � = P � ∪ {r } and Msgs A � = Msgs \ {(r, s}. Therefore, it holds p ∈ P � A � = P � ∪ {r } and (r, s) ∈ Msgs A � = Msgs \ {(r, s} and the step that p can receive p � q � and therefore the subprocess Alg rec � p � is still enabled in A � . If the executed step was a step where a process r ∈ P � added a process s to its neighborhood i. e., add(r ) = s, then it holds that r � = p as P ∩ P � = � and according to Corollary 2 that P A � = P ∪ {r }, P � A � = P � \ {r } and Msgs A � = Msgs. Therefore, it holds p ∈ P � A � = P � \ {r } and (p, q) ∈ Msgs A � = Msgs and the step that p can receive p � q � and therefore the subprocess Alg rec � p � is still enabled in A � .
• Let p ∈ P � be an arbitrary process and q ∈ P with add(p) = q i. e., p could add q to its neighborhood in A and therefore the subprocess Alg add � p, q � is enabled.
If the executed step was a step where any process r ∈ P tried to find a linearization step, then it holds according to Corollary 2 that P A � = P, P � A � = P � and add A � = add. Therefore, it holds p ∈ P � A � and add A � (p) = q and the step that p can add q to its neighborhood and therefore the subprocess Alg add � p, q � is still enabled in A � .
If the executed step was a step where a process r ∈ P received a message r 〈s〉 with s ∈ P , then it holds that r � = p as P ∩ P � = � and according to Corollary 2 that P A � = P \ {r }, Therefore, it holds p ∈ P � A � = P � ∪ {r } and add A � (p) = q and the step that p can add q to its neighborhood and therefore the subprocess Alg add � p, q � is still enabled in A � .
If the executed step was a step where a process r ∈ P � added a process s to its neighborhood i. e., add(r ) = s, then there are two cases. If r = p then it holds that s = q and the subprocess Alg add � p, q � executed the step. Otherwise r � = p and it holds according to Therefore, it holds p ∈ P � A � = P � \ {r } and add A � (p) = q and the step that p can add q to its neighborhood and therefore the subprocess Alg add � p, q � is still enabled in A � .

✷
Since every message in transit is received eventually and the addition of an previously received process id is executed eventually, there is always a configuration reached such that the corresponding process id is in the neighborhood of the receiving process (nevertheless it can be deleted later).

Lemma 4: Progression of adding a Process to the Neighborhood
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Let p ∈ P be an arbitrary process with p ∈ P � A and q ∈ P with add A (p) = q. Then there will be a step where the process p adds q to its neighborhood i. e., there will be configurations R, R � reached with A � =⇒ R and R � −→ R � and it holds that: and therefore q ∈ nb R � (p).

Proof:
From p ∈ P � A and add A (p) = q it follows that the subprocess Alg add � p, q � is enabled and according to Lemma 3 it stays enabled until it executes a step. According to the fairness will execute a step after a finite number of steps. Let R be the configuration before this step. Then it holds according to Corollary 2 and therefore q ∈ nb R � (p).

Lemma 5: Progression of receiving a Message
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Let p ∈ P be an arbitrary process with q ∈ P and (p, q) ∈ Msgs A . Then there will be a step where process p receives the message i. e., there will be configurations R, R � reached with A � =⇒ R and R � −→ R � and it holds that: According to the Assumption 2 that there is no message loss, the message will be eventually (after a finite number of steps) received. According to Lemma 2, p is the only process that can receive this message. Let R be the configuration before this step. Then it holds according to Corollary 2

Corollary 4: Progression of adding a Process from a Message to the Neighborhood
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Let p ∈ P be an arbitrary process with q ∈ P and (p, q) ∈ Msgs A . Then there will be a step where the process p receives the message and later a step where it adds q to its neighborhood i. e., there will be holds that: This follows directly as the conclusion of Lemma 5 is the precondition of Lemma 4.
Whether a process finds a linearization step or not, depends on the number of neighbors a process has. If a process has more than two neighbors, at least two of them must be on the same side (i. e., both have smaller or greater process ids) and therefore there must be a possible linearization step. If a process has less than two neighbors, then there cannot be a possible linearization step and the process sends therefore keep-alive-messages . If a process has exactly two neighbors, there is a possible linearization step if both are on the same side and otherwise it sends keep-alive-messages . Hence, sending keep-alive-messages and finding a linearization step are mutually exclusive, but either one or the other happens if a process tries to find a linearization step.

Lemma 6: Number of Neighbors |nb(·)|
Let A be an arbitrary configuration of the algorithm. Let p ∈ P be an arbitrary process that tries to find a linearization step i. e., the subprocess Alg match � p � executes a step in A. Directly from �� and the property that ≤ is a total order (Definition 11) it follows: if one of the processes is smaller and the other one greater i. e., • there is an enabled linearization step for p ⇐⇒ p can not send keep-alive-messages • p can send keep-alive-messages ⇐⇒ there is no enabled linearization step for p

Topology of Configuration
In this section, we define the network topology of a configuration. We introduce variants, which differ in whether we regard the direction of the edges, and if we take the messages that are in transit into account or not. The network topology graphs with messages describe how the neighborhood sets would be if all current messages in transit were received and processed (depicted in Figure 3.1). Therefore, the network topology graphs without messages of a configuration are always subgraphs of the topology graphs with messages.

Definition 27: Network Topology Graph
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. Then the (directed) network topology graph NT(A) = (V, E ) is defined as follows:

Definition 28: Network Topology Graph with Messages
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. Then the (directed) network topology graph with messages NTM(A) = (V, E ) is defined as follows:

Corollary 5: NT ⊆ NTM
Let A be an arbitrary configuration of the algorithm. Then the directed network topology graph is always a subgraph of the directed network topology graph with messages i. e.,

Definition 29: Undirected Topology Graph
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. Then the undirected network topology graph UNT(A) = (V, E ) is defined as follows:

Corollary 6: undirected(NT) = UNT
Directly from the Definitions 27 and 29 it follows that for an arbitrary configuration A it holds that

Definition 30: Undirected Topology Graph with Messages
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. Then the undirected network topology graph with messages UNTM(A) = (V, E ) is defined as follows:

Corollary 7: UNT ⊆ UNTM
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Then the undirected network topology graph is always a subgraph of the undirected network topology graph with messages i. e.,

UNT(A) ⊆ UNTM(A)
We show that if the topology graph with messages of the initial configuration is weakly connected, than the topology graph with messages of all reachable configurations is weakly connected. The only steps that lead to a removal of edges are linearization steps. Nevertheless, if a process executes a linearization step, the removed edge can always be simulated by the new introduced edge and the edge to the other neighbor of the executing process. Therefore, linearization can not result in partitioning the network topology.

Lemma 7: Connectivity
Msgs 0 , add 0 � be an initial configuration according to Definition 23 and let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary reachable configuration according to Lemma 1. Then, it holds that if the initial undirected topology graph with messages i. e., We will prove the lemma by induction over the execution.
be an arbitrary configuration with A i � −→ A i +1 , according to Corollary 2 there are only the following cases possible: • If a process p ∈ P tries to find match but select � findLin � p, nb i (p) �� = ⊥, it sends keepalive-messages to any neighbor i. e., to any process j ∈ nb i (p). It holds that and therefore UNTM(A i +1 ) = UNTM(A i ) and connected by assumption.
• If a process p ∈ P finds a match with a left-linearization step i. e., it holds that , it sends the smaller process (and therefore the process with the greater distance) j ∈ nb i (p) a message and deletes it from its neighborhood. It holds that , then it holds that the edge is removed or not (dependent on whether there is still a message in transit with same edge or not) and therefore The first case is true if any of the following holds (p, j ) ∈ Msgs i , ( j , p) ∈ Msgs i , ( j , p) ∈ add i or p ∈ nb i ( j ) but the (potentially) addition of a new edge cannot disconnect the topology graph and therefore UNTM(A i +1 ) is still connected. In the second case similarly only the removal of {p, j } could lead to a disconnection. It holds obviously that . Therefore, every path that used the edge {p, j } can be simulated by using the edges {p, k} and {k, j } and it holds that UNTM(A i +1 ) is still connected.
• If a process p ∈ P finds a match with a right-linearization step i. e., it holds that , it sends the greater process (and therefore the process with the greater distance) k ∈ nb i (p) a message and deletes it from its neighborhood. It holds that �� could have any other return value, it holds that and therefore UNTM(A i +1 ) = UNTM(A i ) and connected by assumption.
• If a process p ∈ P i receives a message from another process q ∈ P i. e., (p, q) ∈ Msgs i , the message is consumed but p will later add q to its neighborhood. It holds that and therefore UNTM(A i +1 ) = UNTM(A i ) and connected by assumption.
• If a process p ∈ P � i adds another process q ∈ P to its neighborhood i. e., (p, q) ∈ add i , it holds that and hence UNTM(A i +1 ) = UNTM(A i ) and connected by assumption.

Correct Configuration
A configuration is correct if every process exactly knows its consecutive processes. To ensure that also no other connections will be established through messages, it must additionally hold that every message in transit contains the id of a consecutive process of the receiver. Therefore, the network topology with and without messages must be the desired topology i. e., the linear graph. With exception of the number of these messages and the local state of the processes, the correct configuration is uniquely defined.

Definition 31: Correct Configuration
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be a process term of the algorithm according to Lemma 1.
Then, A is a correct configuration iff the directed topology network graph without and with messages is the linear graph i. e.,

Lemma 8: Up to -Uniqueness of Correct Configuration
The correct configuration is unique up to structural congruence, the number of messages in the system and the state of the processes.

Proof:
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1 and A is a correct configuration i. e., NTM(A) = G LIN ∧ NT(A) = G LIN . Then it holds according to the Definitions 14, 27 and 28 that A is a correct configuration iff: ✷ A weaker property is described by an undirected correct configuration. Here, we only demand that the undirected topology graph with message must be the undirected linear graph (as depicted in Figure 3.2). Therefore, the neighborhood of each process is a subset of the consecutive processes and the messages in transit must satisfy the same requirement as in the case of a correct configuration. In order to ensure connectivity, between each pair of consecutive processes there must be at least one connection while taking the messages in transit into account. Similarly to a correct configuration, an undirected configuration is uniquely defined with exception of the number of messages, the state of a process, and the type of the connection, i. e., a message, addition in progress, or neighborhood relation, between a consecutive pair of processes.

Definition 32: Undirected Correct Configuration
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be a process term of the algorithm according to Lemma 1.
Then A is an undirected correct configuration iff the undirected topology network graph with messages is the undirected linear graph i. e.,

Lemma 9: Up to -Uniqueness of undirected Correct Configuration
The undirected correct configuration is unique up to structural congruence, the number of messages in the system, the state of the processes, and the type of connections.

Proof:
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be a process term of the algorithm according to Lemma 1 and A is an undirected correct configuration i. e., UNTM(A) = UG LIN . Then it holds according to the Definitions 14 and 30 that A is an undirected correct configuration iff:

Closure
In this section, we introduce several closure properties that are based on the properties that only a process itself can remove processes from its neighborhood and a process never removes the process id from a desired neighbor i. e., its predecessor and successor. Furthermore, if every process knows (a subset) of desired neighbors but no other processes, then there are no possible linearization steps anymore in the system. All process can only send keep-alive-messages to their known desired neighbors and receive such messages.
As already stated, the only steps that remove edges i. e., process ids from the neighborhood of a process, are linearization steps. Therefore, whenever a process does not execute any linearization steps, its neighborhood can be expanded by reception of messages from other processes but it cannot shrink.

Lemma 10: Growing Neighborhood
If a process not executes a linearization step, its neighborhood can only grow.
Let A be the process term of the algorithm according to Lemma 1. Let R be an arbitrary

Proof:
We proof this by induction over the step semantics.
Obviously it holds nb A ⊆ nb A . Let p � ∈ P be an arbitrary process. Let C be an arbitrary con- We have to show that if the subprocess ing to Corollary 2 there are only the following cases:

Closure
Let p ∈ P be the executing process. Since Alg match � p � is the executing subprocess and Let p ∈ P be the executing process. Since Alg match � p � is the executing subprocess and Let p ∈ P be the executing process.
✷ Therefore, only in linearization steps a process removes processes from its neighborhood. However, if a process executes a linearization step it never removes a correct neighbor i. e., its successor or predecessor, as it always removes the process that is further away. Therefore, if a process knows a correct neighbor, this correct neighbor remains in the neighborhood for every reachable configuration.

Lemma 11: Preservation of Correct Neighbors
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Whenever a process p ∈ P knows a correct neighbor i. e., succ(p) or pred(p), it will not remove this neighbor anymore. Let R be an arbitrary reachable configuration i. e., A � =⇒ R, then it holds

Proof:
We prove this by induction over the step semantics. Let p ∈ P be an arbitrary process with succ(p) ∈ nb A (p). Obviously it holds nb A = nb A .
Let A � be an arbitrary configuration with A � =⇒ A � � −→ R and succ(p) ∈ nb A � (p). We have to show that succ(p) ∈ nb R (p). According to Lemma 10 it holds that if the executed step is not performed by the subprocess Alg match If the subprocess Alg match � p � executed the step, there are only the following cases left: According to Corollary 1 it holds that succ(p) > p and therefore succ(p) � = j . Hence According to Corollary 1 it holds that succ(p) ≤ j < k and therefore succ(p) � = k. Hence

Closure
The proof for pred(p) is similar.
✷ Therefore, it follows directly that in the directed and undirected topology without messages edges between consecutive neighbors are preserved as the edges depict the neighborhood sets.

Corollary 9: Preservation of Correct Edges
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. For every reachable configuration R i. e., A � =⇒ R it holds with Definitions 27 and 29 that: This preservation holds furthermore also for correct edges in the topologies with messages.
Here, an edge can also represent an adding of a process to be performed or a message in transit. But every id carried by a messages in transit cannot get lost and is therefore received and processed eventually. Therefore, also edges between desired neighbors that represent adding or messages are preserved.

Lemma 12: Preservation of Correct Edges in Topology Graphs with Messages
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to Lemma 1. For every reachable configuration R i. e., A � =⇒ R it holds that: Proof: Let p ∈ P be an arbitrary process with (p, succ(p)) ∈ E NTM(A) , then there are according to Definition 28 the following cases: • succ(p) ∈ nb(p): According to Definition 27 and Corollaries 9 and 5 it holds for every reachable configuration R that (p, succ(p)) ∈ E NTM(R) • add(p) = q: Then it holds that the subprocess Alg add � p, succ(p) � is enabled and according to Lemma 3 it stays enabled until it executes a step. According to the fairness a step after a finite number of steps. Up to this point it holds for every intermediate configuration C that add C (p) = succ(p) and therefore (p, succ(p)) ∈ E NTM(C ) . Let C � be the configuration before this step. Then it holds according to Corollary 2 and therefore succ(p) ∈ nb � (p) and with Definition 28 (p, succ(p)) ∈ E NTM(R � ) . According to the previous case, for every further reachable configuration R it holds also that (p, succ(p)) ∈ E NTM(R) .
• (p, succ(p)) ∈ Msgs: According to the Assumption 2 that there is no message loss, the message will be eventually (after a finite number of steps) received and for every configuration C up to this point it holds that (p, succ(p)) ∈ Msgs C and therefore (p, succ(p)) ∈ E NTM(C ) . According to Lemma 2 p is the only process that can receive this message. Let C � be the configuration before this step. Then it holds according to and with Definition 28 (p, succ(p)) ∈ E NTM(R � ) . We have now reduced the problem to the previous case and for every further reachable configuration R it holds also that (p, succ(p)) ∈ E NTM(R) .
The proofs for pred(p) and UNTM are similar.

✷
The topology of a configuration contains the desired configuration i. e., the linear graph is a subgraph of the topology, if every correct edge is already established but possibly undesired edges are still existent in addition. Since every correct edge is always preserved, it follows directly that whenever the linear graph is a subgraph of a configurations topology, this property applies also to any reachable configuration.

Corollary 10: Closure for NTM ⊆ G LIN ∧ NT ⊆ G LIN
It follows directly from Definition 14, Corollary 9 and Lemma 12 that if A is a configuration In the topology of an undirected correct configuration every edge is a correct edge but there are possibly correct edges missing. Through preservation of correct edges also this property is invariant and therefore carries over to every reachable configuration. Hence, every configuration that is reachable from an undirected correct configuration is itself an undirected correct configuration. Further, for every reachable configuration it holds that there are possibly still correct edges missing but none of the already established correct edges was removed.

Lemma 13: Closure for Undirected Correct Configuration
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm and A is an undirected correct configuration, then it holds for every reachable configuration C that C is also an undirected correct configuration.

Proof:
We prove this by induction over the step semantic i. e., every possible step leads again to an undirected correct configuration.
Since A is an undirected correct configuration according to Definition 32, it holds that UNTM(A) = UG LIN . According to Lemma 9 it holds that Since ∀p ∈ P .nb(p) ⊆ {succ(p), pred(p)} ⊥ and the Definition of select (findLin ()), it holds that According to Corollary 2 there are only the following steps possible: Since the only change in the configuration concerns the multiset of messages and nb(p) ⊆ {succ(p), pred(p)} ⊥ , it still holds that and therefore R ≡ Alg ges � P, P � , nb, Msgs ∪ {( j , p)| j ∈ nb(p)}, add � is an undirected correct configuration according to Lemma 9.
Let p ∈ P be an arbitrary process and q ∈ P with (p, q) ∈ Msgs. According to the assumptions it holds that q = succ(p) ∨ q = pred(p) and therefore Additionally, with the assumptions it obviously holds that: Since UNTM(A) is connected, it also holds according to Lemma 7 that the topology is still connected. Therefore R ≡ Alg ges an undirected correct configuration according to Lemma 9.
Let p ∈ P � be an arbitrary process and q ∈ P with (p, q) ∈ add. According to the assumptions it holds that q = succ(p) ∨ q = pred(p) and therefore Additionally, with the assumptions it obviously holds that: According to definition 1 in order to show that the algorithm is self-stabilizing, we have to prove the properties convergence and closure. In order to be a linearization algorithm according to definition 4, the system is in a legal state if and only if the topology of the system is the linear graph on the nodes of the system. The unique linear Graph G LIN is defined in Definition 14 and describes a sorted doubly-linked-list according to the total order on the process ids.
The topology of a configuration is the linear graph if and only if the configuration is a correct configuration as defined in 31. The correct configuration is unique up to structural congruence, the local state of the processes and the number of messages in the system as shown in Lemma 8. The closure property states whenever a correct configuration is reached, provided that no fault occurs, the system stays in a correct configuration. In order to prove the closure property of the algorithm, we have to show that whenever we have reached a correct configuration according to Definition 31 every possible step leads again to a correct configuration.

Theorem 1: Closure for Correct Configurations
Let A be a correct configuration then it holds for every reachable configuration C i. e., A � =⇒ C , that C is also a correct configuration.

Proof:
We prove this by induction over the step semantic i. e., every possible step leads again to a correct configuration. Let A ≡ Alg ges � P, P � , nb, Msgs, add � be the process term of an arbi- According to Lemma 8 it holds that P ∪ P � = P and P ∩ P � = �, Since ∀p ∈ P .nb(p) = {succ(p), pred(p)} ⊥ and the Definition of select (findLin ()) it holds that According to Corollary 2 there are (up to structural congruence) only the following steps possible: Since the only change in the configuration concerns the multiset of messages and nb(p) = {succ(p), pred(p)} ⊥ , it still holds that and therefore A � ≡ Alg ges � P, P � , nb, Msgs ∪ {( j , p)| j ∈ nb(p)}, add � is a correct configuration according to Lemma 8.
Let p ∈ P be an arbitrary process and q ∈ P with (p, q) ∈ Msgs. According to the assumptions it holds that q = succ(p) ∨ q = pred(p) and therefore Additionally with the assumptions it obviously holds that: Let p ∈ P � be an arbitrary process and q ∈ P with (p, q) ∈ add. According to the assumptions it holds that q = succ(p) ∨ q = pred(p) and therefore Additionally with the assumptions it obviously holds that: � is a correct configuration according to Lemma 8.

✷
In this section, we introduce three potential functions in order to show in Section 3.6 several convergence properties for our algorithm. The first function takes all connections between non-consecutive processes into account, the second only considers the closest neighbor to the left and the closest neighbor to the right, and the third is a combination of both.
The first potential function Ψ sums up the distances between all non-consecutive processes multiplied by the number of connections between them. Therefore, it sumps up the length of all non-correct edges in the topology with messages but takes also the number of connections that cause such an edge into account. For example, if process q ∉ {succ(p), pred(p)} is in the neighborhood of p and there are additionally three messages of the form p � q � , the length of edge (p, q) in the topology, and therefore the distance between p and q, is added four times in the potential function.

Definition 33: Potential Function Ψ p for Processes
Let p ∈ P be an arbitrary process and A be a process term of the algorithm according to be the multiset of all process ids that are sent to p but still in transit and not a desired neighbor and adding : (T × P ) → N with The potential function Ψ p : (T × P ) → N sums up the distances (with respect to the linear order ≤) of all outgoing connections of the process p while ignoring desired connections and is defined as follows:

Definition 34: Potential Function Ψ for Configurations
Let A be a process term of the algorithm according to Lemma 1. The potential function for configurations Ψ : T → N sums up the distances (with respect to the linear order ≤) between all the connections of processes while ignoring desired connections and is defined as: The potential function Ψ is therefore minimal if every connection in a configuration is between consecutive processes and there are no other connections between processes. This is only the case for a (weakly) connected topology if and only if the topology is the linear graph. Hence, the potential function is minimal for (undirected) correct configurations.

Lemma 14: Minimal Potential Ψ for (undirected) Correct Configurations
The potential function Ψ is minimal for a process term A ≡ Alg ges � P, P � , nb, Msgs, add � of the algorithm with a (weakly) connected (loop free) network topology iff A is an (undirected) correct configuration i. e., For every p, q ∈ P with p � = q it holds according to Definition 11 and 15 that and therefore according to Definitions 28 and 30 According to Definitions 15, 33 and 34 it then follows that Ψ(A � ) > 0.

✷
The potential function Ψ is monotonically decreasing with exception of sending keep-alive-messages to undesired neighbors and decreases with every linearization step as the new introduced connection is always strictly shorter than the removed one. Furthermore, it also decreases if an addition of an already known process is processed as the number of connections is then decreased by one. Whereby the sending, receiving and adding of desired process ids does not change anything as the potential function Ψ considers only the connections that still need to be removed.

Lemma 15: Progression of Ψ
Let A be an arbitrary configuration. For A � −→ A � it holds: an arbitrary process p ∈ P finds a left linearization step i. e., it then holds an arbitrary process p ∈ P finds a right linearization step i. e., it then holds or an arbitrary process p ∈ P � A adds an already known process that is not a desired neighbor to its neighborhood i. e., an arbitrary process p ∈ P sends keep-alive-messages to (a subset of) its desired neighbors i. e., an arbitrary process p ∈ P A receives a message i. e., an arbitrary process p ∈ P � A adds a former unknown process that is not a desired neighbor to its neighborhood i. e., it then holds an arbitrary process p ∈ P � A adds a desired neighbor to its neighborhood i. e., or an arbitrary process p ∈ P tries to find a linearization step and none of the other cases is true. It then holds A � ≡ A.
an arbitrary process p ∈ P sends keep-alive-messages not exclusively to its desired neighbors i. e., and therefore Ψ is monotone with exception of sending keep-alive-messages to undesired neighbors.

Proof:
According to Corollary 2 there are the following cases possible: Let p ∈ P be the executing process. The only change in the configuration concerns the multiset of messages and and therefore according to Definition Otherwise, there is at least one process q ∈ P with q ∉ {succ(p), pred(p)} and q ∈ nb A (p) and therefore according to Definition 33 and add A � = add A , according to Definition 33: and further with Definition 33 there are two cases. If k = succ( j ), then it holds according with Definition 33 that ∪ {k} since j < k and therefore also k � = pred( j ) according to Corollary 1. Hence, according to Definition 33 Since ≤ is according to Definition 11 a total order and j < k ∧ k < p, it follows with Definition 15 that dist(p, j ) > dist( j , k) and therefore according to Definition 34 it holds and further with Definition 33 If j � = pred(k), it holds that Rec(A � , k) = Rec(A, k) ∪ { j } since j < k and therefore also j � = succ(k) according to Corollary 1. Hence, according to Definition 33

Potential Functions
Since ≤ is according to Definition 11 a total order and j < k ∧ p < j , it follows with Definition 15 that dist(p, k) > dist(k, j ) and therefore according to Definition 34 it holds that Ψ(A � ) < Ψ(A).
Let p ∈ P A be the executing process with q ∈ P r ocs and (p, q) ∈ Msgs A . The only changes in the configuration that influence Ψ are According to Definition 33 it holds (as p ∈ P A and therefore add A (p) is not defined) that Otherwise q ∈ {succ(p), pred(p)} ⊥ and therefore according to • Let p ∈ P � A be the executing process and add A (p) = q. The only changes in the configuration that influence Ψ are add A � = add A \ {(p, q)} and nb A � . According to Definition 33 it holds that adding(A � , p) = 0 (as p ∈ P A � and therefore add A � is not defined). If q ∉ {succ(p), pred(p)}, it holds further according to Definition 33 that adding(A, p) = dist(p, q) and Rec(A � , p) = Rec(A, p) and since p � = q according to Definition 15 adding(A, p) = dist(p, q) > 0. Now there are two cases, q could be already in the neighborhood of p or not. If q ∈ nb A (p), then with q ∉ {succ(p), pred(p)} it follows Hence with Definition 33 Hence according to Definition 34 Ψ(A) = Ψ(A � ).

✷
The second potential function Ψ E considers the nearest left and the nearest right neighbor of a process while taking the messages in transit into account. The nearest left neighbor is the process with the greatest id in the left-neighborhood with messages, i. e., all processes with smaller ids to them the process has an edge in the topology with messages. The nearest right neighbor is defined correspondingly. The potential function Ψ E sums up the distances to the nearest neighbors with messages for all processes in the system while adding a value that is greater than any possible value for every process that does not have such a neighbor on one of the sides (and is not the smallest respectively greatest process).

Definition 35: Right-and Left-neighborhood with Messages
The left-neighborhood with messages of a process LeftNM : describes all left neighbors of a process in the directed topology with messages. Therefore, it contains all smaller processes to whom p has an outgoing connection.
The right-neighborhood with messages of a process RightNM : describes all right neighbors of a process in the directed topology with messages. Therefore, it contains all greater processes to whom p has an outgoing connection.

Definition 36: Nearest Neighbors of Process with Messages
The nearest left neighbor of a process ShortestLeftN : is the greatest process in the left-neighborhood with messages of a process provided the left-neighborhood is not empty. Therefore, it is the process on the end of the shortest outgoing edge on the left of p in the directed topology with messages.
The nearest right neighbor of a process ShortestRightN : is the smallest process in the right-neighborhood with messages of a process provided the right-neighborhood is not empty. Therefore, it is the process on the end of the shortest outgoing edge on the right of p in the directed topology with messages.

Definition 37: Potential Function Ψ E
The potential function of left neighbors for a process Ψ E (p)l : T × P → N with ShortestLeftN(A, p) returns the distance to the nearest left neighbor of a process while taking the messages that are still in transit into account. If the process does not have any smaller neighbors with messages (and is not the process with the minimum id) it returns a value that is greater than any possible value. Correspondingly, the potential function of right neighbors for a process Ψ E (p)r : returns the distance to the nearest right neighbor of a process while taking the messages that are still in transit into account. If the process does not have any greater neighbors with messages (and is not the process with the maximum id) it returns a value that is greater than any possible value. Therefore, the potential function of neighbors for a process Ψ E (p) : T × P → N with returns the sum of the distances to the nearest left and the nearest right neighbor of the process.
The potential function of neighbors for a configuration Ψ E : T → N with sums up all potential functions of neighbors for all processes in the configuration.
The potential function Ψ E is therefore minimal if every process, with exception of the smallest and greatest process, has a neighbor with messages on both sides and this neighbor is the nearest neighbor that is possible in the system. This is the case if it holds for every process that the predecessor is in the right-neighborhood with messages and the successor is in the left-neighborhood with messages. This holds if every correct edge is already established in the topology with messages and therefore the linear graph is a subgraph of the topology with

Lemma 16: Potential Ψ E Minimal for G LIN ⊆ NTM
Let A be an arbitrary configuration of the algorithm. Then Ψ E (A) is minimal if the desired topology is contained in the directed topology with messages i. e., Proof: It holds with Definitions 15, 35, 36 and 37 that Therefore, it follows with |P | = n that Ψ E (A) ≥ 2 · (n − 1) for an arbitrary configuration A.
If G LIN ⊆ NTM(A), it holds according to Definitions 14 and 28 that Hence with Definition 35 Therefore, with Definition 12, Corollary 1 and Definition 36 Hence with Definitions 15 and 37 it holds and therefore with |P | = n it holds that Ψ E (A) = 2 · (n − 1). If G LIN � ⊆ NTM(A), it holds according to Definitions 14 and 28 that and therefore with Definition 36 ShortestRightN(A, p) = q and according to Definition 35 q > p. Since q � = succ(p), it holds according to Corollary 1 and Definition 15 that dist(p, q) > 1 and therefore with Definition 37 Ψ E (p)r (A, p) > 1. Hence

✷
The potential function Ψ E is monotonically decreasing. The only steps that remove edges are linearization steps and they always remove the process that is further away. Since additionally no messages get lost, the nearest neighbor with message gets never removed. The function decreases whenever a connection is established to a process that is closer than all already known processes. This can happen through sending of keep-alive-messages or linearization steps.

Lemma 17: Progression Ψ E
Let A be an arbitrary configuration. For A � −→ A � holds: an arbitrary process p ∈ P finds a left linearization step and the greater process is nearer to the smaller process than every yet known right neighbor with messages i. e., an arbitrary process p ∈ P finds a right linearization step and the smaller process is nearer to the greater process than every yet known left neighbor with messages i. e., ∧ ∀q ∈ LeftNM (A, k) .q < j

it then holds
or if an arbitrary process p ∈ P sends keep-alive-messages and is a nearer neighbor for at least one of its (at most two) neighbors i. e., an arbitrary process p ∈ P A receives a message i. e., an arbitrary process p ∈ P � A adds a process to its neighborhood i. e., an arbitrary process p ∈ P finds a left linearization step but the smaller process has already a nearer right neighbor with messages than the greater process i. e., an arbitrary process p ∈ P finds a right linearization step but the greater process has already a nearer left neighbor with messages than the smaller process i. e., if an arbitrary process p ∈ P sends keep-alive-messages and every neighbor already knows with messages a nearer process i. e., or an arbitrary process p ∈ P tries to find a linearization step and none of the other cases is true. It then holds A � ≡ A.
and therefore Ψ E is monotonically decreasing.

Proof:
According to Corollary 2 there are the following cases possible: • If a process p ∈ P tries to find a linearization step but select Therefore, with Definition 37 if for all processes q ∈ RightNM � A, j � it holds that p < q, then it follows with Definition 36 Let r be the process with ShortestRightN(A, j ) = r . Since j < p < r , it holds according to Definition 15 dist( j , p) < dist( j , r ) and therefore with Definition 37 Therefore, with Definition 37 if there is a process q ∈ RightNM � A, j � with q ≤ p, then it holds according to Definition 36 that According to the definition of Hence with Definition 37 Therefore, with Definition 37 if for all processes q ∈ LeftNM (A, k) it holds that q < p, then it follows with Definition 36 Let r be the process with ShortestLeftN(A, k) = r . Since r < p < k, it holds according to Definition 15 dist(k, p) < dist(k, r ) and therefore with Definition Therefore, with Definition 37 if there is a process q ∈ LeftNM (A, k) with p ≤ q, then it holds according to Definition 36 that Let j be the process with LeftN � nb A (p), p � = { j } and let k be the process with It holds that either Therefore The proof is similar to the proofs in the previous cases.
• If a process p ∈ P finds a left linearization step i. e., select Since j < p and k < p and j , k ∈ nb A � (p), it holds according to the definition of LeftN that and There are the following cases for Ψ E (p) (A � , j ) since with j < k it holds j � = max (P ): Hence with Definition 37 Therefore, with Definition 37 if for all processes q ∈ RightNM � A, j � it holds that k < q, then it follows with Definition 36 Let r be the process with ShortestRightN(A, j ) = r . Since j < k < r , it holds according to Definition 15 dist( j , k) < dist( j , r ) and therefore with Definition 37 Therefore, with Definition 37 then it holds according to Definition 36 that • If a process p ∈ P finds a right linearization step i. e., select Since j < k and p < j and j , k ∈ nb A � (p), it holds according to the definition of RightN Hence with Definition 35 also min Therefore, with Definition 37 it holds that q < j , then it follows with Definition 36 Let r be the process with ShortestLeftN(A, k) = r . Since r < j < k, it holds according to Definition 15 dist(k, j ) < dist(k, r ) and therefore with Definition 37 Therefore, with Definition 37 it holds according to Definition 36 that Therefore, with Definition 37 Ψ E (p) (A � , k) = Ψ E (p) (A, k) and hence • If for a process p ∈ P it could be that select • If a process p ∈ P A receives a message with the id of q ∈ P i. e., (p, q) ∈ Msgs A , it holds  (A, p) and • If a process p ∈ P � A adds a process q ∈ P to its neighborhood i. e., (p, q) ∈ add A it holds that Ψ E (R) ≤ Ψ E (A) and therefore Ψ E is monotonically decreasing.
The third potential function Ψ � is the weighted sum and therefore a combination of the other two functions. Therefore, the potential function Ψ � is minimal if both composite potential functions Ψ and Ψ E are minimal. This is the case if the topology with messages is the linear graph. The functions are weighted in a way that Ψ � decreases with every linearization step and whenever a process gets to know a closer process than every yet known neighbor with messages on this side. The sending of keep-alive-messages to undesired neighbors gets compensated by establishing a connection to a nearer process. Therefore, whenever a process sends keep-alive-messages it holds that if at least one of the at most two receiving processes gets to know a nearer process, the potential function decreases. The potential function is monotonically decreasing with exception of sending keep-alive-messages to undesired neighbors that already have nearer neighbors.

Definition 38: Potential Ψ �
The potential sumfunction of a configuration Ψ � : T → N with is the weighted sum of the potential function of neighbors Ψ E and the potential function for configurations Ψ.
an arbitrary process p ∈ P finds a left linearization step i. e., and it holds that an arbitrary process p ∈ P finds a right linearization step i. e., and it holds that or an arbitrary process p ∈ P sends keep-alive-messages and is a nearer neighbor for at least one of its (at most two) neighbors i. e., an arbitrary process p ∈ P A receives a message i. e., an arbitrary process p ∈ P � A adds a process to its neighborhood i. e., q ∈ P ∧ add A (p) = q and it holds that an arbitrary process p ∈ P sends keep-alive-messages exclusively to (a subset of) desired neighbors and is already with messages known by them i. e., or an arbitrary process p ∈ P tries to find a linearization step and none of the other cases is true. It then holds A � ≡ A.

Potential Functions
an arbitrary process p ∈ P sends keep-alive-messages and every neighbor already knows with messages a nearer process i. e., and therefore Ψ � is monotonically decreasing with exception of sending keep-alive-messages to undesired neighbors that already have nearer neighbors. Proof: • If a process p ∈ P tries to find a linearization step but select According to Lemma 6 it holds that p has at most two neighbors and * if p will be a nearer right neighbor than all yet from j known processes in the topology with messages i. e., it holds that RightNM  dist( j , p). In both cases, it holds that Ψ(A � ) ≤ Ψ(A) + maxdist. According to Lemma 17 it holds that Ψ(A � ) < Ψ(A). Therefore, with Definition 38  * if p will be a nearer left neighbor than all yet from k known processes in the topology with messages i. e., it holds that LeftNM (A, k) = � ∨ � LeftNM (A, k) � = � ∧ ∀q ∈ LeftNM (A, k) .q < p � : It holds * if p is a desired neighbor of k but already known in the topology with messages i. e., p = pred(k) ∧ p ∈ LeftNM (A, k): It holds that * if k already has a closer right neighbor than p in the topology with messages i. e., p � = pred(k) ∧ ∃q ∈ LeftNM (A, k) .p ≤ q: It holds The proofs are similar to the previous case. * if at least one of the processes gets to know a nearer process i. e., * if p is a desired neighbors of both but already known i. e., According to Lemma 15 it holds that Ψ(A � ) = Ψ(A) and according to Lemma 15 it holds that Ψ E (A � ) = Ψ E (A). Therefore, with Definition 38 it holds that * if both processes already know a closer process i. e., • If a process p ∈ P finds a left linearization step i. e., select According to Lemma 15 it holds that Ψ(A � ) < Ψ(A) and according to Lemma 17 Ψ E (A � ) ≤

Ψ E (A). Hence with Definition 38 it holds that
• If a process p ∈ P finds a right linearization step i. e., select � findLin According to Lemma 15 it holds that Ψ(A � ) < Ψ(A) and according to Lemma 17 Ψ E (A � ) ≤

Ψ E (A). Hence with Definition 38 it holds that
• If for a process p ∈ P it could be that select • If a process p ∈ P A receives a message with the id of q ∈ P i. e., (p, q) ∈ Msgs A : it holds According to Lemma 15 it holds that Ψ(A � ) = Ψ(A) and according to Lemma 17 Ψ E (A � ) =

Ψ E (A). Hence with Definition 38 it holds that
• If a process p ∈ P � A adds a process q ∈ P to its neighborhood i. e., (p, q) ∈ add A : it holds

Convergence
In this section, we prove strong convergence for two special cases and weak convergence, i. e., for every arbitrary initial configuration there exist executions that reach a correct configuration, in the general case. Strong convergence is proven in case that either there are possibly correct edges missing but no non-correct edges existent in the topology with messages i. e., the topology is a subgraph of the linear graph, or there are possibly still non-correct edges existent but at least all correct edges are contained in the topology with messages i. e., the linear graph is a subgraph of the topology.
In case that there are only correct edges missing, the system converges to a correct configuration as between every pair of consecutive processes there is at least one connection. Therefore, no more possible linearization steps exist and every process sends keep-alive-messages to the already known subset of desired neighbors. All these messages are received and processed eventually and therefore all missing correct edges are eventually established.

Lemma 20: Convergence for UNTM = UG LIN
Let A ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary configuration of the algorithm according to

Proof:
Since UNTM(A) = UG LIN , it holds according to Definition 32 that A is an undirected correct configuration and therefore according to Lemma 9 that: P ∪ P � = P and P ∩ P � = �, ∀p ∈ P .nb(p) ⊆ {succ(p), pred(p)} ⊥ , ∀(p, q) ∈ Msgs.(q = succ(p)) ∨ (q = pred(p)), ∀p ∈ P � .(add(p) = succ(p)) ∨ (add(p) = pred(p)) and Otherwise we can show that if U (A) � = �, then |U (A)| ≤ P will always eventually decrease. Therefore, a correct configuration will be reached after a finite number of steps since every process in U adds the missing desired neighbor(s) after a finite number of steps.
Let p ∈ U (A) be an arbitrary process with succ(p) ∈ P and succ(p) ∉ nb(p). We have to show that after a finite number of steps an undirected correct configuration C � is reached with succ(p) ∈ nb C � (p). According to the assumption at least one of the following cases is true: • p ∈ P � ∧ add(p) = succ(p): Then it holds that the subprocess Alg add � p, succ(p) � is enabled and according to Lemma 3 it stays enabled until it executes a step. According to the fairness assumption 3 will execute a step after a finite number of steps. Let R be the configuration before this step. Then it holds according to Corollary 2 and therefore succ(p) ∈ nb C � (p). According to Corollary 11 it holds C � is an undirected correct configuration i. e., UNTM(C � ) = UG LIN and with succ(p) ∉ nb(p) and succ(p) ∈ nb C � (p) that UNT(A) ⊂ UNT(C � ).
• (p, succ(p)) ∈ Msgs: According to the Assumption 2 that there is no message loss, the message will be eventually (after a finite number of steps) received. According to Lemma 2, p is the only process that can receive this message. Let R be the configuration before this step. Then it holds according to Corollary 2 R � −→ R � with R � ≡ Alg ges � P R \ {p}, P � R ∪ {p}, nb R , Msgs R \ {(p, succ(p))}, add R ∪ {(p, succ(p))} � and therefore p ∈ P � R � and add R � (p) = succ(p). According to Corollary 11 it holds that R � is an undirected correct configuration i. e., UNTM(R � ) = UG LIN and UNT(A) ⊆ UNT(R � ). Therefore, we reduced the problem to the previous case.
• p ∈ nb(succ(p)): According to to Lemma 3 the subprocess Alg match � succ(p) � is enabled and stays enabled until it executes a step. According to the fairness assumption 3, Alg match � succ(p) � will execute a step after a finite number of steps. Let R be the configuration before this step. Since R has to be an undirected correct configuration according to Lemma 13, it holds that nb R (succ(p)) ⊆ {succ(succ(p)), pred(succ(p))} ⊥ = {succ(succ(p)), p} ⊥ and therefore select � findLin � succ(p), nb R succ(p) �� = ⊥ and according to Corollary 2 with R � ≡ Alg ges � P R , P � R , nb R , Msgs R ∪ {( j , succ(p))| j ∈ nb R (succ(p))}, add R � and therefore (p, succ(p)) ∈ Msgs R � . According to Corollary 11 it holds that R � is an undirected correct configuration i. e., UNTM(R � ) = UG LIN and UNT(A) ⊆ UNT(R � ). Therefore, we reduced the problem to the previous case.
• succ(p) ∈ P � ∧ add(succ(p)) = p: Then it holds that the subprocess Alg add � succ(p), p � is enabled and according to Lemma 3 it stays enabled until it executes a step. According to the fairness assumption 3 will execute a step after a finite number of steps. Let R be the configuration before this step. Then it holds according to and therefore p ∈ nb R � (succ(p)). According to Corollary 11 it holds that R � is an undirected correct configuration i. e., UNTM(R � ) = UG LIN and UNT(A) ⊆ UNT(R � ). Therefore, we reduced the problem to the previous case.
• (succ(p), p) ∈ Msgs: According to the Assumption 2 that there is no message loss, the message will be eventually (after a finite number of steps) received. According to Lemma 2, succ(p) is the only process that can receive this message. Let R be the configuration before this step. Then it holds according to and therefore succ(p) ∈ P � R � and add R � (succ(p)) = p. According to Corollary 11 it holds that R � is an undirected correct configuration i. e., UNTM(R � ) = UG LIN and UNT(A) ⊆ UNT(R � ). Therefore, we reduced the problem to the previous case.

✷
In case that there are possibly too many edges in the topology but at least all correct edges are already established i. e., the linear graph is a subgraph of the topology, the system also converges to a correct configuration. In this case, the only processes that can send keep-alivemessages are processes that know exactly their desired neighbors. This holds as every process knows at least its desired neighbors and whenever a process has additionally neighbors, there is a possible linearization step that can be executed by the process. Therefore, with every linearization step the topology gets closer to the desired topology. This is shown via the potential function Ψ. Otherwise it holds that Ψ(A) > 0 but the potential function will decrease over the execution and eventually it holds that a configuration C is reached i. e., A � =⇒ C with Ψ(C ) = 0. This follows from the two observations that the potential function can not increase for a process term whose network topology graph contains the desired graph and if the term is not a correct configuration there will always eventually steps executed which decrease the potential function strictly.

Convergence
Therefore, first, for every reachable configuration R with A � =⇒ R � it holds that According to Lemma 15 the only case with Ψ(R � ) > R would be if a process sends keep-alivemessages to processes that are not its desired neighbors i. e., there is p, q ∈ P with select � findLin � p, nb R (p) �� = ⊥, q ∉ {succ(p), pred(p)} and q ∈ nb R (p) and the executed Second, for every reachable configuration R with A � =⇒ R and Ψ(R) > 0 there is always eventually a configuration R � reached i. e., R � =⇒ R � with According to Definitions 33 and 34 and Ψ(R) > 0 it holds that there is are processes p, q ∈ P with p � = q and q ∉ {succ(p), pred(p)} and one of the following cases is true: • q ∈ nb R (p)): According to to Lemma 3 the subprocess Alg match � p � is enabled and stays enabled until it executes a step. According to the fairness assumption 3 Alg match � p � will execute a step after a finite number of steps. Let H be the configuration before this step. It holds according to Corollary 10 that G LIN ⊆ NT(H ) and therefore with Definitions 14 and 27 that {succ(p), pred(p)} ⊥ ⊆ nb H (p). Since p � = q and q ∉ {succ(p), pred(p)}, it holds according to Corollary 1 that pred(p) < q ∨ q > succ(p). Therefore, it follows with the definition of select (findLin ()) that there has to be an enabled linearization step for p and hence either select From the monotonicity of the potential function it follows that Ψ(H ) ≤ Ψ(R) and hence Ψ(R � ) < Ψ(R).
• p ∈ P � R ∧ add R (p) = q: Then it holds that the subprocess Alg add � p, q � is enabled and according to Lemma 3 it stays enabled until it executes a step. According to the fairness assumption 3 will execute a step after a finite number of steps. Let H be the configuration before this step. Then it holds according to Corollary 2 and hence q ∈ nb H � (x) and according to the monotonicity Ψ(H � ) ≤ Ψ(R). Therefore, we can reduce the problem to the previous case.
• (p, q) ∈ Msgs R : According to the Assumption 2 that there is no message loss, the message will be eventually (after a finite number of steps) received. According to Lemma 2, p is the only process that can receive this message. Let H be the configuration before this Therefore, we will eventually reach a configuration C i. e., A � =⇒ C with Ψ(C ) = 0. According to Corollary 10 it holds that G LIN ⊆ NTM(C ) ∧ G LIN ⊆ NT(C ) and therefore with Ψ(C ) = 0 as shown in the base case NTM(C ) = G LIN ∧ NT(C ) = G LIN .

✷
Convergence also holds if the desired topology is a subgraph of the topology with messages. Since every message that is in transit will eventually be received and processed, we always reach a configuration for that holds that the linear graph is a subgraph of the topology without messages. Then according to the last lemma, we always reach a correct configuration.

Lemma 22: Convergence for G LIN ⊆ NTM
Let A be an arbitrary configuration of the algorithm according to Lemma 1. If G LIN ⊆ NTM(A), then a correct configuration C is reached after a finite number of steps i. e., Otherwise we can show that if U (A) � = �, then |U (A)| ≤ P will always eventually decrease. Let p ∈ U (A) be an arbitrary process with succ(p) ∈ P and succ(p) ∉ nb A (p). We have to show that after a finite number of steps configuration C � is reached with G LIN ⊆ NTM(C � ) and succ(p) ∈ nb C � (p). According to the assumption that G LIN ⊆ NTM(A) at least one of the following cases is true according to Definition 28: According to Lemma 4 it is a configuration C � reached with succ(p) ∈ nb C � (p). According to Lemma 12 it holds with Definitions 14 and 28 that G LIN ⊆ NTM(C � ) and with Lemma 11 and succ(p) ∉ nb A (p) and succ(p) ∈ nb C � (p) that U (A) ⊂ U (C � ).
• (p, succ(p)) ∈ Msgs: According to Corollary 4 it is a configuration C � reached with succ(p) ∈ nb C � (p). According to Lemma 12 it holds with Definitions 14 and 28 that G LIN ⊆ NTM(C � ) and with Lemma 11 and succ(p) ∉ nb A (p) and succ(p) ∈ nb C � (p) that The case for pred(p) ∈ P and pred(p) ∉ nb A (p) is similar. Therefore, we will always reach a configuration C �� with G LIN ⊆ NTM(C �� ) and |U (A)| < |U (C �� )|. Hence eventually a configuration R is reached with |U (R)| = 0 and therefore according to the base case G LIN ⊆ NTM(R) ∧ G LIN ⊆ NT(R). Therefore, according to Lemma 21 it holds that Therefore, we proved strong convergence for the special cases that there are only correct edges missing, i. e., the topology is a subgraph of the linear graph, and that there are only too many edges i. e., the linear graph is a subgraph of the topology (with messages). The proofs for both cases use the fact that keep-alive-messages are only exchanged between desired neighbors. However, proving strong convergence in the general case is much more difficult as the sending of keep-alive-messages to undesired neighbors can cause the reestablishing of connections that were already removed through linearization steps and should stay removed. This is explained in more detail in the Chapter 4. Therefore, we show weak convergence in the general case i. e., for every initial configuration there are executions that converge to a correct configuration. In order to prove weak convergence for any arbitrary configuration, we define a perfect oracle. A perfect oracle is a global omniscient instance that suppresses the sending of all keep-alive-messages with exception of keep-alive-messages that are necessary to resolve potential deadlocks. More concrete, whenever the system would deadlock without the sending of keep-alive-messages, in the sense that there are possible linearization steps in the undirected topology with messages but not in the directed topology with messages, the perfect oracle chooses processes that are allowed to send keep-alive-messages once, in order to resolve the deadlock. Example situations are depicted in Figure 3. 3. A perfect oracle cannot be implemented in a distributed system and should therefore only be seen as a restriction on the set of executions. The sending is executed as recently as all corresponding neighborhood relations are established. Therefore, in the first line of Figure 3.3 keep-alive-messages can be send, but in the second one only after the system converged to the first line (i. e., after all messages are received and processed eventually).

Definition 39: Perfect Oracle O
A perfect oracle is a global omniscient instance that only let the processes send keep-alivemessages to resolve deadlocks and otherwise suppresses all keep-alive-messages . Therefore, whenever there is a linearization step in the directed topology with messages in a configuration A i. e., then no process is allowed to send keep-alive-messages i. e., for every process If there is a possible linearization step in the undirected topology with messages i. e., but there is no possible linearization step in the directed topology with messages i. e., the perfect oracle O will choose one respectively two processes and allow them to send keep-alive-messages once in order to resolve the potential deadlock. If it is sufficient that one process sends keep-alive-messages i. e., then O chooses one process q ∈ P such that there are p, r ∈ P and (p < q ∧q < r )∨(r < q ∧q < p)∨(p < r ∧r < q)∨(q < r ∧r < p) and (p, r ) ∈ E NTM(A) ∧(q, p) ∈ E NTM(A) , and allows q to send keep-alive-messages once as soon as a configuration C is reached with r ∈ nb C (p)∧p ∈ nb C (q).
Otherwise it is necessary that two processes send keep-alive-messages in order to resolve the potential deadlock i. e., O chooses two processes q, r ∈ P such that there is p ∈ P and (p < q ∧ q < r ) ∨ (r < q ∧ q < p) and (q, p) ∈ E NTM(A) ∧ (r, p) ∈ E NTM(A) . Then O allows q and r to send keep-alive-messages once as soon as a configuration C is reached with p ∈ nb C (q) ∧ p ∈ nb C (r ). If there is no more possible linearization step in the undirected topology with messages i. e., and therefore UNTM(A) ⊆ UG LIN , then all processes are allowed to send keep-alive-messages .

Remark: A perfect oracle O is not contradictory to the fairness assumption 3 if starting from any initial configuration in every execution after a finite number of steps a configuration is reached
where O does not suppress the sending of keep-alive-messages anymore. In this case, it is possible that every continuously enabled subprocess can execute a step after a finite number of steps. We show in Lemma 23 that starting from an arbitrary initial configuration a correct configuration is reached after a finite number of steps. A perfect oracle O does not suppress the sending of keep-alive-messages in a correct configuration. Once the system is in a correct configuration, it stays in a correct configuration according to the closure property as shown in Theorem 1. Therefore, a perfect oracle is not contradictory to the fairness assumption.
We show that every execution that is admissible under the restriction of a perfect oracle converges to a correct configuration. Since for every configuration this set of executions is nonempty, we prove weak convergence for the general case. We have introduced three potential functions and shown that whenever at least one of them is minimal, the system reaches a correct configuration in a finite number of steps. For every configuration there is exactly one of the three cases true: there is no more possible linearization step in the undirected topology with messages, there is a possible linearization step in the directed topology with messages, or there is a possible linearization step in the undirected but not in the directed topology with messages. In the first case, it follows that Ψ is minimal and therefore strong convergence is ensured. In the second case, the perfect oracle precludes the sending of keep-alive-messages and therefore all three potential functions behave monotonically decreasing. Furthermore, with every executed linearization step Ψ � and Ψ are strictly decreasing. In the third case, the perfect oracle allows chosen processes to send keep-alive-messages in order to resolve the potential deadlock and this leads to an increasing of Ψ and possibly also Ψ � . Nevertheless, Ψ E is still monotonically decreasing and we always reach a configuration with a strictly smaller value of Ψ E and Ψ � such that there is a possible linearization step in the directed topology with messages. Hence, the third case can not occur more often than the initial value of Ψ E without Ψ E getting minimal, as Ψ E is monotonically in every case and strictly decreases with every occurrence of the third case. Therefore, neither we can stay infinite long in the second case nor we can infinitely often alternate between the second and the third case without reaching a configuration in which at least one of the three potential functions is minimal and therefore convergence ensured.

Lemma 23: Convergence with Perfect Oracle
Let I ≡ Alg ges � P, P � , nb, Msgs, add � be an arbitrary connected, i.
Otherwise it holds that Ψ � (A) > 2 · n · (n − 1) but the potential functions will decrease over the execution and eventually it holds that a configuration C � is reached i. e., and Ψ � (R) > 2 · n · (n − 1) where there is still a possible linearization step in the directed topology with messages i. e., ∃p, q, r ∈ P .
and there is always eventually a configuration S reached i. e., R � =⇒ S with Since there is a perfect oracle and there is a possible linearization step in the directed topology with messages i. e., ∃p, q, r ∈ P .((p < q ∧ q < r ) ∨ (r < q ∧ q < p)) ∧ ((p, q) ∈ E NTM(R) ∧ (p, r ) ∈ E NTM(R) ), it holds that no process can send keep-alive-messages according to 39. Therefore, it is not possible that a process p executes a step with select According to Lemmata 19, 17 and 15 it holds therefore that ∀R � Assume p < q ∧ q < r (the proof for r < q ∧ q < p is similar). Furthermore, assume that in every of the below reached configurations R � i. e., R � =⇒ R � the neighborhood of p has only grown i. e., nb R (p) ⊆ nb R � (p), otherwise according to Lemma 10 there has to be intermediate configuration S such that the subprocess Alg match � p � executes a step and select � findLin , but then p exe-cutes a linearization step in S and according to Lemmata 15,19 and 17 . According to Definition 28 there are the following cases: • Both processes are in the neighborhood of p: it holds q, r ∈ nb R (p). According to Lemma 3 the subprocess Alg match � q � is enabled in R and stays enabled until it executes a step. According to the fairness assumption 3 Alg match � q � will execute a step after a finite number of steps. Let R � be the configuration before this step. Since up to this point there was at least one possible linearization step in the directed topology with messages, it holds that Since Alg match � q � does not executed a step it holds according to Lemma 10 that nb R � (p) ⊇ nb R (p) and therefore q, r ∈ nb R � (p). Hence with p < q ∧ p < r and the definition of RightN it holds that |nb • There is just an add-step necessary to enable the linearization step: According to Lemma 4 there is a configuration R � reached with r ∈ nb R � (p). According to the assumptions it holds that q ∈ nb R � (p) and p < q ∧ q < r . Therefore, we reduced the problem to the previous case.
• There is just one message left to receive: assume q ∈ nb R (p)∧(p, r ) ∈ Msgs R . According to Corollary 4 we reach a configuration R � with r ∈ nb R � (p). According to the assumptions it holds that q ∈ nb R � (p) and p < q < r . Therefore, we reduced the problem to the first case. The case (p, q) ∈ Msgs R ∧ r ∈ nb R (p) is similar.
• There is an add-step necessary and a message left to receive: assume � p ∈ P � R ∧ add R (p) = q � ∧ (p, r ) ∈ Msgs R . According to Lemma 4 there are config- and q ∈ nb C � (p). Up to this point p cannot receive any message as the subprocess Alg rec � p � is not enabled as long as Alg add � p, q � is enabled and according to 2 messages cannot get lost and according to Lemma 2 p is the only process that can receive this message. Therefore, it holds that (p, r ) ∈ Msgs C � . According to Corollary 4 a configuration R � is reached with r ∈ nb R � (p). According to the assumptions it holds that q ∈ nb R � (p) ⊇ nb C � (p) and p < q < r . Therefore, we reduced the problem to the first case.
The case for (p, q) ∈ Msgs R ∧ � p ∈ P � R ∧ add R (p) = r � is similar.
• There are two messages left to receive: (p, q) ∈ Msgs R ∧ (p, r ) ∈ Msgs R . According to Corollary 4 a configuration C is reached with q ∈ nb C (p) and a configuration C � is reached with r ∈ nb C � (p) and either R � =⇒ second case is similar). Then according to the assumptions nb C (p) ⊆ nb C � (p) and therefore q, r ∈ nb C � (p) and p < q < r . Therefore, we reduced the problem to the first case.
Assume first, there is never a configuration D reached i. e., A � =⇒ D that has a deadlock in the sense that there is a possible linearization step in the undirected network topology with message i. e., ∃p, q, r ∈ P .{p, q}, {p, r } ∈ E UNTM(D) ∧ ((p < q ∧ q < r ) ∨ (r < q ∧ q < p)) but no possible linearization step in the directed topology with messages i. e., ∀p, q, r ∈ P .
Since there is a perfect oracle, it holds that the potential function can not increase and if the configuration is not an (undirected) correct configuration, there are always eventually steps executed which decrease the potential functions strictly as shown before. Therefore, we eventually reach a configuration . As shown in the base case it holds then for C � that Assume a configuration D is reached where there is no possible linearization step in the directed topology with messages i. e., ∀p, q, r ∈ P .((p < q∧p < r )∨(q < p∧r < p)) =⇒ ((p, q) ∉ E NTM(D) ∨ (p, r ) ∉ E NTM(D) ) but still a possible linearization step in the undirected topology with messages i. e., ∃p, q, r ∈ P .{p, q}, {p, r } ∈ E UNTM(D) ∧ ((p < q ∧ q < r ) ∨ (r < q ∧ q < p)). If there would be no possible linearization step in the undirected topology with messages i. e., it holds that UNTM(D) = UG LIN according to Lemma 7 and I � =⇒ D whereby I is a connect initial configuration. Therefore, according to Lemma 14 it holds that Ψ(D) = 0 and as shown in the base case it holds that D is an undirected correct configuration and Hence Ψ(D) > 0 and therefore Ψ � (D) > 2 · n · (n − 1). We show that a configuration D �� is reached where again at least one linearization step in the directed topology with messages is possible and Now the perfect oracle O allows to send keep-alive-messages. There are two cases. It is either sufficient that one process is sending keep-alive-messages or there are two process that have to send keep-alive-messages to resolve the deadlock. For the first case, it holds � and r respectively q is the process that is allowed to send keep-alive-messages by O as soon as it knows p and p knows the other process. Assume p < q ∧ q < r (the proof for r < q ∧ q < p is similar).
Furthermore, assume that in every of the below reached configurations R i. e., D � =⇒ R the neighborhood of p � ∈ {p, q, r } has only grown i. e., nb D (p � ) ⊆ nb R (p � ), otherwise according to Lemma 10 there has to be an intermediate configuration S in which the subprocess Alg match � p � � executes a step and select � findLin , but then p � executes a linearization step in S which is a contradiction to the assumption that there is no possible linearization step in the directed topology with messages and this can only be resolved by sending keep-alive-messages as all possible steps are receiving messages that are already in transit and the addition of previously received process ids to the neighborhood. According to Definition 28 there are the following cases: • p has one process in its neighborhood and the other process has p in its neighborhood: There are two cases q ∈ nb D (p) ∧ p ∈ nb D (r ) or p ∈ nb D (q) ∧ r ∈ nb D (p).
If q ∈ nb D (p) ∧ p ∈ nb D (r ) and r is the process that is allowed to send keep-alive-messages by O, it holds according to Lemma 3 the subprocess Alg match (r ) is enabled in D and stays enabled until it executes a step. According to the fairness assumption 3 Alg match (r ) will execute a step after a finite number of steps and O allows r to send keep-alive-messages according to the assumptions. Let D � be the configuration before this step. It holds according to Lemmata 19,15 and 17 Ψ E (D) since up to D � no process was allowed to send keep-alive-messages. It holds select (findLin (r, nb D � (r ))) = ⊥ (otherwise there would be a possible linearization step for r which is contradictory to the deadlock assumption). According to Corollary 2 it holds According to the assumptions nb D (r ) ⊆ nb D � (r ). Therefore, it holds (p, r ) ∈ Msgs E . With p < q < r and q ∈ nb E (p) ⊇ nb D (p) it holds with Definition 35 that RightNM

Convergence
Msgs E , we will according to Corollary 4 reach a configuration G with r ∈ nb G (p). According to the assumption it holds q ∈ nb G (p) ⊇ nb D (p). Since no other process was allowed to send keep-alive-messages by O and until now there was no enabled linearization step it holds nb G (p) = {q, r } and this remains unchanged until p executes the linearization step. Therefore, according to Lemma 3 the subprocess Alg match � p � is enabled in G and stays enabled until it executes a step. According to the fairness assumption 3 Alg match � p � will execute a step after a finite number of steps. Let G � be the configuration before this step. Since up to this point there was one possible linearization step in the directed topology with messages, it holds that Since q < r and p < q, it holds with Corollary 2 that Hence with Lemma 15 it holds Ψ(D �� ) < Ψ(G � ). It holds with the assumptions that p ∈ nb D (r ) ⊇ nb G � (r ) and with p < r and Definition 35 therefore that LeftNM With Ψ(D �� ) < Ψ(G � ) and Definition 38 it holds Therefore, with LeftNM � D �� , r � = {p, q} it holds that there is a possible linearization step in the directed topology with messages of D �� and If |nb D � (r )| = 2 ∧ RightN (nb D � (r ), r ) = 1 ∧ LeftN (nb D � (r ), r ) = 1, it holds that there is a process s ∈ P with RightN � D � r, r � = {s} and hence (s, r ) ∈ Msgs E . There are two cases.
and hence E is the searched configuration D �� itself.
. Since (p, r ) ∈ Msgs E , we reach according to Corollary 4 a configuration G with r ∈ nb G (p). With (s, r ) ∈ Msgs E and LeftNM � D � , s � = {q � } we reach with Definition 35, Lemma 4 and Corollary 4 a configuration G � with {r, q � } ⊆ nb G � (s). Therefore, according to Lemma 3 the subprocess Alg match � p � is enabled in G and the subprocess Alg match (s) is enabled in G � and they stay enabled until they each execute a step. According to the fairness assumption 3, Alg match � p � executes a step after a finite number of steps. Let H be the configuration before this step. Additionally, according to the fairness assumption 3, Alg match (s) executes a step after a finite number of steps. Let H � be the configuration before this . Therefore, with the assumptions it holds that q ∈ nb H (p) ⊇ nb D (p). Since no other process was allowed to send keep-alive-messages by O and until now there was no other enabled linearization step that included p it holds nb H (p) = {q, r }. Since up to this point there was one possible linearization step in the directed topology with messages it holds that Since nb H (p) = {q, r } and p < q < r , it holds with the definition of select (findLin ()) that select � findLin � p, nb H (p) �� = (q, r ). Since q < r and p < q, it holds with Corollary 2 that it holds that there is a possible linearization step in the directed topology with messages of D �� and If p ∈ nb D (q) ∧ r ∈ nb D (p) and q is the process that is allowed to send keep-alive-messages by O it holds according to Lemma 3 the subprocess Alg match � q � is enabled in D and stays enabled until it executes a step. According to the fairness assumption 3, Alg match � q � executes a step after a finite number of steps and O allows q to send keep-alive-messages according to the assumptions. Let D � be the configuration before this step. It holds according to Lemmata 19,15 and 17 since up to D � no process was allowed to send keep-alive-messages . It holds select � findLin � q, nb D � (q) �� = ⊥ (otherwise there would be a possible linearization step for q which is contradictory to the deadlock assumption). According to Corollary 2, it holds According to the assumptions nb D (q) ⊆ nb D � (q). Therefore, it holds (p, q) ∈ Msgs D �� . Additionally also nb D (p) ⊆ nb D � (p) ⊆ nb D �� (p) and therefore r ∈ nb D � (p) and r ∈ nb D �� (p).
• p has one process in its neighborhood and for the other process is an add-step necessary: . According to Lemma 4 there is a configuration E reached with p ∈ nb E (r ). According to the assumptions it holds that q ∈ nb E (p) ⊇ nb D (p). Hence, we reduced the problem to the previous case.
• p has one process in its neighborhood and the other process has a message left to receive: assume q ∈ nb D (p)∧(r, p) ∈ Msgs D . According to Corollary 4 we reach a configuration E with p ∈ nb E (r ). According to the assumptions it holds that q ∈ nb E (p) ⊇ nb D (p). Hence, we reduced the problem to the first case.
The proof for (q, p) ∈ Msgs D ∧ r ∈ nb D (p) is similar.
• One process has p in its neighborhood and for p is an add-step necessary: . According to Lemma 4 there is a configuration E reached with q ∈ nb E (p). According to the assumptions it holds that p ∈ nb E (r ) ⊇ nb D (r ). Hence, we reduced the problem to the first case.
The proof for p ∈ nb D (q) ∧ � p ∈ P � D ∧ add D (p) = r � is similar.
• One process has p in its neighborhood and for p is a message left to receive: assume (p, q) ∈ Msgs D ∧ p ∈ nb D (r ). According to Corollary 4 we reach a configuration E with q ∈ nb E (p). According to the assumptions it holds that p ∈ nb E (r ) ⊇ nb D (r ). Hence, we reduced the problem to the first case. The proof for p ∈ nb D (q) ∧ (p, r ) ∈ Msgs D is similar.
• There are two add-steps necessary: assume . According to Lemma 4 there is a configuration E reached with q ∈ nb E (p) and a configuration E � is reached with the second case is similar). Then according to the assumptions nb E (p) ⊆ nb E � (p) and therefore q ∈ nb E � (p). Hence, we reduced the problem to the first case. The proof for • There is an add-step necessary and a message left to receive: assume � p ∈ P � D ∧ add D (p) = q � ∧ (r, p) ∈ Msgs D . According to Lemma 4 there is a configuration E reached with q ∈ nb E (p) and according to Corollary 4 a configuration E � with case is similar). Then according to the assumptions nb E (p) ⊆ nb E � (p) and therefore

Convergence
q ∈ nb E � (p). Hence, we reduced the problem to the first case.
The proof for (q, p) ∈ Msgs D ∧ � p ∈ P � D ∧ add D (p) = r � is similar and the proofs for (p, q) ∈ with switched roles.
• There are two messages left to receive: assume (p, q) ∈ Msgs D ∧ (r, p) ∈ Msgs D . According to Corollary 4 there is a configuration E reached with q ∈ nb E (p) and a configuration E � is reached with p ∈ nb E � (r ) and either Then according to the assumptions nb E (p) ⊆ nb E � (p) and therefore q ∈ nb E � (p). Hence, we reduced the problem to the first case.
The proof for (q, p) ∈ Msgs D ∧ (p, r ) ∈ Msgs D is similar.
For the second case holds Let p, q, r ∈ P with {p, q}, {p, r } ∈ E UNTM(D) , ((p < q ∧ q < r ) ∨ (r < q ∧ q < p)) and r and q are the processes that are allowed to send keep-alive-messages by O as soon as they both know p. Furthermore, assume that in every of the below reached configurations R i. e., D � =⇒ R the neighborhood of p � ∈ {p, q, r } has only grown i. e., nb D (p � ) ⊆ nb R (p � ), otherwise according to Lemma 10 there has to be intermediate configuration S in which the subprocess Alg match � p � � executes a step and select � findLin , but then p � executes a linearization step in S which is a contradiction to the assumption that there is no possible linearization step in the directed topology with messages and this can only be resolved by sending keep-alive-messages as all possible steps are receiving messages that are already in transit and the addition of previously received process ids to the neighborhood. Assume p < q < r (the proof for r < q < p is similar). According to Definitions 28 and 30 there are the following cases: • p is in the neighborhood of both processes: p ∈ nb D (q) ∧ p ∈ nb D (r ). According to Lemma 3 the subprocesses Alg match � q � and Alg match (r ) are enabled in D and stay enabled until they each execute a step. According to the assumption regarding O, Alg match � q � executes a step after a finite number of steps. Let E be the configuration before this step. It holds select � findLin � q, nb E (q) �� = ⊥ (otherwise there would be a possible linearization step for q). According to the assumption regarding O, Alg match (r ) executes a step after a finite number of steps. Let E � be the configuration before this step. It holds select (findLin (r, nb E � (r ))) = ⊥ (otherwise there would be a possible linearization step for q). Now there are two cases regarding the order of this steps.
If D � =⇒ E � � =⇒ E , it holds according to Lemmata 19,15 and 17 since up to E � no process was allowed to send keep-alive-messages . According to Corollary 2 it holds Since no other processes are allowed to send keep-alive-messages, it holds according to Lemmata 19,15 and according to the assumptions nb A (q) ⊆ nb E (q). Therefore, it holds (p, q) ∈ Msgs D �� . Since (p, r ) ∈ Msgs F � , it follows with Assumption 2 and Lemma 2 that p is the only process that can receive this message and therefore (p, since up to E no process was allowed to send keep-alivemessages. According to Corollary 2 it holds Since no other processes are allowed to send keep-alive-messages, it holds according to Lemmata 19,15 and 17 According to Corollary 2 it holds and according to the assumptions nb A (q) ⊆ nb E � (q). Therefore, it holds (p, r ) ∈ Msgs D � .
Since (p, q) ∈ Msgs F , it follows with Assumption 2 and Lemma 2 that p is the only process that can receive this message and therefore (p, q) ∈ Msgs D �� ∨ � p ∈ P � D � ∧ add D � (p) = q � ∨ q ∈ nb D �� (p). Therefore, with (p, r ) ∈ Msgs D � there is a possible linearization step in the directed topology with messages of D �� . And with it holds that there is a possible linearization step in the directed topology with messages of D � and and hence D � is the searched configuration D �� itself.
If |nb E � (r )| = 1, it holds with Lemmata 19 and 17 on O prevents sending keep-alive-messages as long as another deadlocked configuration is reached.
(p, r ) ∈ Msgs D � , we reach according to Lemma 4 and Corollary 4 configurations G and G � with q ∈ nb G (p) and r ∈ nb G � (p). Assume is similar). According to the assumption it holds q ∈ nb G � (p) ⊇ nb G (p). Since no other process was allowed to send keep-alive-messages by O and until now there was no enabled linearization step, it holds nb G � (p) = {q, r } and this remains unchanged until p executes the linearization step. Therefore, according to Lemma 3 the subprocess Alg match � p � is enabled in G � and stays enabled until it executes a step. According to the fairness assumption 3, Alg match � p � executes a step after a finite number of steps. Let G �� be the configuration before this step. Since up to this point there was one possible linearization step in the directed topology with messages, it Since nb G �� (p) = {q, r } and p < q < r , it holds with the definition of select (findLin ()) that select � findLin � p, nb G �� (p) �� = (q, r ).
Since q < r and p < q, it holds with Corollary 2 that Hence with Lemma 15 it holds Ψ(D �� ) < Ψ(G �� ). It holds with the assumptions that p ∈ nb D (r ) ⊇ nb G �� (r ) and with p < r and Definition 35 therefore that LeftNM With Ψ(D �� ) < Ψ(G �� ) and Definition 38 it holds • p is in the neighborhood of one process and for the other one is an add-step necessary: . According to Lemma 4 there will be a configuration E reached with p ∈ nb E (r ). According to the assumptions it holds that p ∈ nb E (q) ⊇ nb D (q). Hence, we reduced the problem to the previous case. The proof for � q ∈ P � D ∧ add D (q) = p � ∧ p ∈ nb D (r ) is similar.
• p is in the neighborhood of one process and the other one has a message left to receive: p ∈ nb D (q) ∧ (r, p) ∈ Msgs D . According to Corollary 4 we reach a configuration E with p ∈ nb E (r ). According to the assumptions it holds that p ∈ nb E (q) ⊇ nb D (q). Hence, we reduced the problem to the first case. The proof for (q, p) ∈ Msgs D ∧ p ∈ nb D (r ) is similar.
• For both processes is an add-step necessary: . According to Lemma 4 there is a configuration E reached with p ∈ nb E (q) and a configuration E � is reached with p ∈ nb E � (r ) the second case is similar). Then according to the assumptions nb E (q) ⊆ nb E � (q) and therefore p ∈ nb E � (q).
Hence, we reduced the problem to the first case.
• For one process is an add-step necessary and the other one has a message left to receive: assume � q ∈ P � D ∧ add D (q) = p � ∧ (r, p) ∈ Msgs D . According to Lemma 4 there is a configuration E reached with p ∈ nb E (q) and according to Corollary 4 a configuration E � with case is similar). Then according to the assumptions nb E (q) ⊆ nb E � (q) and therefore p ∈ nb E � (q). Hence, we reduced the problem to the first case.
The proof for (q, p) ∈ Msgs D ∧ � r ∈ P � D ∧ add D (r ) = p � is similar.
• Both processes have a message left to receive: (q, p) ∈ Msgs D ∧ (r, p) ∈ Msgs D . According to Corollary 4 there is a configuration E reached with p ∈ nb E (q) and a configuration E � is reached with p ∈ nb E � (r ) and either Then according to the assumptions nb E (q) ⊆ nb E � (q) and therefore p ∈ nb E � (q). Hence, we reduced the problem to the first case.
Therefore, for every reachable configuration R i. e., A � =⇒ R it holds for that either there is no more possible linearization step in the undirected topology with message or there is at least one.
In the first case, it holds as shown that If there is still a possible linearization step in the undirected topology with messages, then there are two cases. Either there is still a possible linearization step in the directed topology with messages or not.
In the first case, we reach a configuration S i. e., A � =⇒ R � =⇒ S with In the second case, we reach a configuration S � i. e., A � =⇒ R � =⇒ S � such that there is again a possible linearization step in the directed topology with messages of S � with Therefore, by induction we eventually reach a configuration C � i. e., . As shown in the base case, it holds for C � that

Strong Convergence
In this chapter, first of all, we describe the problem in proving strong convergence. However, we are convinced that the presented algorithm not only converges weakly, but also strongly. Therefore, we give strong arguments for strong convergence in the general case. We will introduce further already proven lemmata and informally further open lemmata with proof sketches, that could be helpful in a formal proof. Afterwards, we discuss several approaches for a proof of the strong convergence property in the general case.

Problem Description
Although keep-alive-messages are necessary to prevent deadlocks and termination of the algorithm, they also introduce problems in proving strong convergence. This is mainly based on the fact that such a message can reestablish an edge that was already deleted through a linearization step. Consider, for example, a configuration with a topology without messages as depicted in Figure 4. 1. Process w can send keep-alive-messages to process u. Assume process u executes its possible linearization step and deletes w from its neighborhood, but afterwards there are still messages of the form u〈w〉 in transit. With reception of such a message, u reestablishes its edge to w. Therefore, u potentially has to execute multiple linearization steps in order to remove the edge to w permanently.
u v w We proved strong convergence holds whenever either only too many edges exist or only desired edges are missing. Unfortunately, for arbitrary configurations where desired edges are still missing and undesired edges existing, the system does not converge always to the same of these situations first. Therefore, it holds neither in the general case that first all undesired edges are deleted nor that first all desired edges are established. In fact, it is possible in a configuration in which both not hold, that with the execution of the last linearization step the desired topology, up to receiving the sent message, is reached directly. To make matters worse, for the same initial configuration there can be depending on the order of steps executions where first all undesired edges are deleted, first all desired edges are established, and the desired topology is reached directly. This holds for example in a configuration with a topology as depicted in Figure 4. 2. If first v and x are sending keep-alive-messages and the messages are received by w before u executed its linearization step, a configuration is reached where only too many edges exist. If u executes its linearization step (and no more u〈w〉 messages are in transit) and w receives the sent message before x sends keep-alive-messages, a configuration that only lacks desired edges is reached. If x sends keep-alive-messages and w receives such a message before u executes its linearization step (and v does not send keep-alive-messages in the meantime), the desired topology, up to message reception, is with execution of the linearization step reached directly. Therefore, it is not possible to show for the general case that always a weaker property, like every process has a neighbor on both sides, holds, before the system reaches a correct configuration.
u v w x We can show that, whenever undesired edges still exist, eventually another linearization step is executed. However, we have no control or knowledge which linearization step will get executed and how the system evolves in the meantime. This is actually a problem for most of the liveness properties. For example, we proved that messages always are received and processed. Therefore, the carried process id will be at some point in the neighborhood of the receiving process. However, we do not know which steps were executed in the meantime and therefore how the rest of the configuration looks like.
A standard way to prove strong convergence is to define a monotonically decreasing potential function that is minimal for a correct configuration. In order to show progress, it is necessary that one can show that this function always eventually decreases strictly as long as a correct configuration is not yet reached. With the property that whenever the system is not stabilized there will be eventually a linearization step executed, this would be achieved most easily if the potential function strictly decreases with every executed linearization step. Unfortunately, this is not readily possible. If we want to design a potential function that decreases with every executed linearization step, we have to take the number of connections (i. e., neighborhood, adding and messages in transit) into account. We have to take the messages in transit and adding of processes into account, because otherwise the potential function would increase whenever a process adds a process id it does not already has in its neighborhood. In order to have a strict decrease with every linearization step, we also have to take the number of connec-

Problem Description
tions into account, as some linearization steps do not change the topology with messages, but only change the number of connections. This is depicted in Figure 4.3, let the shown graph be the topology with and without messages of a configuration. Assume that additionally to the depicted neighborhoods there are messages of the form u〈w〉 and w〈u〉 in transit. Then, the execution of both possible linearization steps does not change the topology with messages.
The only change is that there is one connection less of the form (u, w) (respectively (w, u)) and one more of the form (w, v) (respectively (u, v)). Nevertheless, this leads always to a function that at least increases whenever a process is sending keep-alive-messages to processes that already know it while taking messages into account. These steps lead to no further change in the topology with messages besides to increase the number of such messages and therefore the number of connections between these processes. Therefore, a potential function that decreases strictly with every linearization step, cannot be monotonically decreasing in every case.
u v w Therefore, the best that can be achieve with a monotonically decreasing potential functions is, to design a function that strictly decreases for (linearization) steps that have certain properties. Such properties are, for example, removing the last longest connection or acquaint a process with a nearer process than all already known one. However, we do not only have to show that such steps exist and the potential function strictly decreases whenever such a step is executed, but also that such steps are always reached if the system is not stabilized yet. The problem in this is that such decreasing steps are often triggered by further steps that other processes have to execute previously.
It is crucial to be very careful with simply assuming that certain steps will be executed in a subsystem and therefore lead to a certain configuration for the whole system. The assumption that the system reaches a configuration with certain properties presupposes in general a form of livelock freedom in a subsystem or the overall system. Strong convergence itself shows a special form of livelock freedom in the system whenever the system is not yet stabilized.
Assumptions based on the livelock freedom in a certain subsystem are therefore very prone to introduce circular reasoning. Without careful consideration of such assumptions, it could easily happen that one only shows that strong convergence holds if strong convergence holds and therefore nothing at all. Consider a configuration with a topology without messages as depicted in Figure 4.4. It is not possible without further ado to assume that v will eventually send keep-alive-messages to u and therefore, with reception of such a message, to enable u to execute a linearization step. In order to ensure that v will eventually send keep-alive-messages it is necessary that v previously removes w and x permanently from its neighborhood. This is only the case if there is no livelock in the subsystem containing the processes v, w and x.
u v w x y

Arguments for Strong Convergence
New edges are only established by receiving a corresponding message. A message to a process p can only be send from a neighboring process q that sends keep-alive-messages or executes a linearization step. While sending keep-alive-messages two new edges are established at most, as a process can only send such messages if it has at most two neighbors and they are not on the same side. The established edges have the same length as the edges that are used to send the messages. Furthermore, if a new edge is established in a linearization step, it is always strictly shorter than the potentially removed one. A process p only executes a linearization step if it has two neighbors that have either both smaller or both greater ids than the executing process and are therefore on the same side. The process sends the further away process r the id of the nearer one q and deletes the further away one from its neighborhood. This means that the number of connections always stays the same in a linearization step. The number of connections from r to q is increased by one while the connections from p to r decrease by one.
The distance between the executing process p and the more distant process r is strictly greater than the distance between r and the process in the middle q. Hence, the removed connection is strictly longer than the new established one. Therefore, in every linearization step a longer connection is exchanged through a strictly shorter one. Altogether, it can never be an edge established that is longer than the longest existing edge in the topology with messages.
Only a process itself can remove another process from its own neighborhood. The only steps that lead to such a removal are linearization steps. An enabled linearization step only exists if the process has at least two neighbors on the same side and while executing a linearization always only one process is removed. Therefore, whenever a process knows a process on one of its sides, it always has a neighbor on this side. Additionally, as always the further away process is removed, a process never removes a desired neighbor from its neighborhood. Furthermore, it follows that as soon as the neighborhood of a process contains all desired neighbors it will never send undesired keep-alive-messages again.
Messages can be send through keep-alive-messages or linearization steps. All these messages are eventually received and processed. If a process p receives a message there are four cases, depending on the neighborhood of p before the addition of the received id q. If the neighborhood of the receiving process does not contain any process on the same side like q, then after the addition of this id, there will always be a process on this side in the neighborhood of p. This holds, as processes never remove the current closest ids in the neighborhood to both sides. If the neighborhood of p already contains another process on the same side like q, independent whether this process is closer or more distant to p than q, then the addition of q will enable p to execute a linearization step. This holds, since there are now at least two neighbors on this side. If the distance to q is smaller than to any other previously known process on this side, the nearest neighbor on this side is permanently improved. Furthermore, p will never again send keep-alive-messages on this side to a process that is further away than q. This holds as p can only remove q again from its neighborhood after the reception of an even closer id on this side and processes can only send keep-alive-messages if they only have at most one process in the neighborhood on each side. If a process receives a message with an id that is already in its neighborhood, the number of this connection is decreased by one during addition. Therefore, the only steps that do not yield to any progress in the system are the sending of keep-alive-messages to processes that already know the sending process in the topology with messages. These steps only increase the number of corresponding connections.
Whenever an already deleted edge is reestablished through a message sent during a linearization step, an even longer connection was removed for this. Additionally, it holds that edges that were already deleted during linearization steps in the topology without messages, can be reestablished through keep-alive-messages that are already in transit. However, when executing a linearization step it is ensured that the more distant process eventually forever stops to send keep-alive-messages to the executing process. The executing process p sends the id of the intermediate process q to the further away process r . This message will eventually be received and processed by r . After the addition of q, at the latest, r has a process in its neighborhood that is on the same side then p, but closer. As mentioned before r can never send keep-alive-messages to p again. From this point on, the number of connections from p to r can only be increased if another process sends a p〈r 〉 message during a linearization step. A linearization step that leads to the sending of such a message can again not be disturbed by further keep-alive-messages. For the executing process s of such a linearization step, p itself has to be the further away process. It holds that p already cannot send keep-alive-messages to s ever again, as it will always have a closer neighbor than s on this side, currently r . This is depicted in Figure 4 Furthermore, the current longest edges in the system cannot be reestablished through linearization steps, as the established connection is always strictly shorter than the removed one. Therefore, whenever a process p removes a longest edge during a linearization step where the process r on the other end already cannot send keep-alive-messages and there are no further messages in transit that can reestablish this edge, it is permanently removed. As mentioned before, the sending of such keep-alive-messages stops at the latest with the reception of the message of the first linearization attempt. From this on, the number of connections m for this longest edge (p, r ) can never increase again. If there are still messages in transit that reestablish this edge, all of them will eventually be received and processed. Every processing of such a message that occurs while r is currently in the neighborhood of p decreases the number of connections by one. Furthermore, whenever r is in the neighborhood of p, there is always a possible enabled linearization step involving r , as p will always have a closer neighbor on the same side. Otherwise the linearization step would not have been possible at the first time. Therefore, the edge (p, r ) is permanently removed, whenever p executes at most m more linearization steps that involve r . Thereby, the intermediate process can, but not necessarily has to be the same process.
Every process that is only known in the topology with messages by (a subset of) its desired neighbors will never receive any other messages than keep-alive-messages from these desired neighbors, unless it sends its own id through keep-alive-messages to other processes or the desired neighbor sends its id during a linearization step to another process. Further, such a process cannot receive a message from a desired neighbor during a linearization step as the messages are always sent to the further away process. Every process that only knows (a subset of) its desired neighbors will never send any other messages than keep-alive-messages to these desired neighbors, unless it receives the id of another process. Therefore, a process that in the topology with messages only knows (a subset of) its desired neighbors and is only known by (a subset of) its desired neighbors is permanent partially stabilized. This means, that it only can send and receive keep-alive-messages to and from desired neighbors, until one of them sends its id to another process during a linearization step. Furthermore, if a process is contained in the neighborhood of all its desired neighbors and its neighborhood contains them, this property remains invariant, as the desired neighbors never remove the process during a linearization step and the process never removes them.
If the minimum or maximum process of the system is in the topology with messages only in the neighborhood of desired neighbors and its neighborhood only contains desired neighbors, it is completely stabilized permanently. As mentioned, the process itself can only send keep--alive-messages to desired neighbors, that does not change anything for the topology with messages. Furthermore, a desired neighbor cannot know another process on the same side and will never send the process id during a linearization step to another process. Therefore, the process will never receive another process id anymore and stays stabilized. This property is then transferred to the next process inwards the system, i. e., for the minimum process the next greater process and for the maximum process the next smaller, making this process the next border between the stabilized part of the system and the unstabilized one. Figure  4.6 depicts the topology with messages of a configuration with the border process u and y. Therefore, starting with the minimum and maximum process of the system, every border process that is stabilized once, remains stabilized forever.
u v w x y z t s

Further Proven Lemmata
We show that the system does not deadlock i. e., whenever there are still possible linearization steps in the undirected topology with messages, there is always a configuration reached where again a linearization step is possible in the directed topology without messages. This holds since every process that cannot find a linearization step can send keep-alive-messages to its current neighbors and all messages are received and processed eventually.

Lemma 24: No Deadlock
Let A be a configuration of the algorithm according to Lemma 1. If there is a possible linearization step in the undirected topology with messages i. e., ∃p, q, r ∈ P .{p, q}, {p, r } ∈ E UNTM(A) ∧ ((p < q ∧ q < r ) ∨ (r < q ∧ q < p)) but there is no possible linearization step in the directed topology i. e., ∀p, q, r ∈ P .((p < q ∧q < r )∨(r < q ∧q < p)) =⇒ ((p, q) ∉ E NT(A) ∨(p, r ) ∉ E NT(A) ) then eventually a configuration will be reached where a linearization step is possible in the directed network topology.

Proof:
Since there is no possible linearization step in the directed network topology it holds according to Lemma 6 that ∀p � ∈ P .nb A (p � ) ≤ 2. Since there is a possible linearization step in the undirected topology with messages but not in the directed topology there have to be p, q, r ∈ P with {p, q}, {p, r } ∈ E UNTM(A) and p < q < r (possible left linearization step) or r < q < p (possible right linearization step) . Assume p < q < r , the proof for r < q < p is similar. Furthermore, we assume that in every reached configurations C , but then there was an linearization step possible (and executed) in R. According to Definition 30 one of the following cases is true: The cases when p knows both other processes in the directed topology with messages are: • There is just an add-step necessary to enable a linearization step: . According to Lemma 4 there will be a configuration C reached with r ∈ nb C (p). According to the assumptions it holds that q ∈ nb C (p) ⊇ nb A (p) and p < q < r . Therefore, in C is a linearization step possible. The case • There is just one message left to receive: assume q ∈ nb A (p) ∧ (p, r ) ∈ Msgs A . According to Corollary 4 we reach a configuration C with r ∈ nb C (p). According to the assumptions it holds that q ∈ nb C (p) ⊇ nb A (p) and p < q < r therefore in C is a linearization step possible.
The case (p, q) ∈ Msgs A ∧ r ∈ nb A (p) is similar.
• There is an add-step necessary and a message left to receive: assume According to Lemma 4 there will be and q ∈ nb C � (p). Up to this point p cannot receive any message as the subprocess Alg rec � p � is not enabled as long as Alg add � p, q � is enabled and according to 2 messages cannot get lost and according to Lemma 2 p is the only process that can receive this message. Therefore it holds that (p, r ) ∈ Msgs C � . According to Corollary 4 a configuration C �� is reached with r ∈ nb C �� (p). According to the assumptions it holds that q ∈ nb C �� (p) ⊇ nb C � (p) and p < q < r . Therefore, in C �� is a linearization step possible.
The case for (p, q) ∈ Msgs A ∧ � p ∈ P � A ∧ add A (p) = r � is similar.
• There are two messages left to receive: (p, q) ∈ Msgs A ∧ (p, r ) ∈ Msgs A . According to Corollary 4 a configuration C is reached with q ∈ nb C (p) and a configuration C � is reached with r ∈ nb C � (p) and either A � =⇒ the second case is similar). Then according to the assumptions nb C (p) ⊆ nb C � (p) and therefore q, r ∈ nb C � (p) and p < q < r . Therefore, in C � is a linearization step possible.
The cases when p knows one process and the other process knows p in the directed topology with messages are: • p has one process in its neighborhood and the other process has p in its neighborhood: assume q ∈ nb A (p) ∧ p ∈ nb A (r ) . According to Lemma 3 the subprocess Alg match (r ) is enabled in A and stays enabled until it executes a step. According to the fairness assumption 3 Alg match (r ) will execute a step after a finite number of steps. Let C be the configuration before this step. Assume select (findLin (r, nb A � (r ))) = ⊥ (otherwise there would be a possible linearization step for r and nothing left to show). According to Corollary 2 it holds According to the assumptions nb A (r ) ⊆ nb C (r ). Therefore it holds (p, r ) ∈ Msgs C � . Additionally also nb A (p) ⊆ nb C � (p) and therefore q ∈ nb C � (p). Hence we reduced the problem to the second case.
The case for p ∈ nb A (q) ∧ r ∈ nb A (p) is similar.
• p has one process in its neighborhood and for the other process is an add-step necessary: According to Lemma 4 there will be a configuration C reached with p ∈ nb C (r ). According to the assumptions it holds that q ∈ nb C (p) ⊇ nb A (p). Hence, we reduced the problem to the previous case.
• p has one process in its neighborhood and the other process has a message left to receive: assume q ∈ nb A (p) ∧ (r, p) ∈ Msgs A . According to Corollary 4 we reach a configuration C with p ∈ nb C (r ). According to the assumptions it holds that q ∈ nb C (p) ⊇ nb A (p). Hence, we reduced the problem to the fifth case.
The case for (q, p) ∈ Msgs A ∧ r ∈ nb A (p) is similar.
• One process has p in its neighborhood and for p is an add-step necessary: assume � p ∈ P � A ∧ add A (p) = q � ∧ p ∈ nb A (r ). According to Lemma 4 there will be a configuration C reached with q ∈ nb C (p). According to the assumptions it holds that p ∈ nb C (r ) ⊇ nb A (r ). Hence, we reduced the problem to the fifth case.
The case for p ∈ nb A (q) ∧ � p ∈ P � A ∧ add A (p) = r � is similar.
• One process has p in its neighborhood and for p is a message left to receive: assume (p, q) ∈ Msgs A ∧ p ∈ nb A (r ). According to Corollary 4 we reach a configuration C with q ∈ nb C (p). According to the assumptions it holds that p ∈ nb C (r ) ⊇ nb A (r ). Hence, we reduced the problem to the fifth case. The case for p ∈ nb A (q) ∧ (p, r ) ∈ Msgs A is similar.
• There are two add-steps necessary: According to Lemma 4 there will be a configuration C reached with q ∈ nb C (p) and a configuration C � is reached (the second case is similar). Then according to the assumptions nb C (p) ⊆ nb C � (p) and therefore q ∈ nb C � (p). Hence, we reduced the problem to the fifth case. The case for • There is an add-step necessary and a message left to receive: assume � p ∈ P � A ∧ add A (p) = q � ∧ (r, p) ∈ Msgs A . According to Lemma 4 there will be a configuration C reached with q ∈ nb C (p) and according to Corollary 4 a configuration (the second case is similar). Then according to the assumptions nb C (p) ⊆ nb C � (p) and therefore q ∈ nb C � (p). Hence, we reduced the problem to the fifth case.
The case for (q, p) ∈ Msgs A ∧ � p ∈ P � A ∧ add A (p) = r � is similar and the cases for (p, q) ∈ with switched roles.
• There are two messages left to receive: assume (p, q) ∈ Msgs A ∧ (r, p) ∈ Msgs A . According to Corollary 4 there will be a configuration C reached with q ∈ nb C (p) and a configuration C � is reached with p ∈ nb C � (r ) . Then according to the assumptions nb C (p) ⊆ nb C � (p) and therefore q ∈ nb C � (p). Hence, we reduced the problem to the fifth case.
The case for (q, p) ∈ Msgs A ∧ (p, r ) ∈ Msgs A is similar.
The cases when both other processes know p in the undirected topology with messages are: • p is in the neighborhood of both processes: p ∈ nb A (q) ∧ p ∈ nb A (r ) . According to Lemma 3 the subprocess Alg match � q � is enabled in A and stays enabled until it executes a step. According to the fairness assumption 3 Alg match � q � will execute a step after a finite number of steps. Let C be the configuration before this step. Assume select � findLin � q, nb C (q) �� = ⊥ (otherwise there would be a possible linearization step for q and nothing left to show). According to Corollary 2 it holds and according to the assumptions nb A (q) ⊆ nb C (q). Therefore it holds (p, q) ∈ Msgs C � . Additionally also nb A (r ) ⊆ nb C � (r ) and therefore p ∈ nb C � (r ). Hence, we reduced the problem to the ninth case.
• p is in the neighborhood of one process and for the other one is an add-step necessary: . According to Lemma 4 there will be a configuration C reached with p ∈ nb C (r ). According to the assumptions it holds that p ∈ nb C (q) ⊇ nb A (q). Hence, we reduced the problem to the previous case. The case for • p is in the neighborhood of one process and the other one has a message left to receive: p ∈ nb A (q) ∧ (r, p) ∈ Msgs A . According to Corollary 4 we reach a configuration C with p ∈ nb C (r ). According to the assumptions it holds that p ∈ nb C (q) ⊇ nb A (q). Hence, we reduced the problem to the thirteenth case.
The case for (q, p) ∈ Msgs A ∧ p ∈ nb A (r ) is similar.
• For both processes is an add-step necessary: . According to Lemma 4 there will be

Arguments for Strong Convergence
a configuration C reached with p ∈ nb C (q) and a configuration C � is reached with the   second case is similar). Then according to the assumptions nb C (q) ⊆ nb C � (q) and therefore p ∈ nb C � (q) . Hence, we reduced the problem to the thirteenth case.
• For one process is an add-step necessary and the other one has a message left to receive: assume � q ∈ P � A ∧ add A (q) = p � ∧ (r, p) ∈ Msgs A . According to Lemma 4 there will be a configuration C reached with p ∈ nb C (q) and according to Corollary 4 a configuration (the second case is similar). Then according to the assumptions nb C (q) ⊆ nb C � (q) and therefore p ∈ nb C � (q). Hence, we reduced the problem to the thirteenth case.
The case for (q, p) ∈ Msgs A ∧ � r ∈ P � A ∧ add A (r ) = p � is similar.
• Both processes have a message left to receive: (q, p) ∈ Msgs A ∧ (r, p) ∈ Msgs A . According to Corollary 4 there will be a configuration C reached with p ∈ nb C (q) and a configuration C � is reached with p ∈ nb C � (r ) and either Then according to the assumptions nb C (q) ⊆ nb C � (q) and therefore p ∈ nb C � (q). Hence, we reduced the problem to the thirteenth case.
✷ Therefore, through fairness it holds that whenever the system is not stabilized yet, there will always be linearization steps executed. Nevertheless, it is not possible to show without further ado that a certain linearization step will get enabled or executed.
A crucial fact for convergence is that it is not possible to establish longer edges than the current existing edges. Therefore, whenever m is the length of the longest edges in the system and all edges with length m are removed, there will never be edges with length m again.

Definition 40: Longest Edge(s)
The length set Lengths : T → 2 N with New edges in the topology with messages can only be established through the sending of keep-alive-messages or linearization steps. Every linearization step only introduces (if not already existent) a shorter edge than the deleted (but eventual through messages still existent) one, every sending of keep-alive-messages establishes at most two equal long edges than the edges used to send them. Therefore, no edge can be established that is strictly longer than the already existing edges.

Lemma 25: Only shorter Edges established
Let A be an arbitrary configuration of the algorithm according to Lemma 1. Let A � be an arbitrary configuration with A � −→ A � . It holds two more edges are established at most and every new edge is shorter or equal to another already existing edge. Therefore, it holds Proof: According to Corollary 2 there are only the following cases: • If a process p ∈ P tries to find a linearization step, but select The (undirected) network topology does not change because the neighborhood of all processes stays the same. Since nb A � = nb A it holds according to Definitions 27 and 29 The undirected network topology with messages does not change since it is only pos- with j ∈ nb A (p). Let j ∈ P be an arbitrary process with j ∈ nb A (p). According to Definition 27 it holds (p, j ) ∈ E NT(A) . Therefore, with nb A � = nb A , add A � = add A and Definition 30 it holds that The network topology with messages changes depending on whether the (at most) two neighbors of p already have p in their neighborhood or not. There are two cases. If ( j , p) ∈ E NTM(A) , then also ( j , p) ∈ E NTM(A � ) . If ( j , p) ∉ E NTM(A) , then with ( j , p) ∈ Msgs A � according to Definition 28 ( j , p) ∈ E NTM(A � ) and with Definitions 16 and 15 len(( j , p)) = len((p, j )). Therefore, it holds len((q, p)) = len((p, q)) ∧ (p, r ) ∈ E NT(A) ∧ len((r, p)) = len((p, r )) iff • If a process p ∈ P finds a left linearization step i. e., select In every linearization step p removes the further away process from its neighborhood, hence the network topology without messages is reduced by this edge. Therefore, with j ∈ nb A (p) according to the definition of select � findLin � p, nb A (p) �� and Definition 27 it holds that • If a process p ∈ P A receives a message with the id of q ∈ P i. e., (p, q) ∈ Msgs A , it holds The (undirected) network topology does not change since q is not yet added to the neighborhood of p. Since nb A � = nb A it holds according to Definitions 27 and 29 The (undirected) network topology with messages does not change since the edge is already established through the message in transit. Since (p, q) ∈ Msgs A it holds according to Definitions 28 and 30 that (p, q) ∈ E NTM(A) and {p, q} ∈ E UNTM(A) . With p ∈ P � A � and add A � (p) = q it holds further that also (p, q) ∈ E NTM(A � ) and {p, q} ∈ E UNTM(A � ) . Therefore • If a process p ∈ P � A adds a process q ∈ P to its neighborhood i. e., (p, q) ∈ add A it holds If q is already in the neighborhood of p then the topology does not change, otherwise a new edge is established in the network topology without message.
The undirected network topology does not change if either q is already in the neighborhood of p or vice versa.
Since additionally no process is added to the neighborhood it holds that LeftN ✷ This also induces that the shortest edges of each process never gets longer.

Corollary 14: Shortest Edge to each Side only gets shorter
Let A be an arbitrary configuration of the algorithm. Let R be an arbitrary reachable configuration i. e., A � =⇒ R. It holds that the shortest outgoing edge of any process in R in each direction is shorter or equal to the shortest outgoing edge of this process in A in the same direction. This follows directly with Definitions 15, 27 and 16.
It follows moreover that whenever a process knows a process on each side, its neighborhood always contains at least two (or in the case of the smallest and greatest process one) other processes.

Corollary 15: Neighborhood stays ≥ 2 (resp. 1 for Min and Max)
Let A be an arbitrary configuration of the algorithm. Let R be an arbitrary reachable configu- Whenever this is the case, the reception of every unknown process id leads to an enabled linearization step and stops the process from sending keep-alive-messages for now (if this was possible previously).

Open Lemmata
The sending of keep-alive-messages can reestablish an edge in the topology without message that was already removed through a linearization step. However, if a process executes a linearization step, it prevent the further away process eventually from ever sending keep-alivemessages to it again.

Lemma 27: Stop sending Keep-alive-messages during Linearization Step
If a process p executes a linearization step, then the further away process r eventually can never send keep-alive-messages to p again.

Proofsketch:
Let C be an arbitrary configuration and an arbitrary process p executes a linearization step in C , i. e., (select Assume select � findLin � p, nb C (p) �� = (q, r ) ∧ (q < r ∧ p < q) (the other case is similar). Since (r, q) ∈ Msgs C � it holds according to Corollary 4 that a configuration C �� is reached with q ∈ nb C �� (r ). For every reachable configuration R i. e., C �� � =⇒ R it holds according to Lemma 26 with q < r ∧ p < q that there is a process s ∈ P with s ∈ LeftN (nb R (r ), r ) and s > p. Since p < r it holds if p ∈ nb R (r ), then p ∈ LeftN (nb R (r ), r ) and |nb R (r )| ≥ 2. Therefore, there is an enabled linearization step for r in R and r cannot send keep-alive-messages according to Lemma 6. Hence, it holds for every from C �� reachable configuration R, if r can send keep-alive-messages then p ∉ nb R (r ) and therefore r can never send keep-alive-messages to p again.
If there are only three processes in the system, then an enabled linearization step is successful after a finite number of steps i. e., the longer edge is removed and will never be reestablished. With a similar argumentation it holds that an edge which cannot be reestablished through other linearization steps is removed permanently under the assumption that a corresponding linearization step is chosen often enough.

Lemma 28: Linearization Step for Three Processes
Let |P r oc s| = 3 and P = p, q, r with p < q < r . Let A be an arbitrary configuration with nb A (p) = {q, r } (respectively nb A (r ) = {p, q}). After a finite number of steps there is a configuration C reached with (p, r ) ∉ E NTM(C ) (respectively (r, p) ∉ E NTM(C ) ). It holds then for every reachable configuration R i. e., C � =⇒ R that (p, r ) ∉ E NTM(R) (respectively (r, p) ∉ E NTM(R) ).

Proofsketch:
According to Lemma 3 the subprocess Alg match � p � is enabled and stays enabled until it executes a step. Let A � be the configuration before this step. According to Lemma 10 it holds that nb A � (p) = {q, r }. Since p < q < r and P = p, q, r it holds with the definition of select (findLin (·)) that select � findLin � p, nb A (p) �� = (q, r ). Hence, according to Corollary 2 A � � −→ C � with According to Lemma 27 a configuration C �� is reached with q ∈ nb C �� (r ) and r can never Since there is no connection from p to r , r can never again send keep-alive-messages to p and there is never a message p〈r 〉 sent in a linearization step, it holds for every reachable configuration R i. e., C �� � =⇒ R that (p, r ) ∉ E NTM(R) . Assume m > 0 connections and the claim holds for all m � < m. Since r can never again send keep-alive-messages to p and there is never a message pr sent in a linearization step, it holds for every reachable configuration that the number of connections cannot be increasing. Since m > 0 it holds according to 28 that p〈r 〉 ∈ Msgs C �� , add C �� (p) = r or r ∈ nb C �� (p). With Lemma 4 and Corollary 4 in all cases a configuration L is reached with r ∈ nb L (p). According to Lemma 3 the subprocess Alg match � p � is enabled and stays enabled until it executes a step. Let L � be the configuration before this step. According to Lemma 10 it holds that r ∈ nb L � (p). Since p < q < r and P = p, q, r it holds that q = succ(p) and therefore with Lemma 11 follows nb L � (p) = {q, r }. It holds with the definition of select (findLin (·)) that select � findLin � p, nb L � (p) �� = (q, r ). Hence, according to Corollary 2 Hence, there are with Definition 28 in L �� now m �� < m � connections from p to r and the claim holds with the induction hypothesis.
If there are only three processes in the system, then strong convergence holds for any arbitrary initial configuration. If there are only edges missing, then the configuration is an undirected correct configuration and strong convergence is ensured. Otherwise the possible linearization step(s) will be successful finished after a finite number of steps and therefore a undirected configuration reached.

Lemma 29: Convergence for Three Processes
Let |P r oc s| = 3 and P = p, q, r with p < q < r . Let I be an arbitrary connected initial configuration i. e., the undirected topology with messages of I is connected. A correct configuration C is reached after a finite number of steps i. e., Since the undirected topology with messages of I is connected, it holds with I � =⇒ L �� and Lemma 7 that also L �� is connected.
Since L �� is connected and P = p, q, r , but (p, r ), (r, p) ∉ E NTM(L �� ) , it holds with Definitions 28 and 32 that L �� is an undirected correct configuration. Therefore, with Lemma 20 it holds that a correct configuration C is reached after a finite number of steps i. e., I � =⇒ L � � =⇒ L �� � =⇒ C and NTM(C ) = G LIN ∧ NT(C ) = G LIN . For the case that only one linearization step is enabled, assume nb L (p) = {q, r } (the proof for nb L (r ) = {p, r } is similar). The enabled linearization step will be successful after a finite number of steps according to Lemma 28 and therefore a configuration L � with (p, r ) ∉ E NTM(L � ) is reached. If furthermore (r, p) ∉ E NTM(L � ) , then L � is according to Definitions 28 and 32 an undirected correct configuration, since L � is connected with Lemma 7 and P = p, q, r , but (p, r ), (r, p) ∉ E NTM(L � ) . It then follows with Lemma 20 that a correct configuration C is reached after a finite number of steps i. e., I � =⇒ L � =⇒ L � � =⇒ C and NTM(C ) = G LIN ∧ NT(C ) = G LIN . Otherwise it holds that (r, p) ∈ E NTM(L � ) . With Definition 28 it holds therefore p ∈ nb L � (r ), add L � (r ) = p or (r, p) ∈ Msgs L � . Since the other linearization step is permanently finished it holds additionally q ∈ nb L � (r ). Therefore, there is a possible linearization step in the directed topology with messages and according to Lemma 4 and Corollary 4 a configuration L �� is reached with p ∈ nb L �� (r ). Since P = p, q, r with p < q < r it holds q = pred(r ) and therefore with Lemma 11 that q ∈ nb L �� (r ). Therefore for r is a linearization step enabled in L �� and with Lemma 28 a configuration L ��� is reached with (r, p) ∉ E NTM(L ��� ) . Since L ��� is connected according to Lemma 7 and P = p, q, r , but (p, r ), (r, p) ∉ E NTM(L ��� ) it holds with Definitions 28 and 32 that L ��� is an undirected correct configuration. Therefore, with Lemma 20 it holds that a correct configuration C is reached after a finite If a process sends keep-alive-messages at several times in an execution, then the processes it sends these to, get never further away over the execution. Therefore, the distances only decrease and the sending of keep-alive-messages can only get less disadvantageous.
already knows with or without messages a closer process than r , then q also will eventually be able to execute a linearization step itself, meaning again more progress for the stabilization. In every case, a connection between two more distant processes is exchanged through a shorter connection.

Proofsketch:
The message q〈r 〉 will according to Corollary 4 eventually received and processed and therefore a configuration is reached in which q has a process in its left or right neighborhood (dependent on whether r is smaller or greater than q). According to Lemma 26 q will then always have a process in the neighborhood on this side. If q already had another neighbor on this side before the processing of this message, then according to Lemma 6 it will enable q to execute a linearization step itself. If r is nearer than every neighbor that q had before on this side then according to Lemma 26 the closest neighbor on this side is improved permanently. Since processes can only send keep-alive-messages if they only have at most one process on this side and they never remove their closest neighbor on a side, it holds additionally that q will never send such messages again to a further away process than r on this side (especially not p). It holds for the executed linearization step that either p < r < q or q < r < p and therefore with definition 15 that dist(q, r ) < dist(p, q). Since one connection from p to q is removed and one from q to r is added, it holds that a connection between two more distant processes is exchanged through a shorter connection.
As soon as a process knows all of its desired neighbors it never sends undesired keep-alivemessages again and therefore no further step of this process increases Ψ and Ψ � . If every process knows all desired neighbors, then the desired topology is a subgraph of the topology with and without messages and strong convergence is ensured through Lemma 21.

Lemma 32: Stop sending undesired Keep-alive-messages
Let C be an arbitrary configuration and p ∈ P an arbitrary process with {succ(p), pred(p)} ⊥ ⊆ nb C (p). It holds for every reachable configuration R with C � =⇒ R that p cannot send keep-alive-messages in R to a process q ∉ {succ(p), pred(p)} ⊥ .

Proofsketch:
For every reachable configuration R holds with Lemma 11 that {succ(p), pred(p)} ⊥ ⊆ nb R (p). A process sends keep-alive-messages always to its complete neighborhood. Therefore, if p could send keep-alive-messages in R to q ∉ {succ(p), pred(p)} ⊥ , it holds q ∈ nb R (p). But since all desired neighbors are in the neighborhood of p i. e., {succ(p), pred(p)} ⊥ ⊆ nb R (p), it holds that there is an enabled linearization step for p and therefore according to 6 p cannot send keep-alive-messages at all.

Approaches
The first approach is a structural induction over the topology with messages. If a border process, starting with the process with minimum or the process with the maximum id, has in the topology with messages only edges to and from its desired neighbors, then every step that it executes in every execution can only be the sending to or receiving of keep-alive-messages from its desired neighbors. It can can only send keep-alive-messages as it does not have two neighbors on the same side. Since the only process that could have it in its neighborhood is a desired neighbor, it will never receive another message than a keep-alive-messages anymore, as messages in linearization steps are always sent to the further away process. The process closest to the current border process inwards the system is then the new border process with the same properties. Therefore, from the outside inwards the system stabilizes. Nevertheless, it is not simply possible to prove that the current border processes eventual permanently remove all their connections to undesired neighbors. Even harder to prove is that all other processes remove their connections to them. This is based on the fact that the border process and the inner system influence each other. There are, for example, configurations as depicted in Figure 4.4 where first the inner system has to execute certain steps to enable a border process to remove its connections to undesired neighbors. This requires some form of livelock freedom in the inner system without introducing circular reasoning. In the depicted situation the induction hypothesis could help as the border process can not influence the inner system as long as the inner system does not communicate with a border process. However, as long as there are connections from the border processes to or from undesired neighbors it is possible that we alter between situations where the border processes have to execute certain steps to enable the inner system to execute certain steps and vice versa. In such situations the induction hypothesis can not always be used. Consider a configuration with a topology with messages like depicted in Figure 4. 7. The border process z has to execute its linearization step in order to enable the inner system containing v, w, x and y to execute a linearization step. The border processes u and z can do nothing in the meantime except sending keep-alivemessages, which does not enable further linearization steps in the inner system. If the inner process v does not send keep-alive-messages before the reception of the message from z, it has to execute its linearization step in order to be again able to send keep-alive-messages to u. This is only ensured to happen if v can permanently remove its edge to x, which potentially requires some form of livelock freedom in the inner system although the induction hypothesis can not be used in this case. Only by sending these keep-alive-messages the border process u can execute a linearization step after reception. Neither keep-alive-messages nor linearization steps establishing edges that are longer as the current longest edge in the topology with messages. The potentially new edge that is established through a linearization step is even strictly shorter than the at least temporarily removed one. If one could show that always the current longest edges are removed permanently, strong convergence would hold. This could be shown through induction. The induction variable could be either the length of the longest edge, or one could go for a nested induction over this length and the number of nodes. Another similar possibility is a proof through convergence stairs. The maximum length of an edge in a system with n processes is n − 1. Show that for a configuration with a maximum edge length of k > 1 in the topology with messages, eventually in every execution a configuration is reached with a maximum length of k − 1. A configuration with a maximum edge length of one in the topology with messages is an undirected correct configuration and therefore strong convergence holds. It could be helpful for this approach to change the algorithm to the variant LIN max , which could be simply done by adapting the select functions of the processes. In this variant we have more knowledge about which linearization steps are executed because the processes always select linearization steps that, at least temporarily, remove their longest edge. Nevertheless, the problem remains to show that the linearization steps regarding the longest edges in the topology with messages always get enabled without introducing circular reasoning.
The potential function Ψ E is monotonically decreasing with every step in every case. Therefore, if we can show that whenever the system is not stabilized yet, that always eventually a step is executed that leads to a strict decrease of Ψ E strong convergence would be proven. Since Ψ E is minimal if and only if the topology with messages contains only too many edges, and therefore with Lemma 22 convergence is ensured. Unfortunately, this is not easy to prove. The function Ψ E is the sum of functions for every process. The decrease of the function from a process p is always caused by the sending of messages of another process q. This makes it harder to identify situations that lead to a decrease and reason about them. To make matters worse, there are configurations in which first certain linearization steps have to be executed before a situation is reached where such a strictly decreasing step is enabled (an example is depicted in Figure 4.8). It is very difficult to prove that such a situation is always reached, especially without further knowledge about how the rest of the system evolves in the meantime and no further properties about livelock freedom.
u v w x y In general, perhaps a more global potential function could help. Indeed, it is really challenging to capture certain global properties formally. Also a monotonically decreasing function only leads to a relatively easy proof of convergence if it is possible to show for every configuration that, if the system is not stabilized yet, the function strictly decreases eventually. Finding a monotonically function, like Ψ � or simply the length of the longest edges in the system, is therefore not the hardest part of the convergence proof. But without proving that there are always eventually steps executed in which such a function strictly decreases, it does not prove convergence and all our previous attempts failed for this reason.
A lot of issues in proving strong convergence arise from the fact that almost every lemma regarding liveness properties can just state that eventually a certain property for the system or a certain process holds. Without further invariants, that leads to the problem that we have no knowledge about how the rest of the system evolves in the meantime.
Therefore, it could be more promising to try another approach in proving strong convergence and concentrate even more on properties that could be helpful for a proof through convergence stairs. Here it is especially challenging, for the same reasons as for strong convergence itself, to prove that the next stair i. e., a configuration that satisfies the next predicate, eventually is reached in every execution. Therefore, it is crucial to identify further properties that are weaker than convergence itself, that prevent the system from being captured in a livelock. This would be helpful in all previously stated approaches.

Conclusion
We redesigned the algorithm for shared memory from Gall et al. (2014) in such a way that our algorithm works in an asynchronous message-passing system. The algorithm of Gall et al. (2014) works in a system where potentially all processes must have access to the whole memory and is therefore very restricted. In the redesigned algorithm, processes communicate via message-passing. Furthermore, we do not require any assumptions about the time a process needs to execute a step or for message delivery. The algorithm works therefore in a completely asynchronous distributed message-passing system. This is a significantly weaker requirement and corresponds more to real life system properties. Therefore, the redesigned algorithm is applicable in more systems than the original one.
In order to model the algorithm for a message-passing system, we extended the localized π-calculus. This provides us through its precise defined syntax and semantics, with the possibility to model the algorithm in an unambiguous way. Furthermore, this is the basis for proving properties about the algorithm in a formal way. The usage of a kind of standardform of a configuration helps us to simplify the proof by identifying every possible reachable process term with a structural equivalent representative and therefore reducing the cases to be analyzed. Further, this enables us to explicitly keep track of the global state of the system in a convenient way. This allows us to execute our proofs in a state-based fashion, which is more traditional for distributed algorithms (Lynch, 1996), than in an action-based style, that is more natural for process calculi.
An algorithm is self-stabilizing, if it satisfies the properties closure and convergence. We formally proved the closure property, i. e., if the system reaches a correct configuration, then it stays in a correct configuration and therefore every step that can be executed leads again to a correct configuration. The convergence property postulates that from any arbitrary initial configuration a correct configuration is reached. There are two forms of convergence. Starting with an arbitrary initial configuration, strong convergence requires that in every execution a correct configuration is reached, whereas weak convergence only claims the existence of such an execution. We proved strong convergence for two special cases. First, whenever the topology with messages of a connected initial configuration only lacks desired edges but no undesired ones exist, strong convergence holds. This means more concrete that every message to a process in the system only carries the id of the successor or predecessor, the adding in progress involves only consecutive processes, the neighborhood of each process contains only desired neighbors, and between each pair of consecutive processes is at least one kind of these connections in one direction. Second, strong convergence also holds, whenever in the topology with messages of an initial configuration there are just too many edges, but no desired ones are missing. This means, every process knows its desired neighbors, while also taking the messages in transit into account as well as the adding in progress. For the general case, i. e., an arbitrary connected initial configuration in which there are in the topology with messages desired edges missing as well as still undesired edges exist, we proved weak convergence. For this proof, we introduced a global omniscient entity, called a perfect oracle. A perfect oracle is not implementable in reality, but also can, and should, be seen as a restriction of the set of executions for an arbitrary initial configuration. Then, we showed that every execution that is admissible under the assumption of a perfect oracle ensures strong convergence. Since for every initial configuration this is a non-empty set of executions, weak convergence holds in the general case.
Furthermore, we described the problems and challenges for a strong convergence proof in the general case. These problems arise mainly from undesired keep-alive-messages which can reestablish already deleted edges. These keep-alive-messages are necessary to prevent the system from deadlocks and the algorithm from termination, which would be contradictory for a distributed message-passing self-stabilizing algorithm. In the proof for weak convergence, unnecessary undesired keep-alive-messages are suppressed by the perfect oracle. This is not implementable by the nodes themselves or in a real distributed system, as it requires global knowledge about the system. Additionally, without further weaker livelock freedom properties than convergence itself, there is the threat to introduce circular reasoning. Nevertheless, we gave strong arguments for strong convergence for every arbitrary initial configuration and introduced further already proven, and open lemmata, including for example strong convergence in case of three processes, with proof sketches. These lemmata identify further properties that can support a number of different variants of a formal proof of strong convergence. Conclusively, we discussed several approaches for a proof of strong convergence in the general case.
Our proof is, using the precisely defined calculus as basis, much more formal than the original proof. Therefore, the chance of failures in the proof is significantly lower. Furthermore, it has a higher level of detail. This again reduces the risk of failures and leads to a better insight in the properties of the algorithm and overall to a better understanding. In comparison to the original algorithm, our algorithm is not only applicable in a wider field of system properties, but also reduces the threat of partitioning the system in case of faults. In the original algorithm, for example, even the single loss of a connection in a correct configuration leads to a loss of connectivity in the whole system, that has to be reestablished through an external mechanism.

Related Work
However, the single loss of a connection cannot lead to a disconnection of the system in a correct configuration in our algorithm. A partitioning of the system can only occur, if all connections in both directions between two processes are getting lost through faults. In a correct configuration, there are at least two connections between each pair of consecutive processes.
Self-stabilizing algorithms are very difficult to design. For a distributed message-passing algorithm we need to ensure that the communication between neighboring processes continues in a correct configuration and therefore the algorithm does not terminate. In order to realize this, we introduced the sending of keep-alive-messages in case a process does not find a linearization step. Such messages can lead to a reestablishing of already deleted edges. This cannot be simply prevented by the use of additional variables. It is, for example, not possible to introduce a variable in which a process stores which edges it already has deleted through linearization steps and suppress the reestablishing in case of receiving a corresponding id. Every variable in a self-stabilizing algorithm has to be initializable with an arbitrary value. Therefore, in an initial configuration such a variable could contain a desired neighbor. This would prevent the reachability of a correct configuration, as this desired neighbor would never be added to the neighborhood of the process. For each process the reception of messages and searching for linearization step has to be executable concurrently and cannot be executed alternating as this could lead to deadlocks and prevent the stabilization of the system. This implies that a lot of problems in proving strong convergence are also existent in a weaker form, even with synchronous communication between the processes. Therefore, we decided to model the algorithm directly for asynchronous message-passing to lower the system assumptions as much as possible. Consequently, there are always many different sequences of events possible. Progress properties are mostly only eventually statements. Therefore, certain things will eventually happen, but we have no certainty when they happen. To make matters worse, we have no control or knowledge which steps are executed by the processes in the meantime. Therefore, without further invariants we do not know how the rest of the system evolves. Altogether, this leads for each initial configuration to an enormous number of executions that have to be considered. Additionally, every possible configuration has to be regarded as an initial configuration. Since strong convergence is a property that has to consider all executions of all initial configurations, the sheer number of executions by itself, makes a formal proof a challenging task.

Related Work
Self-stabilization in the context of distributed computing was first introduced by Dijkstra (1974). The fundamentals of topological self-stabilization and linearization for this work are originated in Gall et al. (2014). This paper is also the foundation for the algorithm and the main idea of the proofs. The basics in designing a self-stabilizing algorithm and main proof techniques, as well as a general introduction and overview can be found in Dolev (2000).
We used an extended localized π-calculus to model our algorithm in an unambiguous way and as a formal basis for proofs. The basic localized π-calculus is based on Merro and Sangiorgi (1998) and extended in a way similar to Wagner and Nestmann (2014). Furthermore, we introduce a kind of standardform based on ideas similar to Wagner and Nestmann (2014) which enables us to explicitly keep track of the global state and therefore the topology of the system. The basis of this idea was, in a very simple form, already introduced by Milner (1999).

Future Work
Regarding the future work, the next step is to prove strong convergence in the general case. The primary goal is therefore a convergence proof in the general case without any oracle necessary. On the way, it could be interesting to lower the restrictions on the set of executions by an oracle and therefore consider a weaker oracle to acquire further insight in properties that could be helpful for a proof without an oracle. Thereby, the weaker the oracle the more executions are proven to ensure convergence.
There are several approaches in order to prove strong convergence in the general case without any oracle. The first task is to identify further properties that ensure livelock freedom in the system that are weaker than strong convergence itself. Such properties, for example, can be used to prove that either the monotone decreasing function Ψ E always decreases strictly eventually whenever the system is not stabilized yet or to show that linearization steps involving the longest edges in the system are eventually enabled and executed. With one of the two properties a convergence proof for the general case can be achieved relatively easy. Further livelock freedom properties would also be helpful if considering a potential function that utilizes more global knowledge about the system, as well as a proof using no potential function at all, but works with convergence stairs.
Another future line of work is the consideration of confluence properties of the system. Further, it would be interesting to investigate the possibility of the parallel execution of steps. This would build the basis to analyze the complexity of the algorithm. Also the scalability of the algorithm is of further interest in this context. The algorithm could then be compared to other algorithms or variants of the algorithm itself. For example, the usage of counter variables that only allow to trigger keep-alive-messages every n−th time, could decrease the sending of undesired unnecessary keep-alive-messages significantly.
Furthermore, it would be interesting to consider how far the algorithm could be adapted in order to establish more complex overlay topologies, for example a hypercube. A line is the basic element for a lot of shapes, therefore it should be possible to simulate an algorithm that establishes a more complex topology, for example by running several instances of our algorithm. To analyze this possibility in comparison to other algorithms is an interesting future task. The investigation of algorithms for more complex topologies is in general a promising further field of work.