Jane Scott

Mark John

John Zoe

Anna Jane

Anna John Mark

Scott Scott

Zoe Jane

Anna Zoe

Mark Scott

John Mark

Jane Zoe Anna

Mark, John} Jane {scott

Mark, Scott} Anna {john

Zoe {mark

Anna Scott

Mark, John} Anna {scott

Mark, Scott} Zoe {john

John {zoe

Anna Jane}

Jane {mark

Keywords: Algorithmes Distribués, Modèles Asynchrones, Auto-stabilisation, Mariage Stable, Complexité en Moves, Démon inéquitable, Confidentialité Asynchronous Self-stabilizing Stable Marriage Distributed Algorithms, Asynchronous Model, Self-stabilization, Stable Marriage, Move Complexity, Unfair Daemon, Privacy algorithm Asynchronous Self-stabilizing Stable Marriage Distributed Algorithms, Asynchronous Model, Self-stabilization, Stable Marriage, Move Com-

Mariage Stable Asynchrone et Auto-stabilisant Mots-clés :

The Stable Marriage Problem (SMP) is a matching problem where participants have preferences over their potential partners. The objective is to find a matching that is optimal (stable in certain sens) with regard to these preferences. This type of matching has a lot of widely used applications such as the assignment of children to schools, interns to hospitals, kidney transplant patients to donors, as well as taxi scheduling or content delivery on the Internet. Some applications can be solved in a centralized way while others, due to their distributed nature and their complex data, need a different treatment. For example, when applying this problem to the Cloud-Computing context, virtual machines are emulated by real machines located all over the world. A centralized algorithm would cause unbearable delays and be sensible to failures, which is inconceivable for a service meant to be available at any time.

On the other hand, when humans are to be matched or involved in a matching, they have the right to keep their personal data private and in particular their list of preferences. Consequently, the preference lists should not be transmitted on the Internet, and even less gathered for a centralized treatment. This is why, distribution, faulttolerance (by self-stabilization) and privacy are the three main keywords of this thesis.

In order to handle these challenges, we provide two distributed self-stabilizing solutions. Such solutions tolerate transient (or short-lived) failures (e.g., memory or message corruptions) of any nodes. The privacy of the preference lists is guaranteed by the two proposed algorithms: lists are not shared, only some binary queries and responses are transmitted. One of the differences between the two algorithms is the communication model: the first algorithm uses the state model while the second algorithm uses the more general register model. In both models, executions proceed in atomic steps and a daemon (distributed unfair daemon) conveys the notion of asynchrony. Under this daemon, the stabilization time can be bounded in term of moves (local computations). This complexity metrics allows to evaluate the necessary computational power or the energy consumption of the algorithm's executions. This is not the case when the stabilization time is measured in rounds since an unbounded number of moves may be executed during a round.

The first algorithm, based on the centralized method of Ackermann et al. (SICOMP' 2011), solves the problem in O(n 4 ) moves.

The starting point of the second algorithm is the local detection/global correction scheme of Awerbuch et al. (DA' 1994): a non-self-stabilizing algorithm (with initialization) that satisfies the property of local checkability can be combined with a detector and a reset algorithms. The result of this composition is a self-stabilizing version of the given algorithm. Unfortunately, local checkability definition of DA '1994 does not apply to our case (in particular due to the unfair daemon). Consequently, we propose a new definition. Furthermore, we design a distributed self-stabilizing asynchronous reset

Introduction

"Matching under preferences is a topic of great practical importance, deep mathematical structure, and elegant algorithmics." Kurt Melhorn in [START_REF] Manlove | Algorithmics Of Matching Under Preferences[END_REF] Stable Marriage is a matching problem where the participants have preferences over their potential partners. The objective is to find a matching (i.e., an assignment of the participants to one another) that is optimal (stable in a certain sense) with regards to these preferences. This type of matching has a lot of widely used applications such as the assignment of children to schools, interns to hospitals, kidney transplant patients to donors, as well as taxi scheduling or content delivery on the Internet. But in fact, matching under preferences is as old as civilizations. In some cases, the difficulty to solve this problem seemed to have caused serious trouble. As an example, if we go back to antiquity, Danaus had fifty daughters, the Danaides. After Aegyptus, his brother, commanded that his fifty sons should marry the Danaides, Danaus, maybe afraid of the difficulty of getting a matching which would satisfy everybody, elected to flee instead, and to that purpose, he built a ship, the first ship that ever was and fled to Argos. Naturally, the problem is still relevant nowadays. For example, APB (Admission Post-Bac) and ParcourSup, the applications intended to manage the student/university assignments in France use matching under preferences algorithms.

Matching under preferences is an important topic in the domain of economics, especially in market modelization. As a matter of fact, it is easy to relate the notion of preference to the notion of payoff. The preferred choice is associated to the one with the higher payoff and so on. That is why, since the beginning of its algorithmic study fifty years ago, the matching problem with preferences has received a large attention from the economy world. One of the actors in this domain, Lloyd Shapley, received in 2012 the Nobel Prize in economy, partly for his work on matching under preferences. Later, strong relations with game theory have been established: the solutions achieve a pure Nash equilibrium in a cooperative game. Lloyd Shapley and David Gale, in a famous article [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF], introduced in its current form an instance of matching under preferences by using the metaphor of marriage. There are women and an equal number of men. Each accepts to be married with a person of the other sex. Each participant, woman or man, has a complete list of preferences on the persons of the other sex. The problem is to get them married in such a way that the matching is stable. In this example, stable means that there does not exist a pair of a woman and a man, each married to other partners but that prefer each other. If there is no such unmarried pair, there is always somebody in a married pair who has no interest, in terms of preference, in changing her or his partner (see Chap. 3 for formal definition). Gale and Shapley called this problem Stable Marriage and this name is still used to define the form of matching under preferences. Stable marriage is a model for simple markets (like producers/consumers) but when modeling real world interactions, more complicated situations arise. For this reason, many variants of the problem have since been developed and analyzed. We study some of these variants (e.g., stable marriage with ties, with incomplete list, ...) in Chapter 6.

Although being one of the most studied topics in algorithmics during the last decades, matching under preferences stays a very important subject, because of its universality. A deep theory has been developed, numerous theorems have been established, several books on the topic have been published [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF][START_REF] Roth | Two-sided Matching: A Study in Game-Theoretic Modeling and Analysis[END_REF][START_REF] Manlove | Algorithmics Of Matching Under Preferences[END_REF], Donald Knuth wrote a monograph [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF] on the topic, and yet the subject is still alive. Indeed, emerging networks and in particular the Internet puts this problem in a completely different perspective and scale. Fifty years ago, the issue was to find algorithmic solutions to handle very hard problems. When one had to match several thousands of medical students, each with its own preferences, to hundreds of hospitals, each with its own criteria, in a way where everybody was satisfied, the solutions by hand were not feasible. Thanks to the advent of computers, a satisfying output was obtained: all the complex data was fed into one machine that calculated the matching. This centralized way of computing the data is still used, but there are new situations (i.e., with distributed data/computation power) that require a different treatment. As an example, consider a typical Cloud. There are real machines, the computers, located in data centers all over the world, emulating virtual machines and able to give a personalized service to the consumers. An issue is: on which real machine(s) to run the virtual machines in order to have the best performance? But also: where to migrate them depending on the load of the real machines in real time? This type of problem corresponds to the matching under preferences. A centralized solution would cause unbearable delays in the decisions and create bottlenecks. Such a solution would have no failure tolerance, what is inconceivable for a service that is supposed to be available at any time. Due the nature of the problem, solution here must be distributed: the different data centers have to take their decisions locally, from their own information and the information received from other data centers. On the other hand, consider examples of matching under preferences involving humans, like residents-to-hospitals assignments or students-to-universities matchings (e.g., ParcourSup or APB). People have the right to keep their personal data private and in particular their list of preferences: such a list may give a lot of sensible information on a person. The risk is that connections and deductions could be made from participant's preference lists leading to a loss of privacy. Consequently the preference lists of persons should not be transmitted on the Internet, and even less gathered for a centralized treatment.

That is why we are aiming at solutions based on matching under preferences, which are completely distributed, tolerate a certain type of failures and respect the confidentiality of the lists. To the best of our knowledge, it is the first time that these three notions are incorporated together for solving the problem.

In order to handle faults, we provide self-stabilizing distributed solutions. Such solutions tolerate transient (or short-lived) failures (e.g., memory or message corruptions) of any number of nodes. That means that after any number of such failures (corrupting nodes' memory), which bring the system into an arbitrary state, the algorithm must recover from these failures (automatically -without any intervention). Meanwhile, the constants and the code are assumed to be untouched. Thus a self-stabilizing solution solves a problem whatever starting configuration (the global system state) is (see a formal definition in the models and definitions Chapter 3, Section VI). This property is particularly interesting for Cloud and Internet based applications in general, since they frequently require some level of self-stabilization.

We consider two models of communication commonly used for self-stabilizing algorithms: the state model (cf. [START_REF] Dijkstra | Self-stabilizing Systems in Spite of Distributed Control[END_REF]) and the register model (cf. [START_REF] Dolev | Self-stabilization of dynamic systems assuming only read/write atomicity[END_REF]). In both models, executions proceed in atomic steps and a daemon conveys the notion of asynchrony. We assume the strongest (and the most general) daemon (adversary), the distributed unfair daemon. It models a very high level of asynchrony. In particular, it may keep a node from being activated as long as other nodes are eligible for activation (have instructions to execute). Though being general, designing and analyzing algorithms under such daemon is more difficult than under fair daemons. The natural time measure with unfair daemon is in terms of steps or moves (local computations). This is also practically relevant metrics since all local actions are counted until stabilization, allowing the computational power and the energy consumption being evaluated (cf. [START_REF] Baidas | Energy-efficient partner selection in cooperative wireless networks: a matching-theoretic approach[END_REF]). Indeed, with other deamons such as the weakly fair one (often used for self-stabilizing algorithms), the stabilization time is measured in term of rounds. In a round, all eligible nodes are activated at least once. That is, under an unfair daemon, a round may contain an unbounded number of moves. Thus, a round analysis may lead to a too coarse-grained evaluation of the energy and computational consumption. Hence, a polynomial algorithm in term of rounds can be proved exponential in term of steps/moves. For example, a silent leader election with a linear round complexity [START_REF] Datta | An O(n)-time self-stabilizing leader election algorithm[END_REF][START_REF] Datta | Self-stabilizing leader election in optimal space under an arbitrary scheduler[END_REF] has been proved to be exponential [ACD + 17] in steps. Huang and Chen's BFS Algorithm [START_REF] Huang | A self-stabilizing algorithm for constructing breadth-first trees[END_REF] has an exponential lower bound in steps [START_REF] Devismes | Silent self-stabilizing BFS tree algorithms revisited[END_REF]. Similarly, in [START_REF] Glacet | Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Networks[END_REF], they prove that the step lower bound of their algorithm [START_REF] Glacet | Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Networks[END_REF] is exponential, while the upper bound in rounds is linear. Moreover, the step/move distributed analysis can be compared with the analysis of some centralized solutions for stable marriage where the evaluations are in terms of queries or messages (cf. [START_REF] Ostrovsky | Fast Distributed Almost Stable Matchings[END_REF]).

Contributions and Roadmap

The Stable Marriage Problem (SMP) is defined on the complete bipartite graph K n,n (one set of women and one of men). Each node u has a different priority for each node v in the other set, between 1 (the most preferred) and n. The goal is: (i) to match (marry) the women and the men together such that everyone is matched, in a way that (ii) there is no pair of a woman and a man that are not matched to each other, but prefer each other over their current matches. When there are no such pairs, called blocking pairs (BPs), the set of marriages is said stable.

In this work, we consier decentralized distributed settings, where the bipartite graph represents a communication network. Edges represent the communication links and nodes are computing entities (to be matched), having unique identifiers. Each node has only a partial information about the problem instance, contrary to the centralized case. In particular, it is assumed to be initially aware only of its own preferences, but not of the other nodes' preferences. In addition, to ensure confidentiality of the preferences [START_REF] Brito | Distributed stable marriage problem[END_REF] and avoid high message complexity, we follow the previous related studies and rule out a trivial solution where nodes exchange their preference lists and then run a known centralized solution at each node.

Contributions. The present work aims to design algorithms for SMP in a distributed and self-stabilizing fashion but without exchanging preferences. Since a self-stabilizing algorithm runs from any configuration to a configuration satisfying the problem, nodes have to detect and manage the BPs. Unfortunately, in his monograph [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF], Knuth notices that resolving locally the BPs one after the other can lead to an infinite cycle of actions. The first step towards self-stabilization was made by Ackermann et al. [AGM + 11] who gave a centralized algorithm that solves locally the BPs in a particularly synchronized way avoiding cycling. Expressed in a distributed setting, this solution is not self-stabilizing, since even if the initial matching may be arbitrary, some variables are required to be initialized. Our first main contribution is a self-stabilizing solution to SMP in the distributed state model. This solution adopts the principle of (two) synchronized phases present in the Ackemann et al. solution, but has to add an additional phase for a distributed synchronization and a local management of variables ensuring the self-stabilization property. We present a formal analysis of the complexity in moves of the solution. The Gale and Shapley's Algorithm (GSA) is known to terminate in O(n 2 ) rounds, but also in O(n 2 ) moves. The Ackermann et al. centralized solution is of O(n 2 ) moves too. Our distributed solution is of O(n 4 ) moves [LMB + 17]. This raises the issue of the gap between the relevant centralized and distributed solutions. Note that an independent result [START_REF] Ostrovsky | Fast Distributed Almost Stable Matchings[END_REF] gives a lower bound for the communication complexity of Ω(n 2 ) bits, for solving the same problem (in the two parties communication setting using a single bidirectional link). However, this lower bound implies only Ω(n 2 / log n) moves in the communication model here (assuming constant size registers, used by our solutions).

This leads to the second main contribution of the thesis which is a distributed selfstabilizing solution for SMP in Θ(n 2 ) moves. Moreover we tackle this time the problem in a more general communication model of shared registers. In this model, instead of reading the states of the neighbors directly, a node can only access the designated per neighbor shared registers. This solution involves several stages. The starting point is the local detection/global correction scheme of [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] inspired by [START_REF] Afek | Memory-efficient self stabilizing protocols for general networks[END_REF]. The authors proved that if an algorithm A with initialization is locally checkable, it can be combined with a detector and a reset modules yielding a self-stabilizing algorithm. The basic idea is to launch a reset over the system, when a BP is locally detected (considering it as an abnormal situation). After resetting, the reached configuration is an initial configuration of A. Unfortunately, the local checkability in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] does not apply to our case even though BPs are locally detectable. Indeed, in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], the local checkability is defined under fair assumptions. But an unfair daemon can choose to keep nodes (e.g., those detecting faults) unactivated as long as other nodes are eligible, and in general even forever, avoiding the detection of faults/"anomalies" preventing the correct stabilization. Thus, we propose a new definition of local checkability with, in particular, a termination condition.

In addition, we design a self-stabilizing distributed asynchronous reset algorithm. This algorithm uses a rooted spanning tree that must be built in a self-stabilizing way too. Hence, we build a rooted spanning tree of depth 2. The reset algorithm has a stabilization time of O(n • 6 p ) moves (where p is the depth of the tree). There exist, in the literature, self-stabilizing reset algorithms functioning over a spanning tree [GM91, AO94, KA98, DJ19]. However, there is no one coming with move complexity analysis while running under unfair scheduler with shared registers communication model.

Finally, we propose an asynchronous version of GSA in the distributed link register model [BBB + 18] and we prove its local checkability according to our new definition. Then we put all the modules together and we prove that the algorithm resulting from the composition (with the tree construction, the reset and the detector) is correct and has a stabilization time of Θ(n 2 ) moves.

Other contributions of less importance are adaptations of the solutions for SMP to some variants of the problem: sets of unequal size, indifference, incomplete lists, manyto-one and many-to-many matchings. We want to emphasize that the results that we present are obtained under the so called unfair scheduler, which is the most difficult setting to deal with. An unfair scheduler may never choose to activate a process, unless this process is the only one to be eligible. ence lists), unacceptable partners (incomplete lists), many-to-one matching (Hospitalsto-Residents problem) and the more difficult many-to-many matching. The modifications for each case are presented in such a way that they can be simply combined together to obtain a general algorithm solving all the considered variants. Furthermore, we explain why the complexity and correctness proofs remain (almost) the same. In 1962, Gale & Shapley introduced the stable marriage problem in their seminal paper [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF]. After this publication, a lot of works have been published about this problem in economics but also in mathematics and computer science: the problem (and its variants) has many applications in these areas [START_REF] Biró | Applications of Matching Models under Preferences[END_REF]. It can be viewed as a particular formulation of two sided matching markets and has been proved useful in many empirical approaches. For example, it is central for the solution of the large residents-to-hospitals assignment in USA (since 1952) or to the students-to-schools matching in Boston or New York. Later, in computer science, it was used to perform migrations of VMs or schedule taxis [START_REF] Bai | A novel approach to independent taxi scheduling problem based on stable matching[END_REF][START_REF] Kuemmel | Taxi Dispatching and Stable Marriage[END_REF] . Numerous books [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF][START_REF] Roth | Two-sided Matching: A Study in Game-Theoretic Modeling and Analysis[END_REF][START_REF] Irving | Stable marriage and indifference[END_REF][START_REF] Manlove | Algorithmics Of Matching Under Preferences[END_REF], book chapters [START_REF] Klaus | Matching under Preferences[END_REF][START_REF] Biró | Applications of Matching Models under Preferences[END_REF][START_REF] Cseh | Popular Matchings[END_REF][START_REF] Cechlárová | School Placement of Trainee Teachers: Theory and Practice[END_REF] and surveys [START_REF] Chen | Computational Complexity of Stable Marriage and Stable Roommates and Their Variants[END_REF][START_REF] Cechlárová | Selected open problems in Matching Under Preferences[END_REF] have been written on this topic until now. An International workshop on Matching Under Preferences (MATCH-UP) is devoted to the matching problem each two/three years [MAT]. Finally, a Dagstuhl seminar dedicated to matching under preferences was scheduled in July 2020 [Dag].

We distinguish centralized (Section I) and distributed solutions (Section II). The second section sums up the works regarding two different models: synchronous (Subsection II.1) and asynchronous (Sub-section II.2).

Finally, since we focus on self-stabilization, we summarize main self-stabilizing results in Section III, first in a centralized context (Sub-section III.1), then concerning transformers (Sub-section III.2).

I -Centralized Solutions

In their paper, Gale and Shapley [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF] provided a centralized algorithm (working by deferred acceptances, see Chapter 5, Section III for explanations) running in O(n 2 ) time, which is proved to be asymptotically optimal (for centralized algorithms) in [START_REF] Ng | Lower Bounds for the Stable Marriage Problem and Its Variants[END_REF][START_REF] Segal | The communication requirements of social choice rules and supporting budget sets[END_REF]. Gale and Shapley proved also that there always exists at least one stable marriage in any system. The first application of this algorithm was for the allocation of graduating medical students in US hospitals. Still now, the national Resident Matching program uses (an extension of) this algorithm [NRM] and handle now over 40,000 applicants. Now, stable marriage algorithms are used to assign graduating medical students to residency programs at hospitals also in Canada and Scotland. Similar mechanism are used to assign students to schools and universities in Norway and Singapore (cf. [START_REF] Teo | Gale-shapley stable marriage problem revisited: Strategic issues and applications (extended abstract)[END_REF][START_REF] Golle | A Private Stable Matching Algorithm[END_REF]) but also in Boston [START_REF] Abdulkadiroglu | The Boston Public School Match[END_REF] and New York City [START_REF] Abdulkadiroğlu | The New York City High School Match[END_REF]. More recently, the french students-to-universities matching (APB, ParcourSup) uses also such algorithms.

Notice that, in [START_REF] Golle | A Private Stable Matching Algorithm[END_REF], Golle takles the problem of privacy and cheating in such systems: with the knowledge of all the preference lists, a participant can manipulate the algorithm and change the output matching [GS85, GI89, TST99]. Golle proposes a private algorithm based on the Gale and Shapley algorithm (preference lists are kept secret). Similarly, Doerner et al. in [START_REF] Doerner | Secure Stable Matching at Scale[END_REF] build a more efficient private algorithm (also based on Gale and Shapley algorithm) in order to apply it on large scale (for matching medical residents).

II -Distributed Solutions

Though different distributed problems have been well studied since decades, works on distributed stable marriage appeared much later than the centralized studies of this problem. Among these studies, theoretical ones consider an idealized synchronous distributed communication model, where nodes' progress in a lock-step manner, exchanging information and performing computations all together at each step (called round). These works focus on round complexity of the problem and its variants. On the contrary, studies with application cases consider an asynchronous distributed communication model, where there is no bound on message delivery, channel capacities or relative process speeds. That is, there is no global clock and nodes will eventually perform their computations. These works focus on applications such as Cloud-Computing or content delivery.

II.1 -Synchronous Model

Kipnis and Patt-Shamir [START_REF] Kipnis | A Note on Distributed Stable Matching[END_REF] prove a lower bound of Ω( (n/B log n)) rounds, where B is the number of bits per message, and provide an algorithm that solves the distributed stable marriage in O(n 2 ) rounds. Searching for better time complexity and conditions that can provide it, many studies consider specific restrictions on the preference lists such as weighted stable marriage [START_REF] Amira | Distributed Weighted Stable Marriage Problem[END_REF], incomplete or bounded lists [START_REF] Floréen | Almost Stable Matchings by Truncating the Gale-Shapley Algorithm[END_REF][START_REF] Ostrovsky | Fast Distributed Almost Stable Matchings[END_REF], "almost regular" lists [START_REF] Ostrovsky | Fast Distributed Almost Stable Matchings[END_REF] and "similarity" in preference lists [START_REF] Khanchandani | Distributed Stable Matching with Similar Preference Lists[END_REF]. Still for improving time complexity, approximate versions have been considered (e.g., [KPS09, FKPS10, GNOR15, OR15]), reaching a polylogarithmic time. Furthermore, when assuming strict restrictions on preference lists, approximate stable marriage can be solved even in constant time (cf. [START_REF] Floréen | Almost Stable Matchings by Truncating the Gale-Shapley Algorithm[END_REF][START_REF] Ostrovsky | Fast Distributed Almost Stable Matchings[END_REF]). Notice also several bound results on communication complexity and step complexity (cf. [START_REF] Segal | The communication requirements of social choice rules and supporting budget sets[END_REF][START_REF] Chou | Communication requirements for stable marriages[END_REF][START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF]). In particular, Gonczarowski [START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF] proved a lower bound on communication complexity: Ω(n 2 ) Boolean queries or bits have to be exchanged between two distributed parties, when one (Alice) holds all the preference lists of the one set (women) and the other party (Bob) holds all the preference lists of the opposite set (men), and they want to solve SMP with these preferences.

II.2 -Asynchronous Model

The first paper considering an asynchronous model in distributed settings is [START_REF] Brito | Distributed stable marriage problem[END_REF]. Brito and Meseguer propose an extended version of GSA (with proposals and acceptances), but the participants who receive and accept a proposal delete all the worse ranked participants in its preference list. Thus, the preference lists are not communicated, reenforcing the privacy of the data. This algorithm is intended to work in the message passing model and is asynchronous. It is provided with empirical results but no complexity analysis. In the domain of Cloud computing, stable marriage is used for performing efficient migration of virtual machines to servers (e.g., [START_REF] Xu | Egalitarian Stable Matching for VM Migration in Cloud Computing[END_REF][START_REF] Kim | Stable Matching with Ties for Cloud-assisted Smart TV Services[END_REF]). Notice that the Xu and Li's algorithm [START_REF] Xu | Egalitarian Stable Matching for VM Migration in Cloud Computing[END_REF] is an extension of the Brito et Meseguer's algorithm. Content delivery networks that distribute much of the world's content and services have to solve a large and complex stable marriage problem between users and servers [START_REF] Xu | Seen as stable marriages[END_REF][START_REF] Maggs | Algorithmic Nuggets in Content Delivery[END_REF]. Recently, in [START_REF] Yucel | Efficient and privacy preserving supplier matching for electric vehicle charging[END_REF], the authors apply the Brito' and Meseguer's algorithm for the scheduling of electric vehicle charging. Since charging takes a long time and the station depends on the demander's route, the scheduling must be done in-advance for efficient resource allocation. Furthermore, due to the frequent charging, driving patterns and preference lists can be divulged if the algorithm exchanges the input data. Thus, the algorithm must be dynamic, private and efficient. To compare their algorithm with the Gale and Shapley's algorithm, they made experiments and observe that their algorithm is more efficient and exchanges less message (than a adapted distributed version Gale and Shapley's algorithm).

III -Self-stabilizing Solutions

Introduced by Dijkstra in [START_REF] Dijkstra | Self-stabilizing Systems in Spite of Distributed Control[END_REF][START_REF] Dijkstra | A belated proof of self-stabilization[END_REF], self-stabilization is a property of distributed algorithms. A self-stabilizing algorithm for a problem P ensures that, from any configuration of the system (resulting from transient faults or not), the algorithm converges to the solution of P . Since many applications of stable marriage, especially in computer science, require failure tolerance1 , it is natural to look at a self-stabilizing solution (one of the failure tolerance schemes).

We first present works on the stable marriage that are related to self-stabilization in Sub-section III.1. There is no distributed, asynchronous and self-stabilizing solution for SMP but some results are helpful for our study.

A way of obtaining a self-stabilizing algorithm for a problem P is to combine a nonself-stabilizing algorithm for P with a transformer. Thus, in Sub-section III.2, we sum up such transformers with their pros and cons.

III.1 -On the Way to Self-stabilizing Stable Marriage Algorithms

Since self-stabilizing algorithms have to solve the problem from any configuration, a central issue is the resolution of blocking pairs (BPs). If a configuration contains an unstable marriage, the algorithm must detect BPs. Knuth in a famous monograph [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF] puts forward this question by providing a problematic example. Indeed, when starting from an arbitrary configuration, it may exist a circular path of BPs resolutions (by matching the blocking pair and the previous partners) involving that an execution may cycle. In the self-stabilizing context, this cycle can lead to a non convergent execution (see Chapter 4, Section I, for explanations). In [START_REF] Roth | Random Paths to Stability in Two-Sided Matching[END_REF], an open question raised by Knuth is answered: from any configuration containing an unstable matching, there exists at least one path of resolutions (by only matching the BPs' partners) that provides a stable matching. A consequence is that, under fair assumptions, from any unstable marriage there is a finite path of BPs resolutions that reaches a configuration with a stable marriage with probability one.

In [AGM + 11], Ackermann et al. propose an algorithm for the stable marriage problem, starting from an arbitrary matching. This algorithm works in two phases. The first solves BPs in the same manner as Roth [START_REF] Roth | Random Paths to Stability in Two-Sided Matching[END_REF], i.e. married women start solving their BPs. In the second phase, single women run GSA. This algorithm converges in polynomial time.

Finally, in [START_REF] Mathieu | Self-stabilization in preference-based systems[END_REF][START_REF] Mathieu | Upper bounds for stabilization in acyclic preference-based systems[END_REF][START_REF] Mathieu | Autour du pair-à-pair : distribution de contenus, réseaux à préférences acycliques[END_REF] the author investigates the so-called "selfstabilizing" stable marriage in peer-to-peer networks. The problem is restricted to acyclic preference lists (i.e. containing no cycle of peers such that each peer in the cycle prefers its successor to its predecessor). In this case, it is known that exactly one stable marriage exist. Moreover, the fact that there exists no cycle in the preference lists induces that Knuth's cycle cannot happen. Thus, starting in any given marriage, following any strategy of choosing and "fixing" blocking pairs, eventually results in a stable marriage. So, in this particular sense, the case of acyclic preferences is self-stabilizing. The authors prove that the number of such "fixes" (using any strategy) till stabilization can be exponential. However, if choosing the fixes in a round-robin fashion over the nodes' set, the number of fixes can be reduced to polynomial. Finally this study presents simulation results in P2P networks.

III.2 -Transformer to Self-stabilizing Solutions

There are several ways to transform a non-self-stabilizing algorithm into a self-stabilizing one. The first transformer was proposed by Katz and Perry [START_REF] Katz | Self-stabilizing Extensions for Message-passing Systems[END_REF]. It works for an asynchronous message passing system. Using a self-stabilizing snapshot [START_REF] Chandy | Distributed Snapshots: Determining Global States of Distributed Systems[END_REF], the protocol repeatedly evaluates the global state of the system. This evaluation is made by a fixed leader. If a "bad" global state is detected, a reset of the system is launched, restoring a pre-determined global state. This snapshot tool needs some synchronization (round numbers) and exchanges a lot of information (values of local variables and messages). The authors do not provide an upper bound on the number of messages. This approach uses global detection and global correction.

In [START_REF] Afek | Memory-efficient self stabilizing protocols for general networks[END_REF], a new approach is introduced: local detection and global correction. If a node maintains locally some information so that it can detect bad configurations, a global reset can be launched. When the reset is terminated, the algorithm is restarted from a predefined configuration from which it is correct. If such a local detection is feasible, the algorithm is said to be locally checkable. Notice that the communication model uses Read/Write atomicity [START_REF] Dolev | Self-stabilization of dynamic systems assuming only read/write atomicity[END_REF] with a fair daemon. Later, in [START_REF] Awerbuch | Self-stabilization by local checking and correction[END_REF][START_REF] Varghese | Self-stabilization by Local Checking and Correction[END_REF], another transformer with a local detection and local correction is proposed. A protocol is said to be locally correctable if the global state of the protocol can be corrected to a legitimate global state by applying independent local actions. The protocol uses the Input/Output Automata model with bounded channels [START_REF] Lynch | An Introduction to Input/Output Automata[END_REF].

Since many algorithms are not both locally checkable and correctable (most of the time only locally checkable), Awerbuch et al. [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] develop the local detection/global correction idea of [START_REF] Afek | Memory-efficient self stabilizing protocols for general networks[END_REF]. The global correction is made with a global reset. They formalize the definitions of local checkability and give an analysis of the combination: the stabilization time of the combined algorithm has an overhead of O(R) asynchronous rounds where R is the response time of the reset.

The global correction is made through a global reset. An example of such an approach is given in [START_REF] Arora | Distributed Reset[END_REF], where a self-stabilizing reset uses a spanning tree built in a self-stabilizing way. The requirements are unique identifiers and the knowledge of a bound on the number of nodes in the network. The stabilization time of this protocol has been proved for asynchronous rounds with a fair daemon.

In this work, we adopt the idea of the latter transformer, by adapting it to our setting with the unfair daemon (Chapter 5). We also design an appropriate reset algorithm. All that with the goal to evaluate the move complexity of the transformed self-stabilizing algorithm to SMP in the link register model under unfair daemon. This allows us to obtain a better time complexity of only O(n 2 ) moves in a more general (than the state reading) model. We first give a formal definition of the blocking pairs (BPs) and the Stable Marriage problem in Section I.

Chapter 3

Models and Definitions

Contents

Then, we define distributed systems and distributed algorithm (Section II and III) and the notion of an execution in Section IV. Then, in Section V, we define the two different communication models. Our algorithm (Chapter 4) is designed for the state model while the second one (Chapter 5) is designed for the link register model.

Finally, we define the self-stabilization property of distributed systems in Section VI and the associated complexity metrics (Section VII).

I -The Stable Marriage Problem

The stable marriage problem has been introduced by Gale and Shapley in their seminal paper in 1962 [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF]. We consider a set of men (Men) and a set of women (Women) such that each women w is given with a priority for each man m, denoted priority(w, m), and reciprocally. The priorities go from 1 to n and the most preferred person has priority 1. In such a system, the goal is to match (marry) women and men together such that everyone is matched and there is no blocking pair (BP), i.e., no unmarried pair (w, m) of a woman w and a man m, who both prefer each other to their current matches (partners). When there are no such pairs of nodes, the set of marriages is said to be stable. Formal definitions are given below.

Definition 1 (Blocking Pair (BP)). Given a matching M ⊂ Women × Men, a pair (w, m) is a blocking pair iff the following conditions hold: Notice that Gale and Shapley proved that there always exists at least one stable marriage for any instance of preference lists, but there are possibly several. In the Table 3.1, we present an example of an SM instance. Let us first consider a matching M 1 = {(Jane, M ark), (Anna, Scott), (Zoe, John)}. In this matching, the pairs (Zoe, Scott) and (Jane, Scott) are BPs, i.e. M 1 is unstable. On the contrary, the matchings M 2 = {(Jane, Scott), (Anna, John), (Zoe, M ark)} or M 3 = {(Jane, M ark), (Anna, John), (Zoe, Scott)} are stable. Remark 1. For technical reasons, we use in the proofs a more general definition of blocking pair than the definition given above, as it applies to incomplete matching. In the original definition, a blocking pair has to be a pair of already married persons. In the definition of BP used here, man can be unmarried. Formally, a pair (w, m) of a woman w and a man m is blocking iff w is matched to m , m is matched to w and w and m prefer each other to their actual matching, or, w is matched to m , m is unmatched and w prefer m to m . Clearly enough, the two notions coincide if the matching is complete. The definition implies that a man prefers to be matched with any woman rather than to stay unmatched.

II -Distributed Systems

A distributed system includes a set of computational units called nodes (or processes). They are connected, i.e. able to communicate in a one-to-one fashion and do not have a central memory. Furthermore, there is no centralized control over the nodes.

Each node v can communicate (directly) with a subset of other nodes, called its neighbors and denoted by N (v) (not including v). Communication is assumed to be bidirectional. Hence, the topology of the system can be represented as a simple undirected graph G = (V, E), where V is the set of nodes and E the set of edges, i.e., communication links. It is assumed that G is the complete bipartite graph K n,n , over two subsets of nodes of equal size n.

Following the terminology of [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF], we call women the n nodes of the first subset (Women) in the bipartite graph and men the n nodes of the second subset (Men). Each node has a unique identifier that can be compared to others. For a clear presentation, we use names to identify nodes. In addition, each node has locally a complete list of n ordered preferences for the nodes of the other set (each woman has a complete list of men and reciprocally) to represent the priorities.

III -Distributed Algorithms

III.1 -Algorithm

A distributed algorithm consists of a set of local algorithms (one per node). Each node updates its state according to its local algorithm. One way to represent the code of a node v is by a finite set of guarded rules of the following form:

Label: (* Comment *)
{Guard} Actions

The labels are used to identify rules. The guard of a rule in the code of v is a Boolean expression involving the variables of v and of its neighbors (inside their states or the shared registers, depending on the model). If the guard of some rule evaluates to True, then the rule is said to be enabled at v. Node v is said to be eligible if at least one of its rules is enabled. Actions represent a sequence of actions on v's variables. A rule can be executed (activated) only if it is enabled. In this case, its execution consists in performing the sequence of actions, using the values of the variables at the time of the guard evaluation.

III.2 -Configurations

The state of a node is a vector of the values of its variables. A configuration of the system is a vector of states of all nodes. For a given sub-algorithm Alg, we denote by C Alg a projection of a configuration C to the variables of Alg. By default, in a section dedicated to a particular algorithm Alg, when speaking of some configuration we refer to the projection of a configuration to the variables of Alg. Furthermore, we use the notation var(C) for the value of var in the configuration C.

IV -Execution of Distributed Algorithms

IV.1 -Scheduler

The asynchrony of the system is modeled by an adversary, called scheduler or daemon. In a configuration, the scheduler selects a non-empty subset of eligible nodes, then chooses one of the enabled rules per node, then, still atomically, executes the corresponding actions. This is called a step (or transition) and the activation of each rule in the step is called a move, i.e., there are at most n moves per step (one per node). Notice that, since the evaluation of all the rules is made at the same time, moves are causally independent. Such a scheduler is called distributed in the literature (contrary to a central scheduler, choosing at each step only one enabled node, or to the synchronous scheduler that chooses all the enabled nodes). It is convenient to represent a scheduler as a set of sequences of steps or, equivalently as the predicate defining this set. Different types of fairness, limiting the possible decisions of the scheduler, appear in the literature. We do not make any such limitation on the predicate except forcing the scheduler to choose at least one eligible node at each step. This scheduler appears in the literature under the name of unfair scheduler. It allows to obtain the strongest results, in particular because some constantly eligible node may stay inactivated for an arbitrary period of time.

IV.2 -Execution

When a step is executed in the configuration C, it leads to a configuration C' and we write C → C'. We say that C'

is reached from C, denoted by C * → C', if C s → C 1 s 1 → C 2 s 2 → . . . sx → C'. An execution is a maximal sequence of pairs (step, configuration): (s 0 ,C 0 ), (s 1 ,C 1 ), . . . , (s k ,C k ), . . . such that C i s i → C i+1
for all i ≥ 0 and such that the sequence of steps s 0 , s 1 , . . . satisfies the predicate of the scheduler.

The term "maximal" means that the execution is either infinite or ends in a terminal configuration, i.e., a configuration in which no node is eligible.

A distributed algorithm solves the stable marriage problem if each of its executions starting from a predefined initial configuration, under the unfair distributed scheduler, reaches a terminal configuration in which there is a stable marriage.

V -Communication Models

Several communication models exist in the literature. In this thesis, we use two models: the state model in Chapter 4 and the register model in Chapter 5. Thus, in the following, this two models are presented.

State model. This is the composite atomicity model of computation (cf. [START_REF] Dijkstra | Self-stabilizing Systems in Spite of Distributed Control[END_REF][START_REF] Ghosh | Distributed Systems: An Algorithmic Approach[END_REF]) in which the nodes communicate by reading the variables', but not constants', values directly in the states of their neighbors. That is, each node can read its own variables and those of its neighbors, but can write only to its own variables. Constants cannot be directly read by a neighbor. This is for being able to keep confidential a sensitive information of a node (like the preference list).

Register model. In Chapter 5, we adopt the link register communication model (cf. [START_REF] Dolev | Self-stabilization of dynamic systems assuming only read/write atomicity[END_REF]). Each process is associated with a set of atomic registers, each of size of O(1) bits (our algorithm does not require more space). For each adjacent node u, the node v shares a register r v,u in which v is the only node allowed to write and that u can read. Each register is a record with several fields. The field var in the register r v,u is named var v,u .

The Figure 3.2 shows the characteristics of the register model. As for the state model, the variables of the node v are read and written by v. The difference with the state model is the read access of the neighbors. Indeed, j can read sv1 v,j and sv1 u,j (similarly sv2 v,j , and sv2 u,j ) while i can read sv1 v,i and sv1 u,i (similarly, sv2 u,i and sv2 u,i ). Notice that, at the starting configuration, a shared variable sv1 v,j may be outdated in the correspondence with the local state of v, before v is activated and writes into it. This is impossible in the state reading model, since a neighboring node reads the local memory of v directly.

u v i j local variables lv1v lv2v shared variables sv1 v,j sv2 v,j sv1 v,i sv2 v,i local variables lv1 j lv2 j shared variables sv1 j,v sv2 j,v sv1 j,u sv2 j,u local variables lv1 i lv2 i shared variables sv1 i,v sv2 i,v sv1 i,u sv2 i,u local variables lv1u lv2u shared variables sv1 u,j sv2 u,j sv1 u,i sv2 u,i

VI -Self-stabilization

The notion of self-stabilization [START_REF] Dijkstra | Self-stabilizing Systems in Spite of Distributed Control[END_REF] is related to transient failure tolerance. Corruptions of variables1 may put the system in an arbitrary configuration, from which the algorithm has to recover. Formally let A be a distributed algorithm, C the set of its configurations and E the set of its executions from any configuration in C. A (specification of a) problem is a predicate Prob on executions. For any execution of a self-stabilizing algorithm A, whenever Prob is satisfied, we say that A has stabilized.

On the Figure 3.3, the rectangles represent configurations of a system (in C). Green rectangles are legitimate configurations (in L). Orange rectangles are non-legitimate configuration (in C \ L). Arrows are the possible transitions from a configuration to another. From non-legitimate configurations, the execution reaches eventually a legitimate configuration. Furthermore, from a legitimate configuration only legitimate configurations are reachable: this is a particular case of stabilization.

All system configurations

Legitimate configurations

Stabilization (for Prob)

Figure 3.3: Self-stabilization

In the context of stable marriage, the predicate Prob defining the problem is satisfied by an execution iff a) the execution reaches a terminal configuration (i.e., a configuration in which no node is eligible), and b) this configuration contains a stable marriage (i.e., all nodes are married and there is no BP).

VII -Time Complexity

The time complexity of a self-stabilizing distributed algorithm can be evaluated in terms of moves, steps or asynchronous rounds (see Definition 4). The stabilization time, counted in moves (respectively in steps or in rounds), is the maximum number of moves (resp. steps, rounds) until a configuration in L is reached, starting from an arbitrary configuration. The stabilization time in moves gives an upper bound on the stabilization time in steps and rounds.

Asynchronous rounds. Asynchronous rounds (or simply rounds in the following) have been introduced in [DIM97] and extended with the concept of neutralization [START_REF] Bui | Snap-stabilization and PIF in tree networks[END_REF]. A process v is said neutralized during a step

C i → C i+1 , if v is eligi- ble in configuration C i but not in configuration C i+1 ,
and is not activated in the step C i → C i+1 . The rounds are inductively defined as follows.

Definition 4 (Asynchronous rounds). The first round of an execution e = (s 0 , C 0 ), (s 1 , C 1 ), . . . is the minimal prefix e = (s 0 , C 0 ), . . . , (s j , C j ), such that every process that is eligible in C 0 either executes a rule or is neutralized during a step of e . Let e be the suffix (s j , C j ), (s j+1 , C j+1 ), . . . of e. The second round of e is the first round of e , and so on. In this chapter, we present our first solution to SMP. This work is published [LMB + 17] and received a best paper award. At the time of publication, it was the first self-stabilizing distributed solution for general SMP. The algorithm is designed for the model of composite atomicity (state reading model), under an unfair distributed scheduler (see Chapter 3 for definitions).

We first present an historical background and explain how this algorithm is obtained, in Section I. Then, in Section II, we present the solution. In Section III, the proof analysis is provided in two steps. We first sketch the proof in Sub-section III.1 and in Sub-section III.2, we provide the formal proof of correctness and a time complexity analysis, providing an upper bound in terms of moves and steps. Finally, we conclude this chapter with some remarks and perspectives (Section IV).

I -Preliminaries and Contribution

Even though the original stable marriage algorithm by Gale and Shapley (GSA) is essentially centralized, it can be interpreted as a distributed one [START_REF] Brito | Distributed stable marriage problem[END_REF] and most of the existing distributed algorithms rely on GSA. In general, the algorithm proceeds by iteratively realizing proposals, e.g., by women, and acceptances, e.g., by men (or vice-versa). Intuitively speaking, the algorithm creates matches and resolves appearing BPs, when improving iteratively the quality of the matches according to the preferences ("better match" dynamics). But, GSA does not necessarily converge towards correct configurations from any initial configuration. In other words, it does not naturally tolerate transient failures that can put a system in an arbitrary configuration, i.e., it is not self-stabilizing. In particular, from some configurations, BPs can appear and not been eliminated during the execution. Thus the issue of their elimination in a self-stabilizing context naturally appears.

SMP has received a lot of attention, in particular by Knuth [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF]. When investigating combinatorial properties of the problem, Knuth discovered the possibility of cycles when resolving BPs (in a specific way) from some initial configurations with an incomplete or unstable matching.

The Figures below show an example of such a cycle. The pair (Jane, M ark) is a BP, i.e. the marriage is unstable. Knuth proposes to resolve the BP by exchanging the partners of the pair. Here, M ark and Jane are married together and their former partners, Zoe and John are married together (Figure 4 In the reached system, the marriage is still unstable: the pair (Jane, Scott) is a BP (Figure 4.2.a). After the repair (in the same way as previously), the system is as in Figure 4.2.b. 11] works in two phases. In the first one, only married women make proposals for improving their marriages. When no married woman can improve anymore, the second phase starts. In this phase, only unmarried women can make proposals (until they all are matched). At the end of this phase, a stable marriage is obtained (after at most O(n 2 ) steps). In a distributed context, being able to start from an arbitrary matching is not sufficient to be self-stabilizing, for the reasons that we explain below. Nevertheless, it is a first step towards self-stabilization, and it is the reason why we adopted the idea of the two phases, like in [AGM + 11].

Making this idea work in a distributed asynchronous and self-stabilizing way is still very challenging. First, there is a need of a sort of synchronization of phases between the nodes that cannot move all together to the next phase, like in the centralized case. Then, termination detection is needed for detecting the end of the first phase. Furthermore, Ackermann et al. supposed "best response" dynamics, contrary to the "better" ones in a distributed GSA. "Best response" dynamics are inherently centralized too, since creation or suppression of a match is not instantaneous (as it is in the centralized case) and the actual matches can change during the delay for realizing these actions. Hence, it is difficult to implement perfect "best response" dynamics. Finally, notice that a distributed matching has to be encoded with pointers that can be badly initialized. This is not taken into account in the algorithm of Ackermann et al..

In addition to these difficulties, we strive to provide a truly decentralized solution using neither leader nor global reset and detecting and correcting faults locally (similarly to the way GSA resolves BPs). This rules out the known self-stabilizing automatic transformers requiring such type of primitives. On the positive side, this allows obtaining more efficient algorithms in terms of time and space. This is also the reason for not using known synchronization techniques (e.g., [AKM + 07], [START_REF] Boulinier | When graph theory helps selfstabilization[END_REF]). The proposed algorithm works with only one additional phase of synchronization (in addition to the two phases in the strategy of Ackermann et al.), while using known synchronization techniques would result in much more additional phases. On top of that, it ensures a sort of confidentiality, in the sense that the preference lists of the nodes are not public1 . Notice that keeping the complete preference lists of users secret may be an important requirement, for instance in some economic contexts. This goal cannot be achieved by any centralized solution.

The proposed algorithm works under an unfair distributed scheduler, i.e., choosing at each step a non-empty subset of nodes that have actions to perform (i.e., enabled nodes; see model Section V in Chapter 3 for a formal definition). In spite of all the aforementioned difficulties, we design (Section II) and prove (Section III) such a self-stabilizing stable marriage algorithm (which also guarantees confidentiality of the preference lists). The sketch of its proof is in Sub-section III.1 and the details in Subsection III.2 The time complexity analysis provides an upper bound of O(n 4 ) moves (activations changing the state of a node). Straightforwardly, this upper bound applies to steps (activations changing the configuration of the system; see the model section). Note that, in Chapter 6, we also study how the proposed algorithm can be useful for obtaining self-stabilizing solutions to some variants of the stable marriage problem. The results (variants included) have been submitted to a journal.

II -Self-stabilizing Solution to SMP

The solution of Ackermann et al. proceeds in two phases. In the first phase, already married women try to improve their marriage as in the example of Figures 4.5 -4.7. In this example, married women are green. In the initial configuration (Figure 4.5.a), there is only one BP: (Zoe, John). In the Ackermann et al. algorithm, resolving a BP means to match the BP but, contrary to Knuth, former partners become single. After resolving the BP (Zoe, John) leads to a configuration (Figure 4 When no improvement (i.e., no resolution of BP) is possible, phase 2 starts. In the second phase, single women (in blue in Figure 4.7.a) try to be married, using the Gale and Shapley's mechanism: they propose to men in their preference list's order. If a married man receives a better proposal, he accepts the proposal and divorces from his actual spouse, who becomes single and, then, proposes in her preference list's order. In this example, Jane is the only single woman and she proposes to M ark, her first choice. When all single women are married, the final stable marriage is reached ( In the first phase, women globally reduce their regrets, i.e., increase the quality of their matching, and in the second phase, men do symmetrically the same. The algorithm is correct, even when started from an incomplete matching, but is not self-stabilizing in the strict sense, because all nodes must start in phase 1 and change simultaneously to phase 2. That is, some possible configurations cannot appear in an execution, while self-stabilization has to recover from any starting configuration. It could be made self-stabilizing using centralization, with the implementation of an incorruptible global phase counter. In a distributed asynchronous setting, things are more difficult. The distributed self-stabilizing solution that we propose takes the idea of two phases, but use a supplementary phase for the purpose of synchronization. We number the phases 1, 1.5 and 2. Phases 1 and 2 play about the same role as in Ackermann et al.'s algorithm.

Phase 1.5 is an intermediary phase performing synchronization between phase 1 and 2 (due to an erroneous initial configuration). During phases 1 and 2, women have the initiative to propose marriage, men can only choose among the different proposals. We start by explaining the role of phases when all nodes are initially in phase 1. The transition from phase 1 to phase 1.5 is realized first by women who have checked the lack of BPs. Once all women are in phase 1.5, men can change to phase 1.5 if they do not detect BPs. Otherwise, the detecting man blocks the process (by staying in phase 1). When the woman involved in the BP is activated, it changes its phase to 1 (forcing a come back to phase 1 for all men). It is only when all nodes reach phase 1.5 that women can move to phase 2. Then, men follow by moving to the phase 2 too. The verification of the absence of BPs before entering phase 1.5 guarantees their absence at the beginning and during phase 2. Now we precise how self-stabilization is obtained. When a faulty configuration is detected, nodes can move from phase 2 to phase 1. For example, this happens if it is detected that some pointers are badly initiated, if the phase number of a man is greater than the one of a woman, or if some phase values are not consecutive. This move can also be initiated by a married woman in phase 2, who detects a possible improvement (i.e., a BP since the woman is married). All other nodes will detect the phase change and move to phase 1 too.

We will show that no execution cycles more than one time through the phases 1, 1.5, 2. Similarly to the algorithm of Ackermann et al., we show that, during the last execution of the first phase, the regrets of the married women are globally decreasing. This ensures that no BP exists at the end of this phase. During the last execution of phase 2, it is the same for the regrets of men and, thus, no BP can appear (even though the matching can be still incomplete). At the end, in O(n 4 ) moves in overall, a complete stable marriage is obtained.

II.1 -Algorithm Implementation

We now make precise the implementation of these ideas. Each node v has variables and constants. The variables can be read by the neighbors, but the access to constants is limited, for the confidentiality reasons that we explained before.

II.1.1 -Variables, Constants, Functions and Predicates (for a node v)

Variables.

• marriage ∈ N (v) ∪ Null: if the value is not Null, we say that it is the spouse of v. Otherwise we say that v is single.

• proposal ∈ N (v) ∪ Null: if v is a woman, we say that this is the node to whom v has proposed; if v is a man, this is the woman whose proposal has been accepted by v. If the value is Null, we say that there is no proposal or acceptance.

• phase ∈ {1, 1.5, 2}: v is said to be in phase α if v.phase = α.

Constants.

• pref : the v's list of its n neighbors in preference order. The priority of the i th element of the list is i. Then, the first element is the most preferred neighbor and its priority is 1.

Observe that pref is an ordered list that exactly contains all the elements in N (v).

Recall that the lists of preferences are kept secret. A node v only communicates to its neighbor u the priority it gives to u and the priority of its actual spouse. If v is single, the latter is n + 1.

Functions.

• priority(v,u): returns the priority of u in the preference list of v. Note that if parameter u is evaluated to Null, priority(v,u) = n + 1 (v is single).

• min(A): returns the most preferred node in a set A of nodes Let C v be the set of nodes which prefer v and are preferred by v:

C v = { u ∈ v.pref : priority(v,u) < priority(v,v.marriage) ∧ priority(u,v) < priority(u,u.marriage) }
The following function is used by women to determine which man to propose to.

P v = {u ∈ C v : u.proposal = v ∧ u.phase = v.phase ∧ [(u.marriage = Null ∧ u.phase = 1) ∨ (u.marriage = Null ∧ u.phase = 2)]
The following function is used only by men to determine which proposal to accept.

• BestProposal(v) = if (P v = ∅) then return min(P v ) else return Null

Predicates.

The solution that we propose uses predicates for testing locally some properties. The predicate Married(v) is used by a woman v for checking whether she is reciprocally married (True), or not (False).

• Married(v) ≡ (v.marriage = Null) ∧ [(v.marriage.marriage = v) ∨ (v.marriage.proposal = v)] • MarriedM(v) ≡ (v.marriage = Null) ∧ (v.marriage.marriage = v)
The predicate Response(v) checks if the proposal of v has been accepted.

• Response(v) ≡ (v.proposal = Null) ∧ (v.proposal.proposal = v)
The predicate AlreadyEngaged(v) is used by a man to detect if he already accepted a proposal.

•

AlreadyEngaged(v) ≡ (v.proposal = Null) ∧ [(v.proposal.proposal = v) ∨ (v.proposal.marriage = v)]
Since there is an asymmetry between women's proposals and men's acceptances (women ask first for a marriage and then men answer), they have different predicates to verify whether their pointers are correct and, in particular, that their marriages are reciprocal (suffix W in the predicate name refers to women and M to men). Otherwise, the predicate is False and pointers are said incoherent.

• IncoherentPointersW(v) ≡ (v.marriage = Null) ∧ [((v.marriage.marriage = v) ∧ (v.marriage.proposal = v)) ∨ (v.marriage = v.proposal) ∨ (v.marriage.proposal = v ∧ priority(v.marriage,v) > priority(v.marriage,v.marriage.marriage))] • IncoherentPointersM(v) ≡ (v.marriage = Null) ∧ [(v.marriage.marriage = v) ∨ (v.marriage = v.proposal)]
Since the definition of BP is asymmetrical (cf. Remark 1), there are two predicates for checking the presence of BP (which involves a married woman). Hence, if at least one of these two predicates is True, that indicates there is a BP. If a node detects a BP, we say that it is involved in a BP.

•

BlockingPairW(v) ≡ Married(v) ∧ (C v = ∅) • BlockingPairM(v) ≡ (∃u ∈C v : u.marriage = Null)
The following predicate, AllCoherentPhase(v), checks some coherence in phases, namely whether v and all its neighbors are in phase 2, or v is in phase 1 and all its neighbors in phases 1 or 1.5. It is used only by men to decide if they can accept a proposal (women verify somewhat different conditions).

• AllCoherentPhase(v)

≡ (v.phase = 2 ∧ (∀u ∈N (v): u.phase = 2)) ∨ (v.phase = 1 ∧ (∀u ∈N (v): u.phase ∈ {1, 1.5}))

II.1.2 -Algorithm.

The matching M built by the presented algorithm is defined by pairs (w, m) ∈ E such that w.marriage = m and m.marriage = w.

The algorithm predicate is Pred2Phases ≡ [∀w ∈Women: Married(w) ∧ ¬BlockingPairW(w) ∧ ¬BlockingPairM(w.marriage)] and for the proof of self-stabilization, we define the legitimate configurations as the configurations satisfying this predicate. Notice that executions satisfying Pred2Phases satisfies also Prob.

The part of the algorithm executed by women (Algorithm 1) has 9 rules. We start by describing intuitively what those rules do.

1. The Reset rule performs a reset of marriage and proposal pointers, if these pointers appeared to be incoherent according to IncoherentPointersW.

2. The rule BadInit is executed by a woman in phase 2. In this phase a married woman is not supposed to make a proposal. Thus, if her proposal and marriage pointers are not set to Null (the only reason for that is a bad initialization), BadInit resets the proposal pointer and sets the phase to 1 (to restart the computation of a matching).

3. The rule Propose1 (respectively Propose2) is executed by a married (resp. single) woman in phase 1 (resp. 2). This rule's effect is a proposal to the man who corresponds to the best marriage for her (i.e., best for the woman but also for the man with respect to its actual spouse or single status).

4. The rule Confirm1 (resp. Confirm2) is executed by a married (resp. single) woman in phase 1 (resp. 2), after she has made a proposal to a man and this proposal has been accepted (the man has put the name of the woman in its variable proposal). Then, the woman confirms the marriage, breaking from her previous man (only Confirm1) and matching with the new one. The couple is now considered married.

5. The rule ToPhase1.5 is a phase transition rule from phase 1 to phase 1.5. When a woman in phase 1 cannot make any proposal (no BP is detected or she is single), she has to move to phase 1.5 if all men are in phase 1.

6. The rule ToPhase2 is also a phase transition rule. A woman in phase 1.5 can change to phase 2 if she does not detect any BP and if all men are in phase 1.5.

7. The rule ToPhase1 is the third phase transition rule. It is executed by a woman in order to move from phase 2 or phase 1.5 to phase 1. The change happens if the following (faulty) conditions are detected: (a) the woman is in phase 2 but some man is in phase 1 (either a BP has been detected or phase synchronization has not stabilized yet); (b) the woman is in phase 1.5 but a man is in phase 2 (the phase synchronization has not stabilized yet); (c) the woman is married and either in phase 1.5 or 2 but detects a BP.

Remark 2. If a man m does not answer positively to a proposal from a woman w (it has a better priority proposal), she detects it. BestMarriage(w) will not return m any longer and w can change her proposal with Propose1 or Propose2.

Algorithm 1 for w ∈ Women w.phase ← 1, w.proposal ← Null

The part of the algorithm executed by men (Algorithm 2) consists of 6 rules:

1. The Reset rule resets the marriage pointer of a man and changes its phase to 1.

We prove later that this can happen only once for a man in phase 2.

2. The Accept rule checks that women are in a consistent phase with respect to the phase of the man executing the rule (AllCoherentPhase), that the best proposal received is different from his actual partner and that he has not accepted another proposal (¬ AlreadyEngaged). Remark that this is a commitment, but the couple is not yet married. If the man is married to another woman, he has to break the marriage since he received a better proposal.

3. The role of the rule Confirm is to confirm a marriage. The rule checks that the phases are coherent (AllCoherentPhase) and if the woman has her variable marriage set to the man, he confirms too.

4. The rule ToPhase1.5 is a phase transition rule from phase 1 to phase 1.5. If all women are in phase 1.5 and no BP is detected, the man changes his phase to 1.5.

5. ToPhase2 makes men change to phase 2. When all women are in phase 2 and men have checked the lack of BPs, then phase 2 can begin.

6. The ToPhase1 rule detects a phase synchronization problem (a woman being in phase 1 or 1.5 with the man in phase 2) or a woman willing to change to phase 1 (a BP has been detected) when he is in phase 1.5. Then the man moves to phase 1.

Algorithm 2 for m ∈ Men

III -Correctness Proof and Time Complexity Analysis (Algorithms 1 and 2)

We have to prove that Algorithms 1 and 2 are self-stabilizing for the specification Prob of SMP. For that, we prove that any execution (from an arbitrary configuration) terminates in a configuration satisfying Pred2Phases. That establishes convergence and, as Pred2Phases ⇒ Prob, this property yields also correctness.

In the following Sub-section III.1, we sketch the proof. The detailed proofs can be found in Sub-section III.2.

III.1 -Sketch

The analysis of the algorithm appears to be complex for several reasons. First, the algorithm has to overcome the unfair adversary that can prevent some enabled nodes from being activated as long as there are other enabled nodes. This may take many moves made by nodes in different states and configurations. Moreover, all these moves may not contribute to the convergence (e.g., if an existing fault is not yet detected). Still, they have to be taken into account for the correctness and the time analysis. Another reason for the analysis difficulty is the distribution and asynchrony of the solution. For example, as mutual marriage, divorce, and blocking pair detection cannot be done instantaneously, or at least within some timing guarantees (as in synchronous lock-step models), the related results on previous centralized or synchronous solutions cannot be used in our case.

Finally, due to self-stabilization, the analysis has to consider executions starting from an arbitrary configuration. In particular, initially, the phase numbers can be arbitrary. Moreover there are specific rules applying to such or such phase number. The consequence of that is a great number of cases to treat, each case necessitating a particular treatment and special arguments. For classifying the different cases into categories, the following definition is introduced.

Definition 5. We say that a configuration C is in (A, B, bp) iff, in C, the set of phase numbers of women is A, the set of phase numbers of men is B and there are bp blocking pairs. The configuration C is in (A, B, bp) × iff, in C, the set of phase numbers of women is included in A, the set of phase numbers of men is included in B and there are bp blocking pairs.

For example, we have the identity:

({a}, {b, c}, X) × ≡ ({a}, {b, c}, X) ({a}, {b}, X) ({a}, {c}, X)
. Furthermore, we denote by C 1W (resp. C 1M ) the set of configurations having at least one women (resp. one man) in phase 1 and we set C 1 = C 1W C 1M . We denote by C 1 the set of configurations where ∃ v ∈ V : v.phase = 1. C 1W and C 1M are sets of configurations in C 1 where, respectively, v ∈ Women and v ∈ Men.

We prove the correctness of the algorithm for every possible starting configuration type. We start by giving a skeleton, which allows to skip the countless cases of the detailed proof and which is sufficient for understanding its main ideas. Interested readers will find all the details in the following Sub-section (Sub-sect. III.2).

The first proposition states that any terminal configuration is legitimate (see definition in Sub-sect II.1.2) and in (2, 2, 0). Proposition 1. In a terminal configuration, the set of edges {(w, m) ∈ E : w.marriage = m ∧ m.marriage = w} is non-empty and is a stable matching. This configuration is in ({2}, {2}, 0).

Then, we study the convergence. Lemmas 7 -16 establish that from any configuration in C 1 , in O(n 4 ) moves, an execution reaches a configuration in ({1.5}, {1.5}, 0). That is made by showing that the sum of the regrets of married women is regularly decreasing. Notice that this property cannot be derived directly from a similar result for the centralized two-phased algorithm of Ackermann et al., since it is based on the "best response" dynamics that are used there (in phase 1). As already explained before, since marriages, divorces and detection of BPs cannot be done instantaneously under a distributed setting, it is difficult and costly to realize such dynamics.

Then, Lemmas 17 -29 and Proposition 2 below establish that every execution, starting in ({1.5}, {1.5}, 0), reaches a configuration in ({2}, {2}, 0). From there, in every reachable configuration, nodes are in phase 2. Recall that in a configuration ({2}, {2}, 0), there may be still unmarried nodes.

Proposition 2. Every execution takes O(n 4 ) moves to reach a configuration C in ({2}, {2}, 0). Moreover, every configuration reached from C is in ({2}, {2}, X) for X ≥ 0.

Proposition 2 ensures that the condition required by Proposition 3 (all nodes in phase 2) holds after O(n 4 ) moves. Proposition 3 concerns precisely a segment of execution, in which nodes stay in phase 2, and establishes a bound O(n 4 ) on the length of this segment. The bound is obtained by showing that the sum of the regrets of married men is strictly decreasing. Notice that, as before (for phase 1), this property cannot be directly derived from a similar result for the centralized two-phased algorithm of Ackermann et. al.. Then, by Proposition 3, from configurations in ({2}, {2}, X) for X ≥ 0, a terminal configuration is obtained in additional O(n 4 ) moves (this is proven through Lemmas 30 -37 and Corollary 1). Proposition 3. Let E be a sub-execution such that, in every configuration, all nodes are in phase 2. Nodes can execute at most O(n 4 ) moves in E.

III.2 -Detailed Proofs

In this section we prove the technical lemmas needed for Proposition 1 (Lemmas 1 -6), Proposition 2 (Lemmas 7 -29) and Proposition 3 (Lemmas 30 -37). The three propositions yields the main Theorem 1, as described in Sub-sect. III.1.

III.2.1 -Properties of the Terminal Configurations

We start by proving that terminal configurations are configurations in (2, 2, 0) (Lemma 5) by showing that in all other sets of configurations, there is at least one node eligible for a rule. Then, in Proposition 1, we prove that terminal configurations have a set of edges such that (w, m) ∈ E : w.marriage = m ∧ m.marriage = w is a stable marriage.

Lemma 1. Let C be a terminal configuration. For a node m ∈ Men (resp. w ∈ Women), IncoherentPointersM(m) (resp. IncoherentPointersW(w)) is False.

Proof. A node satisfying this predicate is eligible for Reset, whence a contradiction with the fact that the configuration is terminal.

Lemma 2. Let C be a terminal configuration and let

m ∈ Men. Then AllCoherent- Phase(m) is True in C.
Proof. Assume that AllCoherentPhase(m) is False, by contradiction. Then there exists a woman w ∈ Women such that:

1. if m.phase = 2 then w.phase ∈ {1, 1.5} 2. if m.phase = 1 then w.phase = 2
IncoherentPointersW(w) is False by Lemma 1. If w.phase ∈ {2, 1.5} then w is eligible for ToPhase1 since m ∈N (w) and because of points 1 and 2. If w.phase = 1 then m is eligible for ToPhase1. This contradicts the fact that the configuration is terminal.

Lemma 3. Let C be a terminal configuration and v be a node. If there exists a node u ∈N (v) such that v.marriage = u then u.marriage = v.

Proof. Assume first that v ∈ Men and that v.marriage = u ∈Women. If u.marriage = v, then IncoherentPointersM(v) is True, which is not possible in a terminal configuration, by Lemma 1.

Assume now that v ∈ Women, that v.marriage = u with u ∈Men and that u.marriage = v. Necessarily u.proposal = v or IncoherentPointersW(v) is True, which is not possible by Lemma 1. There are two cases.

• Assume first that u.marriage = Null. Then u is eligible for Confirm since priority(u,v) < Null. This yields a contradiction.

• Assume now that u.marriage = v 1 ∈ Women. Necessarily priority(u,v) > priority(u,v 1 ) or u is eligible for Confirm (since IncoherentPointersM(u) is False by Lemma 1 and that AllCoherentPhase(u) is True by Lemma 2). Observe now that the inequality priority(u,v) > priority(u,v 1 ) implies that IncoherentPointersW(v) is True. This is not possible by Lemma 1.

Lemma 4. Let C be a terminal configuration. No node is in phase 1 in C.
Proof. Assume by contradiction that there exists a node in phase 1, in a terminal configuration C.

We consider first the case in which there exists w ∈ Women in phase 1. Let m ∈ Men. IncoherentPointersM(m) and IncoherentPointersW(w) are False by Lemma 1. Observe now that m is in phase 1 or eligible for ToPhase1. Thus we can assume that all men are in phase 1 as well. There are two different cases for a woman w.

• She is married (Married(w) is True) and she forms a BP with some node m 1 ∈ Men. Assume without loss of generality that m 1 corresponds to BestMarriage(w).

Necessarily w.proposal = m 1 or w eligible for Propose1.

Observe first that BestProposal(m 1 ) = Null since w.proposal = m 1 and both are in phase 1.

-If m 1 .proposal = w then w is eligible for Confirm1 since Response(w) is True and IncoherentPointersW(w) is False, by Lemma 1. This yields a contradiction.

-Assume now that m 1 .proposal = w. First, AllCoherentPhase(m 1 ) is True by Lemma 2 and BestProposal(m 1 ) = Null. If AlreadyEngaged(m 1 ) is False then m 1 is eligible for Accept. Therefore assume that AlreadyEngaged(m 1 ) is True. This implies that there exists w 2 ∈ Women such that w 2 = m 1 .proposal and w 2 .proposal = m 1 or w 2 .marriage = m 1 . By definition of the predicate, w 2 = Null. Now m 1 .marriage = w 2 or Incoherent-PointersM(m 1 ) is True, which is not possible by Lemma 1. There are two cases.

First, if w 2 .marriage = m 1 and priority(m 1 ,w 2 ) < prior- ity(homme 1 ,m 1 .marriage) then m 1 is eligible for Confirm. If prior- ity(m 1 ,w 2 ) > priority(m 1 ,m 1 .marriage) then IncoherentPointersW(w 2 )
holds and w 2 is eligible for Reset which yields a contradiction. Thus consider the second case in which w 2 .marriage = m 1 . Observe first that w 2 is either in phase 1 or 1.5 or AllCoherentPhase(m 1 ) is False since m 1 is in phase 1. This is not possible by Lemma 2. We consider these two cases. * Assume first that w 2 is in phase 1. There are two sub-cases.

• w 2 is married with some node m 2 ∈ Men. If BlockingPairW(w 2 )
is False then w 2 eligible for ToPhase1.5. If it is True, then by definition of the predicate, the set C w 2 is not empty and BestMarriage(w 2 ) = Null. Recall also that w 2 .proposal = m 1 . Thus, if BestMarriage(w 2 ) = m 1 then w 2 eligible for Confirm1. Otherwise, if BestMarriage(w 2 ) = m 1 then w 2 eligible for Propose1. This yields a contradiction. • w 2 is not married by definition, BlockingPairW(w 2 ) is False. In that case, it is eligible for ToPhase1.5. This yields a contradiction. * Secondly assume that w 2 is in phase 1.5. If BlockingPairW(w 2 ) is False then it is eligible for ToPhase2. If it is True, it is eligible for ToPhase1. This yields a contradiction.

• She is single or married with no BP: ToPhase1.5 can be applied. Thus, in a terminal configuration C, women are not in phase 1. Assume now that ∃m ∈ Men with m.phase = 1 in C. Women can either be in phase 1.5 or 2 (since women are not in phase 1, as proved above).

If some woman is in phase 2, she is eligible for ToPhase1 since m.phase = 1. Thus we can assume that all women are in phase 1.5. If there exists a woman w such that BlockingPairW(w) is True, then she is eligible for ToPhase1. Thus, this predicate is False for every woman. There are two cases.

-Assume first that BlockingPairM(m) is True. Let w be the woman which forms a BP with m. Then, BlockingPairW(w) is True. This is not possible as shown above.

-Therefore assume BlockingPairM(m) is False.

Then, m eligible for ToPhase1.5, which yields a contradiction. Lemma 5. A terminal configuration is in ({2}, {2}, 0).

Proof. We prove this lemma by contradiction. Let C be a terminal configuration not in ({2}, {2}, 0). Since by Lemma 4 no node is in phase 1, we have that C is in one of the following sets:

1. ({1.5}, {1.5}, X) 2. ({1.5, 2}, {1.5}, X) 3. ({1.5, 2}, {2}, X) 4. ({2}, {1.5, 2}, X) 5. ({1.5}, {1.5, 2}, X) 6. ({1.5, 2}, {1.5, 2}, X) 7. ({1.5}, {2}, X) 8. ({2}, {1.5}, X) 9. ({2}, {2}, X), X > 0.
In case 1, all nodes are in phase 1.5. If X = 0 then women can apply ToPhase2. If X = 0 then the woman in a BP can apply ToPhase1.

In case 2, all women are in phase 1.5, men are in phase 1.5 or 2 (with at least one in each phase). Women in phase 1.5 are eligible for ToPhase1. The same holds for cases 6 and 8.

For cases 3, all women are in phase 2, men are in phase 1.5 or 2. If there are BPs, women in these pairs are eligible for ToPhase1. Otherwise, men in phase 1.5 are eligible for ToPhase2.

For cases 4, all men are in phase 2 and women are in phase 1.5 or 2. If there are BPs, women in these pairs are eligible for ToPhase1. Otherwise, women in phase 1.5 are eligible for ToPhase2.

For cases 5, all men are in phase 1.5 and women are in phase 1.5 or 2. If there are BPs, women in these pairs are eligible for ToPhase1. Otherwise, men in phase 1.5 are eligible for ToPhase2.

For cases 7, if there are BPs, women in these pairs are eligible for ToPhase1. Otherwise men are eligible for ToPhase2.

Finally consider configurations in ({2}, {2}, X), X > 0. Women which have a BP are eligible for ToPhase1. This concludes the overall proof. Lemma 6. In a terminal configuration, for every woman w, Married(w) holds.

Proof. Let C be a terminal configuration. By Lemma 5, C is in ({2}, {2}, 0). Assume by contradiction that there exists w ∈ Women for which Married(w) does not hold. This implies that there is at least one man m for which MarriedM(m) does not hold, since the graph is bipartite complete with the same number of men and women.

There are two cases. First, if m.marriage = Null then m is eligible for Reset since m.marriage.marriage = m by definition of MarriedM(m).

Then if m.marriage = Null, it can be also assumed that w.marriage = Null. Otherwise, by definition of Married(w), the disjunction w.marriage.marriage = w ∨ w.marriage.proposal = w holds, which implies that w is eligible for . Altogether, we can assume that m.marriage = w.marriage = Null.

We have first that C w , the set of nodes u such that (w, u) is a BP, is not empty, since both m and w prefer each other to their current (Null) marriage. Assume without loss of generality that m = BestMarriage(w). If w.proposal = m then w is eligible for Propose2. Thus assume that w.proposal = m, implying that BestProposal(m) = ∅. Thus let w 1 = BestProposal(m). If AlreadyEngaged(m) is False then m is eligible for Accept, which yields a contradiction. Then assume that it is True. By definition of this predicate, m.proposal = Null. Let w 2 such that w 2 = m.proposal. We also have by definition of AlreadyEngaged(m) that w 2 .proposal = m or w 2 .marriage = m.

In the second case, m is eligible for Confirm since priority(m,w 2 ) < m.marriage = Null. In the first case, if w 2 .marriage = Null then it is eligible for BadInit. Thus assume that w 2 .marriage = Null. If BestMarriage(w 2 ) is m then w 2 is eligible for Confirm2 and otherwise it is eligible for Propose2. This concludes the proof.

Proposition 1. In a terminal configuration, the set of edges

{(w, m) ∈ E : w.marriage = m ∧ m.marriage = w} is a stable marriage.
Proof. By Lemma 5, a terminal configuration is in ({2}, {2}, 0), which implies that there are no BPs in such a configuration. By Lemma 6 and Lemma 3 all nodes are matched.

III.2.2 -Convergence Proof

There are multiple techniques for proving the convergence of a self-stabilizing algorithm (Definition 3). Here we adopt a method introduced by Gouda and Multari [START_REF] Gouda | Stabilizing Communication Protocols[END_REF], called convergence stairs or sometimes attractors. The image of a stair describes well the method. For reaching the desired set of legitimate configurations, the algorithm proceeds step by step, and the proof consists in showing that, once one step has been reached, the following step will be necessarily reached too. In our case, the steps of the stair correspond to the sets of configurations resulting from Definition 5. This technique allows to compute an upper bound of the stabilization time, by adding the upper bounds of moves, necessary for going from one step to another.

Recall that C 1W (resp. C 1M ) denotes the set of configurations having at least one women (resp. one man) in phase 1 and that (b) or is eligible for ToPhase1 since at least one man is in phase 1.

C 1 = C 1W C 1M .

III.2.2.1 -Convergence to ({2}

Others rules cannot be applied since at least one man is in phase 1 and w in phase 2.

• A man m in phase 1 is eligible for Reset if IncoherentPointersM(m) = True.

• A man in phase 2 is eligible either for Reset if IncoherentPointersM(m) = True (after a Reset, m.phase = 1), or for Confirm and Accept. Indeed, if ∀w ∈Women:

w.phase = 2, if m.proposal = Null ∧ m.
proposal.marriage = m, m is eligible for Confirm. Furthermore, after this move, AlreadyEngaged(m) = False and, if a better woman is proposing to m, BestProposal(m) = Null. Thus, m can also be eligible for Accept.

• A man in phase 1.5 is eligible either for Reset or ToPhase2 (all women are in phase 2). Indeed, after a Reset, m.phase = 1 and m is no more eligible for ToPhase2. Reciprocally, after a ToPhase2, m cannot be eligible for Reset since IncoherentPointersM(m) = False for ToPhase2.

We enumerate all possibles sets of configurations with all women in phase 2 and we ount the number of moves in the corresponding executions:

A. ({1}, {2}, X ≥ 0): first at most n men's and n women's Reset (both do not change nodes' phases), then at most n women's ToPhase1. After these O(n) moves a configuration in C 1W is reached.

B. ({1, 2}, {2}, X ≥ 0): first, at most n women's Reset and n -1 men's Reset (men in phase 1). Furthermore, men in phase 2 can also be eligible for Confirm and/or Accept, that is at most 2n moves. After this moves, all remaining rules change the phase number. There are two cases that reach both a configuration in C 1W :

(a) all nodes are activated: at most n -1 men in phase 2 for Reset (if they had not been activated for Accept/Confirm) and at most n women for ToPhase1 after 4n -1 moves, that is O(n) moves.

(b) only men in phase 2 are activated (if they had not been activated for Accept/Confirm) for Reset and the reached configuration is in ({1}, {2}, X) and then, in C 1W (see the point A. for explanations) after O(n) moves.

C. ({1, 1.5}, {2}, X ≥ 0): at most n women and at most n -1 men in phase 1 can be activated for Reset. After that, there is four possible cases: (c) If some men in phase 1.5 are activated for Reset and/or some men in phase 1.5 for ToPhase2 (at most n -2 men altogether), a configuration in ({1, 1.5, 2}, {2}, X) is reached after O(n) moves. From there, C 1W is reached after at most O(n) moves (see the point D. for explanations except the transition to a configuration in ({1, 1.5}, {2}, X) since men in phase 2 have been activated for ToPhase2 and cannot be now eligible for Reset).

(d) at most n men are activated (for ToPhase2 or Reset) but also at most n women for ToPhase1, the reached configuration is in C 1W after at most O(n) moves.

D. ({1, 1.5, 2}, {2}, X ≥ 0): at most n women and at most n -2 men in phase 1 can be activated for Reset. Furthermore, at most n -2 men in phase 2 can be eligible for Accept and/or Confirm, that is at most 2n -2 moves. After that, there is four possible cases: Proof. In these sets of configuration, a women w in phase:

• 1.5 is eligible for Reset and ToPhase1 if ∃w ∈Women : w.phase = 2 or if BlockingPairW(w) = True.

• 2 is eligible for Reset and ToPhase1.

Since ∃w 1 , w 2 ∈Women : w 1 .phase = 2 ∧ w 2 .phase = 1.5, a man m in phase

• 1 is only eligible for Reset.

• 2 is eligible either for Reset or for ToPhase1.

• 1.5 is eligible for Reset.

We enumerate all possibles sets of configurations with all women either in phase 2 or 1.5 and count the moves in the corresponding executions:

A. ({1}, {1.5, 2}, X ≥ 0): after at most 2n Reset (men and women), only at most n -1 women are eligible (women in phase 2, for ToPhase1). Thus, after at most 3n -1 moves, that is O(n) moves, a configuration in C 1W is reached.

B. ({1, 1.5}, {1.5, 2}, X ≥ 0): after at most 2n -1 Reset (all men except one in phase 1.5 and n women), there is two cases:

(a) Either only the last man in phase 1.5 is activated for the Reset and a configuration in ({1}, {1.5, 2}, X) is reached after 2n moves. From there, by the point A., after O(n) moves a configuration in C 1W is reached.

(b) Or at most n -1 women (those which are in phase 2) and the last man in phase 1.5 are activated (respectively for ToPhase1 and Reset), that is 3n-1 moves, i.e. O(n) moves. The reached configuration is then in C 1W .

Hence, from ({1, 1.5}, {1.5, 2}, X ≥ 0) and after O(n) moves, a configuration in C 1W is reached.

C. ({1, 2}, {1.5, 2}, X ≥ 0): after at most 2n -1 Reset (all men except one in phase 2 and n women), there are two cases. Proof. Let us suppose, by contradiction, that starting from C, no C' in C 1W or ({1.5}, {1.5}, X) with X ≥ 0 is ever reached. Thus, women are only eligible for Reset. Indeed, since C 1W is not reached and women are in phase 1.5, ToPhase1 is not activated. ToPhase1.5 is not enabled since women are already in phase 1.5 and ToPhase2 is not enabled since all men are not in phase 1.5 (({1.5}, {1.5}, X ≥ 0) is not reached). Other rules are also not enabled because of women's phases.

Men have several enabled rules relying to their phases and to women's phases (that does not change since they are only eligible for Reset). A man m in phase:

• 1 is only eligible for Reset and for ToPhase1.5 if BlockingPairM(m) = False.

• 2 is eligible either for Reset or for ToPhase1.

• 1.5 is eligible for Reset or for ToPhase1 if BlockingPairM(m) = True.

Since women cannot change their phases and that there is no configuration in C 1W or ({1.5}, {1.5}, X ≥ 0), either a terminal configuration is reached or the execution reaches two times the same configuration (since the variables are bounded and if no terminal configuration is reached). By Proposition 1, the terminal configuration is in ({2}, {2}, 0). But since no man is eligible for ToPhase2, this case is impossible. Now consider the configuration that is reached twice. Because all rules change at least one value and the same configuration is reached twice, at least one node v sets the same values to variables twice. Since women are eligible only once for Reset, v / ∈ Women. If v.phase = 1, there are two cases. Either v is first activated for Reset and then for ToPhase1.5. But after this move, he is no more eligible (Reset not enabled because v.proposal = Null after ToPhase1.5). Or v is only activated for ToPhase1.5. In both cases, the variables of v have different values. If v.phase = 1.5, there are also three cases. Either v is first activated for Reset and then for ToPhase1.5. But after this move, v is no more eligible (Reset is not enabled because v.proposal = Null after ToPhase1.5), or it is only activated for ToPhase1, or it is activated for ToPhase1 and ToPhase1.5. In the first two cases, the variables of v have different values. For the third case, v has been activated for ToPhase1 because of a BP. If he is activated for ToPhase1.5, BlockingPairM(m) = False. This case happens if the woman w involved in the BP is now considered as single by v after a Reset (i.e. she was not married, but her marriage pointer was not Null). Then, v can have the same state after these two moves but w has now a new pointer value. If v.phase = 2, there are four cases. Node v is either activated for Reset and ToPhase1.5, for ToPhase1 and ToPhase1.5, only for Reset or only for ToPhase1. In this four cases, the phase number is not the same, i.e. the state is not the same. This lead to a contradiction. Note that, men can reach phases 1 or 1.5 from all phases. Thus, if ∀m ∈Men: BlockingPairM(m) = True, m.phase = 1.5 in C and if the two nodes involved in the BPs are not activated in the execution until C', all other men shift to phase 1.5, C' is in ({1.5}, {1.5}, X ≥ 0). Otherwise, at least a woman is activated and the configuration is in C 1W .

Thus, there is no execution not reaching a configuration in C 1W or in ({1.5}, {1.5}, X ≥ 0). Furthermore, women can only be activated for Reset and ToPhase1 and each man can at most be activated for 2 moves, that is O(n) moves in total.

Lemma 10. Let C be a configuration in C 1 . Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W or in ({1.5}, {1.5}, X ≥ 0). Proof. By definition of C 1 , in C, ∃ v ∈ V : v.phase = 1. Necessarily, v ∈ Men,
otherwise the configuration would be already in C 1W . Let us enumerate all possible sets of configuration in which C can be:

• C 1 where ∀ w ∈ Women : w.phase = 2. By lemma 7, a configuration in C 1W is reached after O(n) moves. In short, in O(n 2 ) moves, the execution reaches C'.

In the sequel, we consider a particular node and we enumerate its possible interactions with the perspective of determining upper bounds to their number. Naturally, there is a great number of cases to examine, but no one is complicated and its results come from a simple examination of the rules of the algorithm.

Let v be a node in phase 1. Firstly, consider the case of v ∈ Men. Other men may be in any phase. Let w be in Women. If its pointers are incoherent, w can be eligible for Reset . For the other rules, we consider the different sub-cases:

1. w.phase = 2: w is only eligible for ToPhase1 (one of its neighbors is in phase 1), BadInit and Reset. The first two rules set the phase of w to 1, after a Reset if necessary. Reset does not affect the phase value.

2. w.phase = 1.5: if w is involved in a BP, its is eligible for ToPhase1. Otherwise, w is eligible for Reset, ToPhase1 and ToPhase2. If w is eligible for ToPhase2, all men are in phase 1.5, but v could move to 1.5 from 1 only if all women are in phase 1.5 too, thus the configuration C'has been reached. Otherwise, w is eligible either for Reset or for ToPhase1. ToPhase1 sets w.phase to 1, after a Reset if necessary. Reset does not affect the phase value.

3. w.phase = 1: if some men are not in phase 1, w has no enabled rule except the Reset. Otherwise, w is eligible for:

• Reset only once. Indeed, after Reset w is single in phase 1 and cannot be married (propose or confirm) in this phase. • ToPhase1.5 only once and when w is single or married without a BP. In phase 1.5 and after man's Reset, w may detect a BP with this man. She is then eligible for ToPhase1. To be eligible again for ToPhase1.5, w has to propose, a man has to accept, and w then has to confirm. Till confirmation, w has to stay in phase 1 and all men have to be in phase 1. They cannot change their phase till confirmation of w. Moreover, a man can accept only if all women are in phase 1 or 1.5. Thus C' is already reached, contradicting the fact that w eligible for ToPhase1.5 for the second time before C' is reached. • Propose1: since w may propose only once to each man (and not to her spouse), w is eligible for this rule at most n -1 times. Indeed, if w propose to a man m, BestMarriage selects the best possible spouse. But if pointers of men are incoherent, w cannot detect the BP with a better spouse m 1 and propose to m. After the activation of m 1 for the Reset, she can propose. And this case may happen n -1 times.

• Confirm1: it is a special case of the previous case. Indeed, since women are not all in phases 1 or 1.5, men cannot accept a proposal. But in the configuration C, the proposal pointer of a man m can be already set to w.

Then, if w proposes to this man, w can also be eligible for Confirm1. Then, w has resolved a BP (because in the definition of C v , w checks if its proposal is also more interesting for m). Man m is eligible for Confirm when all women are in phase 1 or 1.5, that is the configuration C'.

The worst case is when all women are in phase 1 except one in phase 2 and men all in phase 1, because they can propose to men n -1 times. Indeed, each woman is eligible for O(n) moves. That is altogether, O(n 2 ) moves of women and then all women are either in phase 1 or 1.5. Now, let us consider the case of v ∈Women. Let us analyze the other nodes next moves. Let m ∈ Men. In all cases, m is eligible for Reset and then its phase is set to 1. Otherwise, if:

1. m.phase = 1, m has nothing to do. In fact, if m is eligible for Accept or Confirm, all men are in phase 1 because otherwise women could not propose or confirm a marriage. If all women are in phase 1 and there is an incoherent pointer, a woman possibly has her pointer of proposal to m and m is eligible for Accept, but the woman will not answer while all men are not in phase 1 (and then, the configuration is C'). Furthermore, if all pointers of a woman are incoherent (the two pointers are set to m for example) m cannot be eligible for these two rules because of the definition of P v . A man is eligible at most once for one of these rules.

2. m.phase = 2 or m.phase = 1.5, m is eligible for ToPhase1 if he was not eligible for Reset: one of his neighbors is in phase 1. If a woman in phase 2 proposes to m, m cannot accept (AllCoherentPhase(m) is False).

Then, a man is eligible for at most two rules. That is altogether O(n) moves after which men are all in phase 1. In short, in O(n 2 ) moves, the system reaches C'.

In the two following lemmas (Lemmas 12 and 11), we introduce a norm function and we precise conditions in which this function is strictly decreasing. A norm function is a function from a set of configurations into a well ordered set (ordered set with no infinite strictly decreasing sequence). If there exists a norm function on a subset of configurations, an execution on this subset either terminates or reaches a configuration outside the subset. Then exhibiting a norm function allows to prove that an execution does not remain indefinitely at the same step of a convergence stair. The considered norm function is based on the notion of regret ([Knu76, GI89]).

Let MarriedWomen(C) be the set of nodes v in Women that are married in the configuration C. Let R w (C) be the sum of the regret of nodes v in MarriedWomen(C):

R w (C) = v ∈ MarriedWomen(C) priority(v,v.marriage(C)) Lemma 12. Let C be a configuration in ({1}, {1, 1.5}, X > 0) × . Any execution start- ing from C takes O(n 2 ) moves to reach a configuration C' in ({1}, {1, 1.5}, Y ≥ 0) ({1}, {1}, Y ≥ 0) such that R w (C) > R w (C').
Proof. Let T be the transition C 1 → C 2 and let us consider moves such that R w (C 1 ) > R w (C 2 ). Note that Confirm1 is the only rule that decreases R w (C) (no rule increases the sum). Indeed, a woman w 0 is married if [(w 0 .marriage.marriage = w 0 ) ∨ (w 0 .marriage.proposal = w 0 )] (Married(w 0 )) and Confirm1 set her marriage pointer to a man m 0 if m 0 .proposal = w 0 (Response(w 0 )). Furthermore, BestMarriage(w 0 ) = w 0 .proposal checks if w 0 .proposal is the best man for w 0 in the current configuration. Then, if a woman is activated for Confirm1, she gets married with a new man, better ranked than its actual partner, i.e., decreases R w . Now, we consider all enabled rules in C that do not change R w and we count how many times each rule is enabled for each node. First, let m be in Men. Relying on its state and the state of the system , m is eligible for:

• Reset, once. Indeed, since Reset is enabled only if m.marriage = Null and sets m.marriage to Null between the two activations of Reset, m.marriage is set to some value. So m has been activated for Confirm (the only rule that sets m.marriage). Thus, if a man is eligible twice, a woman has been activated for Confirm1 and R w has decreased. Then, Reset is enabled only once.

• ToPhase1.5: m is eligible only if all women are in phase 1.5, BlockingPairM(m) = False and AlreadyEngaged(m) = False. Furthermore, m is eligible only once for this rule. Indeed, if m is activated twice for this rule (let us called this two transitions A and B), it means that before A and B all women were in phase 1.5. But between them, m has shift back to phase 1 (otherwise he would not be eligible the transition B). The only reason for which a woman shift to phase 1 between A and B is a BP. Moreover, she was in phase 1.5 for B. Then a BP has been resolved between A and B.

• ToPhase1: since men are eligible for ToPhase1.5 and there are X BP(s), at least one man (involved in a BP (m 1 , w 1 )) will stay in phase 1. Woman w 1 will be activated for ToPhase1 (BlockingPairW(w) is True). After this move, if m is in 1.5 he is eligible for ToPhase1, at most once between each resolved BP.

• Accept: there is a woman w such that w.proposal = m and her proposal is the best proposal for m in C, i.e. P v = w. Since P v is defined with respect to the preferences of the proposing woman and of m, m accepts only if the marriage is beneficial for both of them. If m is activated for Accept in C 0 such that C * → C 0 (such that C 0 * → C 1 ), m can be activated once again for Accept in C 1 , if a woman w 1 has been activated for Propose for m and that w is proposing to a better ranked man. Then, m is eligible O(n) times (for each woman).

• Confirm: when m confirms, m is already considered married (after Confirm1 of the woman). But he is not eligible twice, because it would implies a new marriage (and then a woman would have been activated for Confirm1).

Altogether, a man is eligible for at most O(n) moves, that is O(n 2 ) moves for all men. Now, let w be in Women. The 4 following rules may be enabled for w:

• Reset: if she is eligible for Reset, that means she is not married. She cannot be involved in a BP and she is at most eligible for another move: ToPhase1.5.

• ToPhase1.5: if she is single or not involved in a BP in phase 1. Woman w can be activated for this rule only once, otherwise it means she has gone back to 1 (because of a BP, see the next point). But if she is eligible again for ToPhase1.5, that means there are no more BPs.

• ToPhase1: if a woman w involved in a BP (BlockingPairW(w) is True) is in phase 1.5 (only once because of the previous point).

• Propose1: if BlockingPair(w) = True: she proposes to the best ranked man in C v . Woman w can be involved in at most n -1 BP(s) (if she is married with the worst ranked man), she can be eligible n -1 times for Propose1. Indeed, if, for a man m, IncoherentPointersM(m) = True, w cannot detect the BP (w, m). Then, she can propose to a first man m 1 before a man m 2 is activated for Reset and she detects the BP because m 2 is better ranked than m 1 ).

In overall, a woman is eligible for at most O(n) moves, that is O(n 2 ) moves for all women.

To summarize, nodes are eligible for at most O(n 2 ) moves before that at least one woman w is eligible for Confirm1. Men are in phase 1 (since there was a BP before w's Confirm1) and women are either in phase 1 or 1.5. Thus, C' is reached. Note that the number of BPs is now Y ≥ 0 but not necessarily Y < X: a BP (m, w) has been resolved but the previous spouse m 1 of w is now single. New BP(s) involving m 1 can appear after the resolution of the BP. Indeed, since single women in phase 1 or 1.5 cannot been eligible for Propose1, the case w.marriage(C) = Null and w.marriage(C') = m is not possible (Married(w)) in C is False). The first case appears if there is a BP (w 1 , m) for some woman w 1 : w 1 proposes to m (w 1 .proposal = m) and m accepts/confirms the proposal (m.proposal = w and then m.marriage = w). Then, w becomes single. We have R w (C) > R w (C') because w is now single and does not count any longer and w 1 diminishes her regret.

ToPhase1.5 is now enabled for w since she is no more married (and cannot belong to a BP) and, after that, for ToPhase2.

The second case happen if (w, m 1 ) is a BP: m 1 is better ranked by w than m. Woman w resolves the BP by making a proposal (w.proposal = m 1 ) and a confirmation (w.marriage = m 1 ). Then, R w (C) > R w (C'). Woman w cannot be married once again with m implying the existence of a BP (w, m), because m is worse ranked than m 1 : w cannot propose to m while she is married with m 1 (BestMarriage(w) = m). Then, if there is still a BP involving w, she improves again her regret but can still not be married again with m. When there is no more BP involving w, she is only eligible for ToPhase1.5 and ToPhase2 if all men are in phase 1.5.

In all stages that we considered up to know, the complexity in moves is an O(n 2 ). Now we arrive at the hard part, which will weigh on the global complexity and which is an O(n 4 ). The reason is simple: there can be O(n 2 ) BPs in a configuration and the resolution of a single BP may take O(n 2 ) steps. These O(n 2 ) supplementary steps with respect to Ackermann et al.'s algorithm is caused by the distribution. While the centralized algorithm resolves a BP in one action, the distribution, together with an adversarial unfair scheduler, makes that there can be some delay before the BP is effectively solved. It seems that nothing can be done against that, but trying a completely different approach. This other approach is the object of the next chapter, but presently, we continue with the analysis of the first algorithm.

Lemma 14. Let C be in ({1}, {1, 1.5}, X) × . Any execution starting from C takes O(n 4 ) moves to reach a configuration C' in ({1}, {1, 1.5}, 0) × .
Proof. Remind that ({1}, {1, 1.5}, X) × ≡ ({1}, {1.5}, X) ({1}, {1, 1.5}, X) ({1}, {1}, X). If X = 0, there is nothing to prove except if C is in ({1}, {1}, 0). Women are eligible for at most two rules: Reset and ToPhase1.5. Men can only be eligible for Reset. Then, if X = 0, after at most 2n Reset (men and women) and ToPhase1.5 (women), that is O(n) moves, the configuration C' is reached. Now assume X > 0. Let us determine an upper bound on X. Since there is a BP (w, m) only if w is married, w is involved in at most n -1 BP(s). Then, if each women is involved in n -1 BP, there are O(n 2 ) BP(s).

By Lemma 12, one BP is resolved in O(n 2 ) moves. Since each BP can be resolved at most once (Lemma 13), there is no more BPs after O(n 4 ) moves. When a woman w is activated to confirm (resolving the last BP (w, m) by setting w.marriage = m), all men are in phase 1 and at least w is in phase 1 too (AllCoherentPhase(w) in Confirm1). Other women are either in phase 1 or 1.5 (ToPhase2 cannot be applied since men are in phase 1). This configuration is in ({1}, {1, 1.5}, 0) × . Lemma 15. Any execution starting from a configuration C in ({1}, {1, 1.5}, 0) takes O(n) moves to reach a configuration C' ∈ ({1}, {1.5}, 0).

Proof. Consider the enabled rules in configuration C. Men are only eligible for Reset. Indeed, they are not eligible for Accept or Confirm. Even if there are woman's incoherent pointers, men cannot accept because of the definition of P v . Indeed, P v evaluates if the proposal is more interesting for both, the man and the woman and if the woman is married (if there exists still a BP). This yields to a contradiction with the fact that there is no more BPs in C by definition. Men are not eligible for Reset since they are already in phase 1 (men) and also not for ToPhase1.5 because of women in phase 1.

Women are eligible for Reset and ToPhase1.5 (women in phase 1). Indeed, since there are no more BP, no woman is eligible for Propose1 or even Confirm1. Concerning ToPhase1, women cannot be eligible, since there is no more BPs (women). ToPhase2 and BadInit are not enabled because of nodes' phases.

Thus, after at most 2n Reset, at most n -1 women are eligible for ToPhase1.5 (and men have no enabled rules), that is O(n) moves, the system reaches a configuration C' in ({1}, {1.5}, 0).

Lemma 16. Any execution starting from a configuration

C in ({1}, {1.5}, 0) takes O(n) moves to reach a configuration C' ∈ ({1.5}, {1.5}, 0).
Proof. Let us consider first women. They have no enabled rule except Reset since they are in phase 1.5 and not all men are in phase 1.5. Now, let us consider men. As women are in phase 1.5 and cannot change their phase, men are only eligible for ToPhase1.5. Furthermore, they are eligible for Reset. Notice that each man is eligible for Reset before ToPhase1.5 due to IncoherentPointersM.

Then, after 2n Reset (men and women) and n men's ToPhase1.5, that is O(n) moves, the configuration C'∈ ({1.5}, {1.5}, 0) is reached.

Lemma 17. In a configuration C in ({1.5}, {1.5}, 0) ({1.5}, {1.5, 2}, 0), women are enabled for rules in the following set {ToPhase2, Reset} and men are only enabled for Reset. Furthermore if C → C', then the configuration C' is:

• in ({1.5}, {1.5}, 0) ({1.5}, {1.5, 2}, 0) if only women's Reset are activated in the transition.

• in ({1.5}, {1.5, 2}, 0) ({1.5}, {2}, 0) if at least one women's ToPhase2 and no men's Reset is activated in the transition.

• in C 1 if at least one men's Reset is activated in the transition.

Proof. Let v be an eligible node in Men. By definition of C, v.phase = 1.5. Then, Accept, Confirm and ToPhase1.5 cannot be applied. Since there is no woman in phase 1 and v is in phase 1.5, v cannot be eligible for ToPhase1. Furthermore, as there exists at least one woman in phase 1.5, ToPhase2 is also not enabled. Thus, v is only eligible for Reset, if its pointers are incoherent. Now, let v be in Women. Because men's phase is 1.5, v cannot be eligible for Propose1, Confirm1, Propose2, Confirm2, BadInit and ToPhase1.5. ToPhase1 is also not enabled: there is no BP and there is no man in phase 1. Thus, the only possible rules for v are ToPhase2 (if v is in phase 1.5) and Reset (if its pointers are incoherent).

To sum up, if in the transition C → C' at least one man (Reset) is activated, the configuration C' is in C 1 . Otherwise, if only women are activated, C' is in (({1.5}, {1.5, 2}, 0) ({1.5}, {2}, 0) if at least one women's ToPhase2 is activated or in ({1.5}, {1.5}, 0) ({1.5}, {1.5, 2}, 0) if only women's Reset are activated. • in ({1.5, 2}, {2}, 0) ({2}, {2}, 0) if at least one men's ToPhase2 and no men's Reset are activated in the transition.

• in C 1 if in C if at least one men's Reset is activated in the transition.
Proof. Let v be an eligible node in Women. By definition of C, there exists at least one man in phase 1.5. Then, Propose1, Propose2, Confirm1, Confirm2 and BadInit cannot be applied. Since women are already in phase 2 and there is no BP, ToPhase2, ToPhase1.5 and ToPhase1 are also not enabled. Then, if the pointer of v is incoherent, v is eligible only for Reset (the marriage is not reciprocal), otherwise, women have no enabled rules. Now, let v be in Men. Because v.phase = 1, v cannot activate ToPhase1.5. Since women are in phase 2, ToPhase1 is also not enabled. Let us consider Accept and Confirm and the two possible cases:

• v.phase = 1.5. Because of AllCoherentPhase(v), these rules cannot be applied.

• v.phase = 2. If there is a woman w such that w.proposal = v, that Best-Proposal(v) = Null and if ¬AlreadyEngaged(v), v is eligible for Accept. But if v accepts the proposal and since the woman cannot answer in this configuration, there is no new marriage. Furthermore, if v is eligible for Confirm, he was already married (the woman had its identifier in her pointer of marriage). In any cases, that does not create a marriage and thereby also not a BP. Moreover, the phase of nodes activated for these rules is still 2.

Finally, we consider C', the new configuration after the transition from C. If at least one man has been activated for Reset, C' is in C 1 . If nodes have only been activated for Accept (men), Confirm (men) or Reset (women), C' is in ({1.5}, {2}, 0) {1.5, 2}, {2}, 0). Otherwise, if at least one man has been activated for ToPhase2 and none for Reset, C' is in ({1.5, 2}, {2}, 0) ({2}, {2}, 0).

Lemma 19. Any execution starting from a configuration

C in ({1.5}, {1.5}, 0) ({1.5}, {1.5, 2}, 0) ({1.5}, {2}, 0) ({1.5, 2}, {2}, 0) takes O(n) moves to reach a config- uration C' in ({2}, {2}, 0) or in C 1 after at least one men's Reset.
Proof. Let C be in ({1.5}, {1.5}, 0) ({1.5}, {1.5, 2}, 0). By Lemma 17, men are eligible only for Reset and women for Reset and ToPhase2. If at least one man is activated, the reached configuration is C' in C 1 . Otherwise, women are eligible for Reset (each woman at most once, since women cannot set their pointers) and for ToPhase2 (also at most once for each woman, since in phase 2 women are not eligible for ToPhase2). Thus, after O(n) moves, either a configuration in ({1.5}, {2}, 0) or in C 1 is reached. From ({1.5}, {2}, 0) ({1.5, 2}, {2}, 0), by Lemma 18, men are eligible for ToPhase2, Reset, Accept and Confirm and women are eligible only for Reset. If at least one man is activated for Reset, the reached configuration is C' in C 1 . Otherwise, at most n men are eligible for ToPhase2 and then, n -1 for Accept and Confirm. Furthermore, women are eligible for Reset (each woman at most once, since women cannot set again their pointers). Thus, after O(n) moves, a configuration in ({2}, {2}, 0) or in C 1 is reached.

In overall, from C, after O(n) moves, a configuration either in ({2}, {2}, 0) or in C 1 (if a man is activated for Reset) is reached.

Lemma 20. Let C be a configuration in ({1.5}, {1.5}, X) where X > 0. Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W .
Proof. Let us consider first a node v in Women. Since v is in phase 1.5 and all men are in phase 1.5, v is not eligible for Propose1/2, Confirm1/2 or ToPhase1.5. Since there are X BP(s), some women are involved in these BPs. Women involved in a BP are eligible for ToPhase1 and the others are eligible for ToPhase2 (because of BlockingPairW). Once they are in phase 2, while all men are in phase 1.5, they can do nothing. Node v is also eligible for Reset.

Let us consider now a node v in Men. Since v is in phase 1.5, he cannot be eligible for Accept, Confirm and ToPhase1.5. ToPhase1 and ToPhase2 are also not enabled: there are some women in phase 1.5 and others in phase 2 (after ToPhase2). Then v can only be eligible for Reset.

Thus, after at most n Reset (women) + (n -1) women's ToPhase2 the only enabled rule is ToPhase1 of a woman involved in a BP or a man's Reset. If only men are activated, C 1 is reached, but, after this shift to phase 1, men that are not involved in a BP can shift back to phase 1.5 (at most n -1). Women involved in a BP are still eligible. Thus, after at most n Reset (women) + (n -X) women's ToPhase2 + n men's Reset + n -1 ToPhase1.5, women involved in a BP are eligible and activated for ToPhase1. Then, after O(n) moves, a configuration C' in C 1W is reached.

Lemma 21. Let C be a configuration in ({1.5, 2}, {1.5}, X) ({1.5, 2}, {1.5, 2}, X) ({2}, {1.5}, X) with X ≥ 0. Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W or in ({1.5}, {1.5}, 0).

Proof. A common feature to the configurations specified in the statement is:

∃ w ∈ Women ∧ ∃ m ∈ Men : w.phase = 1.5 ∧ m.phase = 2
Let us consider first a node v in Men. Independently of phases, Reset can be enabled. Notice that if a man is activated for Reset, the configuration is immediately in C 1 . By lemma 10 and 20, after O(n) moves, the reached configuration is C 1W or ({1.5}, {1.5}, 0). Since there exists at least one woman in phase 1.5 and a man in phase 2, AllCoherentPhase(v) is False and Accept and Confirm are not enabled. For the same reason, ToPhase2 is also not enabled. Since nodes can only be in phase 1.5 or 2, ToPhase1.5 cannot be activated. Concerning ToPhase1, it can be enabled only if the node v is in phase 2 (because there exists a woman in phase 1.5) or if v is involved in a BP. In short, men in phase 1.5 are only eligible for Reset and men in phase 2 are eligible for Reset or ToPhase1 (any of this two rules is sufficient to reach a configuration in C 1 ). Now, let us consider a node v in Women. Independently of phases, Reset may be enabled. Then v cannot be eligible for Propose1, Confirm1, ToPhase2 and ToPhase1.5 because of men in phase 2. Since v and all men are not in phase 2 together, Propose2 and Confirm2 are not enabled. But if v is in phase 2, v may be activated for BadInit (and then the system reaches a configuration in C 1W ). Concerning ToPhase1, since there is at least a man in phase 2, all women in phase 1.5 are eligible. Married women involved in a BP in phase 2 are also eligible for this rule. To summarize, a woman v is eligible for • Reset.

• ToPhase1 (if v is in phase 1.5 or in phase 2 with a BP).

• BadInit (if v in phase 2).

So, after at most n Reset (women), women are only eligible for ToPhase1 or BadInit and men for Reset and ToPhase1. Then, after the next activation, that is altogether O(n) moves, the configuration is in C 1 . Furthermore, after lemma 10 and 20, we know that the execution will reach a configuration in C 1W or in ({1.5}, {1.5}, 0). Lemma 22. Let C be a configuration in ({2}, {1.5, 2}, X ≥ 0). Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W or in ({1.5}, {1.5}, 0).

Proof. Let us consider first a node u in Men. Independently of phases, Reset can be enabled. Note that if a man is activated for Reset, the system reaches immediately a configuration in C 1 . Since there exists at least one woman in phase 1.5 and no node in phase 1, AllCoherentPhase(u) is False and then Accept and Confirm are not enabled. Since men are in phase 2, ToPhase2 and ToPhase1.5 are also not enabled. Concerning ToPhase1, it may be enabled because a woman is in phase 1.5.

In short, men are only eligible for Reset or ToPhase1. (These two rules lead to a configuration in C 1 ). Now, let us consider a node u in Women. Independently of phases, Reset may be enabled. Let u.phase = 1.5. Then u cannot be eligible for Propose1/2, Confirm1/2, BadInit and ToPhase1.5 because of the phase of u. Moreover, because men in phase 2, ToPhase2 is also not enabled. Then, u is eligible for ToPhase1. Now, let u.phase = 2. Then, u cannot be eligible for Propose1, Confirm1, ToPhase2 and ToPhase1.5 (because of u's phase). In case of incoherence between proposal and marriage pointers, u is eligible for BadInit. But if she is activated for this rule, the system reaches a configuration in C 1 . Concerning Propose2, Confirm2 and ToPhase1, there are several cases:

• u is married: Propose2 and Confirm2 are not enabled. However, u can be activated for ToPhase1 if u is involved in a BP.

• u is single: u cannot be activated for ToPhase1, but for Propose2 and Con-firm2. We know that men cannot apply Accept or Confirm. But if proposal pointers are incoherent, a woman may propose to a man u and then confirm to u the marriage because of u's incoherent proposal pointer. Each woman may propose and confirm only once. Otherwise it would mean that m 1 , a man better ranked for u, has been discovered after u's Propose2 or Confirm2. But when u made her proposal to m, m 1 wasn't interesting for u (better marriage or incoherent pointers). In any case, this means that m 1 has been activated for Reset and then should be in phase 1. That is in contradiction with the fact that all men are in phase 2 and the system is now in a configuration in C 1 . Furthermore, this new marriage between m and u can create a new BP, but we will see later in this proof that the system will reach a configuration where a node is in phase 1.

To summarize, a woman u is eligible for

• Reset
• BadInit if u is in phase 2 with incoherence between pointers but the system reaches a configuration in C 1 .

• ToPhase1 if u is in phase 1.5 or in phase 2 with a BP.

• Propose2 and Confirm2 if u is in phase 2.

So, after at most n Reset (women), and n -1 Propose2 and Confirm2 (there is at most one woman in phase 1.5) moves, nodes are only eligible for rules that set their phase to 1 (ToPhase1, men's Reset and BadInit).

Then, after at most O(n) moves, the system reaches a configuration in C 1 . After Lemmas 10 and 20, from there, a configuration in

C 1W or in ({1.5}, {1.5}, 0) is reached in O(n) moves.
Altogether, that is O(n) moves to reach a configuration in C 1W or in ({1.5}, {1.5}, 0) from C. Lemma 23. Any execution starting from a configuration C in ({1.5}, {1.5, 2}, X > 0) takes O(n) moves to reach a configuration C' in C 1 ({1.5}, {2}, X > 0).

Proof. Let us consider first a node v in Men. Since there is at least one woman in phase 1.5 and one in phase 2, v can be only eligible for Reset. After his move, the reached configuration is in C 1 . Now, let us consider a node v in Women. There are several cases:

• v is eligible for Reset if she has incoherent pointers (IncoherentPointersW(v) = True).

• If BlockingPairW(v) = True and v.phase ∈ {1.5, 2}: v is eligible for ToPhase1. This rule change v' phase.

• If BlockingPairW(v) = False and v.phase = 1.5, she is eligible for ToPhase2. This rule sets 2 in v.phase.

Let us say first that all women in phase 1.5 (at most n -1) are not involved in a BP. They are enabled for ToPhase2. There are two cases:

• All women not involved in a BP (at most n -1) are activated first for Reset.

Subsequently, women in phase 1.5 (at most n -1) are activated for ToPhase2. Thus, a configuration in ({1.5}, {2}, X) is reached after at most 2n -2 moves, that is O(n) moves.

• If other nodes are activated in the same transition (of the previous point) that women are activated for ToPhase2 (i.e. at most n -1 men for Reset and the rest of women, i.e. 1 here, for ToPhase1), a configuration in C 1 is reached after at most 3n -2 moves, that is O(n) moves.

Now, let us say that women in phase 1.5 are involved in a BP. These women cannot shift to phase 2. As previously, women not involved in a BP (at most n-1) are activated first for Reset. And after that, in the same time, n -1 men are eligible for Reset, 1 for ToPhase1 and n -1 women for ToPhase2. A configuration in C 1 is reached after at most 3n -2 moves, that is O(n) moves.

Lemma 24. Any execution starting from a configuration C in ({1.5}, {2}, X > 0) takes O(n) moves to reach a configuration C' in C 1 or in ({1.5, 2}, {2}, X > 0).

Proof. Let us consider first a node v in Men. Since, in C, ∀ w ∈ Women, w.phase = 2, men are eligible for two rules: either Reset or ToPhase2 (if BlockingPairM = False). Both rules change nodes' phase (to 2 or 1): if a man is activated for one of these rules, the reached configuration is either in C 1 (one Reset has been executed) or in ({1.5, 2}, {2}, X) (one ToPhase2 and no Reset have been executed). Now, let us consider a node v in Women. Node v can be eligible for Reset or, if v's BlockingPairW is True, ToPhase1, but not for both in the same time. ToPhase1 changes nodes' phase. After at most n women's moves, the reached configuration is in C 1 (n -1 Reset and one ToPhase1).

Then, after at most 3n moves, (n women's Reset, n women's ToPhase1 and n men's Reset or ToPhase2), that is O(n) moves, the configuration is either in C 1 (if at least a man is activated for Reset or a woman for ToPhase1) or in ({1.5, 2}, {2}, X > 0) (if women are only activated for Reset and men for ToPhase2).

Lemma 25. Any execution starting from a configuration C in ({1.5, 2}, {2}, X > 0) takes O(n) moves to reach a configuration C' in C 1 or in ({2}, {2}, X > 0).

Proof. Let us consider first a node v in Men. If v.phase = 1.5, v is eligible for several rules: Reset and ToPhase2 if BlockingPairM = True. If v.phase = 2, v is eligible for several rules: Reset, Accept and Confirm. In fact, if a woman w is proposing to v, v is eligible for Accept if w is the best proposal regarding his preference lists. In this case, since w cannot confirm in this configuration (at least one man is in phase 1.5), there is no new marriage. If v is eligible for Confirm, w.marriage = v and v.proposal = w i.e. they are already married (Married(w) = True). In any cases, that does not create a marriage and thereby also not a BP. Moreover, the phase of men activated for these rules is still 2. After the move of a man with one of these rules, the reached configuration is in C 1 (at least one Reset) or in ({1.5, 2}, {2}, X) (only ToPhase2, Accept and Confirm). Now, let us consider a node v in Women. Node v is eligible for Reset or BadInit if she has incoherent pointers, but not for both. Indeed, if v is activated for Reset, then her guard of BadInit is False (v.marriage and v.proposal are set to Null). And if BadInit is applied, that means that Reset was not enabled and after BadInit is still not enabled. There are two cases for other rules: 1. if BlockingPairW(v): v is eligible for ToPhase1, 2. otherwise, v is eligible for any rule. In any case, since there is at least one man in phase 1.5, v is not eligible for Confirm2 and Propose2.

Then, after at most n Reset of women, the enabled rules are men's Reset (at most n), men's ToPhase2 (at most n -X), women's ToPhase1 and BadInit. Then, either only ToPhase2 of men are applied (at most n -1) and the reached configuration is in ({2}, {2}, X) or at least one of the following rules are activated: men's Reset, men's ToPhase1, women's ToPhase1 or BadInit. In this case, the reached configuration is in C 1 .

In short, after O(n) moves, the reached configuration is either in ({2}, {2}, X) or in C 1 .

Lemma 26. Let C be a configuration in ({2}, {2}, X > 0). Any execution starting from a configuration C takes O(n 2 ) moves to reach a configuration C' either in C 1 or, if no man has been activated for Reset or woman for BadInit or ToPhase1, in ({2}, {2}, 0) .

Proof. Let us consider a woman w with ¬BlockingPairW. There are two cases:

• w is married without BP (i.e. Married(v) ∧ C v = ∅). Only BadInit can be executed if w.proposal = Null.
• w is single (i.e. v.marriage = Null). Then, w is eligible for the Reset, Propose2 and Confirm2.

After her Reset (if she needs one), she is eligible for Propose2. There is now also two cases. She proposes to m and we assume that w is the best proposal for m. Then m accepts the proposal and both confirm one after the other. In all cases, because of the definition of C v and P v , m decreases his regret (either he was single and is now married or he was married and is now with a better ranked spouse). If m was involved in a BP (w 1 , m), after this new marriage, the BP may be resolved. Indeed, if w has a better priority for m than w 1 , there is no more BP (w 1 , m). Note that the pair (w, m) was not a BP because w was single.

If each BP in C is resolved by a single woman, the number of BPs decreases and it cannot grow since men are only improving their marriage (BestProposal sets). Since there are O(n 2 ) possible matches, there are O(n 2 ) BPs. If all women make their proposals to each man in a BP, in at most O(n 2 ) moves, there is no more BPs and the configuration is then in ({2}, {2}, 0). If before resolving all the BPs, a married woman involved in one of them is activated (for ToPhase1) or a woman for BadInit or a man is activated for Reset, the system reaches a configuration in C 1 . Consider a subset of configurations C 2 in ({2}, {2}, 0) such that no man is eligible for Reset and ∀w ∈Women, w.proposal = Null ∨ (w.marriage = Null ∧ w.proposal = Null). Let us first consider that C 2 is in C 1 after a man's Reset. Thus, there is configuration C 1 such that C 1 → C 2 and, during this transition, a man m has been activated for Reset. Let us prove by contradiction that it is not possible. First, by definition of C, no man is eligible for Reset and there is no BP. Thus, First case, sub-case 1a, in T, m.marriage ← w with w.marriage = m. The only rule that set the marriage pointer of m is Confirm. But in the guard of this rule, w.marriage = m must be True. Therefore, the first case cannot happen. Sub-case 1b, in T, m.marriage ← w and m.proposal ← w. But no rule can set the two pointers to a value at the same time. Sub-case 1c, in T, m.marriage ← m.proposal with m.proposal = Null after the transition. Confirm is the only rule that set m.marriage ← m.proposal but also m.proposal ← Null. Thus, this transition is not possible.

Second case, sub-case 2a, in T, m.marriage.marriage ← Null. The only rule resulting in this action is the Reset. Thus, in C 0 , w is eligible for Reset because (w.marriage = w.proposal) (the condition (w.marriage.proposal = w ∧ priority(w.marriage,w) > priority(w.marriage,w.marriage.marriage)) cannot be True since m.marriage.marriage = m in C 0 ). Since in C, this condition is not True for w, this two cases have been constructed performing one or several actions. The first case, as previously for men, no rule can set both pointers to the same value at the same time, or in a consecutive fashion (guard of Confirm1/2). Sub-case 2b, in T, m.marriage.marriage ← m 1 . As for the previous sub-sub-case, women can assign a value to their marriage pointers only if all nodes are in phase 2, and thus, the configuration is already C 2 . Sub-case 2c, in T, m.proposal ← m.marriage with m.marriage = Null. The only rule that set m.proposal to a value with possibly m.marriage = Null is Accept. But, by definition of BestProposal(m), the value returned by this function cannot be the value of m.marriage if m.marriage = Null.

Thus, by contradiction, C 2 is in ({2}, {2}, 0). Now, let us prove that C 2 is in C 2 , i.e. in ({2}, {2}, 0) with the two following conditions: (a) no man is eligible for Reset and (b) ∀ w ∈ Women, w.proposal = Null ∨ (w.marriage = Null ∧ w.proposal = Null). Case (a), since there cannot have a transition to C 1 with a man's Reset before C 2 , in C 1 (such that C 1 → C 2 ), no man is eligible for Reset. Furthermore, men are eligible only for ToPhase2 and women for no action until all men are in phase 2. ToPhase2 sets only m.proposal to Null. Thus, m are not eligible for Reset after the transition, in C 2 (guard of Reset depend on m.marriage). Finally, since in phase 2, no woman is eligible for any rule (until all men are also in phase 2 i.e. in C 2 ) and that the last actions of these women are ToPhase2, m.proposal = Null.

Thus But since in C, at least one woman w is in phase 1, and since w is in phase 1.5 in C 2 , she has been activated for ToPhase1.5 in a transition T:

C 0 → C 1 such that C * → C 0 → C 1 * → C 2 . Furthermore, since the condition for ToPhase1.5 is ∀ v ∈ N (w) ∪ {w} : v.phase = 1, in C 0 all
men are in phase 1. Thus, in the sub-execution C 1 * → C 2 , men are activated for ToPhase1.5 (they are in phase 1.5 in C 2 ). Then, C 2 is in ({1.5}, {1.5}, 0) and men have been already activated and are no more eligible for Reset. But, notice that women are possibly eligible for Reset. If a woman is eligible because of the condition w.marriage.marriage = w ∧ w.marriage = w.proposal, after her Reset, the man w.marriage is eligible for Reset. Other conditions does not break a reciprocal marriage and, thus, men are not eligible for Reset afterward. Then, man w.marriage shifts back to phase 1 (possibly with a woman that was in phase 2) and goes back again to phase 1.5. Thus, there is a loop between these configurations until there is no more woman eligible for Reset because of this condition. This can happen at most n times because women's Reset set pointers to Null. Indeed, after a Reset, women are in phase 1.5 and cannot set their pointers until phase 2.

Therefore, let us consider the last configuration in ({1.5}, {1.5}, 0) where ∀ w ∈ Women : w.marriage.marriage = w ⇒ w.marriage = w.proposal and no man is eligible for Reset. From this configuration, by Lemma 27, a configuration D in C 2 is reached.

Lemma 29. Every configuration reached from a configuration

C in C 2 is in C 2 .
Proof. Let us prove the result by induction. Let T be a transition C → C'. Notice first that in this transition, no node can change its phase value: men are not eligible for Reset, women are not eligible for BadInit nor ToPhase1 (there are no BP or incoherent phases). Other rules (men's ToPhase1, ToPhase1.5 and ToPhase2) are not enabled because of nodes' phases. Now, let us analyze all possible moves in T and their effect. First, since women are in phase 2, they are eligible for either Propose2, Confirm2 or Reset. Let w be a woman. Since there is no BP and if w is (reciprocally) married, she is not eligible for any rule. If w is single, there are two cases for C: either 1. w.proposal = Null or 2. w.marriage = Null ∧ w.proposal = Null.

In case 1, w can be eligible for Reset or Propose2. If w is activated for Reset in C, w.marriage = Null and either the marriage is not reciprocal ((v.marriage.marriage = v) ∧ (v.marriage.proposal = v)) or the man has a better marriage (v.marriage.proposal = v ∧ priority(v.marriage,v) > priority(v.marriage,v.marriage.marriage)) (other conditions cannot be fulfilled since w.proposal = Null). After this move, w.proposal = w.marriage = Null. Notice that no marriage has been broken: in both cases, the man is still married or single, but his marriage pointer does not point to w and, thus, man's Reset conditions are not True after w's Reset. Thus, the man is not eligible for Reset in C'. If w is not eligible for Reset and is activated for Propose2 after this move, the following conditions are still fulfilled: w.marriage = Null ∧ w.proposal = Null (see conditions of Propose2 (w.marriage = Null) and how this rule sets w.proposal). In the case 2, w is only eligible for Confirm2. After this move, the reached configuration is in C 2 (Confirm2 contains the following action: w.proposal ← Null). Since BestMarriage(w) = w.proposal is in the guard of the rule, w does not create any BP. Indeed, because all pointers are coherent, the predicate checks whether w is proposing to the best choice. If not, w is not eligible for Confirm2, thus, does not create a BP. Now, let us analyze men's moves. Men are eligible for Accept and Confirm. Let m be a man. Notice that both rules cannot create any BP. Indeed, a man involved in a BP can be married or not. Thus, Accept or Confirm set proposal or marriage pointers but do not create any BP. But since, by Lemma 32, men are always improving their marriage, a better one cannot create a new BP. Furthermore, after a transition where one of these two moves has been applied, Inco-herentPointersM(m) is still not True. Indeed, in C, m.marriage = Null and, after Accept, this is still True. And if the move is Confirm, m.marriage = Null but m.marriage = m.proposal (effect of the rule: m.proposal is set to Null). And m.marriage.marriage = m is False since in C, m.proposal.marriage = m and women cannot change their marriage when they are already married.

Thus, C' is in C 2 and by induction, all the reachable configurations from C are also in C 2 . Proposition 2. Every execution takes O(n 4 ) moves to reach a configuration C in ({2}, {2}, 0). Moreover, every configuration reached from C is in ({2}, {2}, X) with X ≥ 0.

Proof. For each set of configurations C = ({1.5, 2}, {1.5, 2}, X) × with X ≥ 0 listed below, we show how any execution starting from a configuration in C reaches a configuration in C 1 or in ({2}, {2}, 0). For doing that, we indicate the lemmas justifying the reachability from one set of configurations to another. Note that each such sub-execution takes O(n 2 ) moves.

1. From ({1.5}, {1.5}, X) to:

• C 1W , for X > 0: Lemma 20.

• C 1 (if there is at least one man's incoherent pointer) or ({2}, {2}, 0), for X = 0: Lemma 19.

2. From ({1.5}, {1.5, 2}, X) to C 1 or • ({1.5}, {2}, X), for X > 0: Lemma 23,

• ({2}, {2}, 0), for X = 0: Lemma 19.

3. From ({1.5}, {2}, X) to C 1 or :

• ({1.5, 2}, {2}, X), for X > 0: Lemma 24,

• ({2}, {2}, 0), for X = 0: Lemma 19.

4. From ({1.5, 2}, {2}, X) to: C 1 or ({2}, {2}, X):

• for X > 0: Lemma 25,

• for X = 0: Lemma 19.

5. From ({1.5, 2}, {1.5}, X) to C 1W or ({1.5}, {1.5}, 0), for X ≥ 0: Lemma 21.

6. From ({1.5, 2}, {1.5, 2}, X) to C 1W or ({1.5}, {1.5}, 0), for X ≥ 0: Lemma 21.

7. From ({2}, {1.5}, X) to C 1W or ({1.5}, {1.5}, 0), for X ≥ 0: Lemma 21.

8. From ({2}, {1.5, 2}, X) to C 1W or ({1.5}, {1.5}, 0), for X ≥ 0: Lemma 22. 9. From ({2}, {2}, X) to C 1 or ({2}, {2}, 0), for X > 0: Lemma 26. Now, we consider a configuration C' in C 1 . By Lemma 10, any execution starting from C' takes O(n) moves to reach a configuration C 1 in C 1W or in ({1.5}, {1.5}, X) with X ≥ 0.

If C 1 is in ({1.5}, {1.5}, 0), the case is listed above (item 1): by Lemma 19, a configuration either in C 1 (if there is at least one man's incoherent pointer) or in ({2}, {2}, 0) is reached. Note that can lead to cycle between ({1.5}, {1.5}, 0) and C 1 because of men's incoherent pointers. But since each man can have at most once incoherent pointers, this cycle can only last until there is no more incoherent pointers, that is n times. After that, from ({1.5}, {1.5}, 0), the reached configuration is in ({2}, {2}, 0) in O(n) moves, by Lemma 19. From C 1W , by Lemma 28, a configuration C 2 in C 2 is reached. Moreover, by Lemmas 11, 14, 15, 16 and 19, this configuration is reached in O(n 4 ) moves.

Thus, starting from C', any execution reaches a configuration C 2 in C 2 or in ({2}, {2}, 0). By Lemma 29, from C 2 in C 2 , every configuration is in C 2 . If C 2 is in ({2}, {2}, 0), either a configuration in C 1 is reached or all reachable configurations are in ({2}, {2}, X) (with X ≥ 0 ). Indeed, nodes in phase 2 can only shift to phase 1. Then, either from C 2 all configurations are in ({2}, {2}, X ≥ 0) or there exists a transition (with either ToPhase1, BadInit or men's Reset) to C 3 ∈ C 1 (in O(n 4 ) moves, by Lemma 3). From C 3 , a configuration C 4 in C 2 is reached (see the above case where C' is in C 1 ) and all reachable configurations are in C 2 .

In summary, we have listed above all possible types of configurations and shown that, in each case, a configuration C" in ({2}, {2}, 0) is reached in O(n 4 ) moves and that every configurations reached from C" are in ({2}, {2}, X) with W ≥ 0. Proof. Since w is in phase 2 in D 0 (by hypothesis), w is not enabled for any rule in {ToPhase1.5, ToPhase2, Confirm1, Propose1}. Moreover, since w remains in phase 2 in D 1 , w cannot execute ToPhase1 and BadInit. If it is the case, then w will be in phase 1 in D 1 , which yields a contradiction. This proves point 1.

III.2.2.2 -

The point 2 holds according to the guard of Reset, Propose2 and Confirm2.

Assume that w executes a rule in D 0 → D 1 . We consider two cases. First, if w.marriage = Null in D 0 , then according to the algorithm, w is eligible for Propose2 and Confirm2 in D 0 but not for Reset, which proves the point 3.

Second, if w.marriage = Null in D 0 , then w is not eligible for Propose2 neither Confirm2 according to the guard of these rules, which proves the point 4.

Lemma 31. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Assume that in some transition D 0 → D 1 in E a man m executes a rule. Lemma 32. Let m be in Men. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Let D 0 → D 1 and F 0 → F 1 be two transitions corresponding to two consecutive activation by m of Confirm. We have: m executes at least one Accept between D 1 and F 0 .

The activated rules is either

Proof. We have: m.proposal = Null in D 1 and m.proposal = Null in F 0 according to Confirm. So, m has to execute a rule that writes a non-null value in m.proposal between D 1 and F 0 . Since E is a sub-execution such that for each configuration in E, all nodes are in phase 2, m can execute only Accept or Confirm by Lemma 31. Among these two rules, there is only one rule doing that: Accept. Thus, m executes this rule at least once between D 1 and F 0 . This concludes the proof.

Lemma 33. Let m be in Men. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Let D 0 → D 1 and F 0 → F 1 be two transitions corresponding to two consecutive activations by m of Confirm. We have: priority(m,m.marriage(D 1 )) > priority(m,m.marriage(F 1 )).

Proof. We prove the first point. First, let D 0 → D 1 and F 0 → F 1 be two transitions corresponding to two consecutive Confirm executed by m.

From Lemma 32, there exists at least one transition between D 1 and F 0 in which m executes Accept. Let A → B be the last such transition between D 1 and F 0 . Thus, m only executes some Accept in D 1 * → A (from Lemma 31 and since m does not execute any Confirm between D 1 and F 0 ). Accept does not write in m.marriage, so m.marriage remains constant between D 1 and F 0 . Let m.marriage = w 1 in D 1 . Thus m.marriage = w 1 in A. From the definition of Accept, we have:

BestProposal(m) = Null in A. Let w 2 = BestProposal(m) in A.
According to the predicate we have: w 2 = min(P m ) and so priority(m,w 2 ) < priority(m,m.marriage) with m.marriage = w 1 in A. Thus priority(m,w 2 ) < priority(m,w 1 ). Moreover, since w 2 = BestProposal(m) in A, then m.proposal = w 2 in B. Observe that m does not execute any rule between B and F 0 . Thus m.proposal = w 2 in F 0 . Since m executes Confirm in F 0 → F 1 then m.marriage = w 2 in F 1 .

Finally, we have: m.marriage(D 1 ) = w 1 and m.marriage(F 1 ) = w 2 and priority(m,w 2 ) < priority(m,w 1 ) which concludes the proof.

Corollary 1. Let m be in Men. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Man m can execute at most n + 1 Confirm in E.

Proof. By Lemma 31, m upgrades its marriage between two consecutive Confirm.

There is at most n distinct possible marriages and there exists a total order among all these possibilities. Lemma 34. Let w be in Women and let m be in Men. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Let A 1 and A 2 be two configurations of E such that A 1 * → A 2 and w does not execute any rule between A 1 and A 2 .

1. If m ∈ C w in A 1 and m ∈ C w in A 2 then m executes Confirm in A 1 * → A 2 ; 2. If m ∈ C w in A 1 and m ∈ C w in A 2 then m executes Confirm in A 1 * → A 2 . Proof. 1. m ∈ C w in A 1 implies
= BestMarriage(w) in F 0 . Assume that m 1 = BestMarriage(w) in D 0 .
There are two cases: either w does not execute any rule between D 0 and F 0 or w does execute some rules. We start with the first case.

Observe that w.proposal = m 1 in D 1 and in F 0 . Moreover according to the Propose2 guard, BestMarriage(w) = w.proposal in F 0 . Thus BestMarriage(w) = m 1 in F 0 meaning that m 1 = m 2 . There are now three sub-cases. Consider the second case in which w executes Propose2 in C 0 → C 1 . In that case, the lemma holds.

The third case is when w executes Reset in C 0 → C 1 . In configuration C 1 we have that w.proposal = w.marriage = Null. The same holds in configuration C 2 since w does not execute any rule between these two configurations, by hypothesis. In C 2 , woman w can only execute Propose2 or Confirm2 by point 3 of Lemma 30. Since we also have that w.proposal = Null in configuration C 2 then Response(w) does not hold in C 2 and thus w is only eligible for Propose2, which concludes the proof.

Lemma 37. Let m be in Men. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Let D 0 → D 1 and F 0 → F 1 be two transitions corresponding to two consecutive activations by m of Accept. If m does not execute any rule between D 1 and F 0 then there exists a woman which executes a move between D 1 and F 0 .

Proof. Assume by contradiction that this is not the case. BestProposal(m) = Null in D 0 so there exists w ∈ Women such that w = BestProposal(m) in D 0 and so w.proposal = m in D 0 . Thus in D 1 , AlreadyEngaged(m) holds or otherwise w executed a rule in D 0 → D 1 which yields a contradiction. By definition of Accept, AlreadyEngaged(m) does not hold in F 0 . Since this predicate holds in D 1 and since m does not execute any rule between D 1 and F 0 then necessarily w executes a rule, which yields a contradiction. Proposition 3. Let E be a sub-execution such that, in every configuration, all nodes are in phase 2. Nodes can execute at most O(n 4 ) moves in E.

The complexity gap between the original Gale and Shapley's Algorithm (GSA) [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF] and the distributed version using Ackermann et al.'s phases is quite large. There would be multiple reasons for that: distribution, asynchrony and in particular the very adversarial scheduler, self-stabilization or simply a wrong approach to the problem. The difference between O(n 2 ) and O(n 4 ) is big and it seems important to understand the real reasons for it. A way for attacking this issue could be to start from the optimal version, GSA, and to add step by step supplementary constraints in order to localize where the discrepancies come from. It is what we do in the present chapter. The result of our investigation is somewhat surprising: as a matter of fact, the gap disappears when considering the problem in the right way. Indeed, as we show it in the previous chapter, the cost of the local detection of "errors" (e.g., BPs) is negligible, but the local resolutions of these "errors" may require a huge (and even infinite) number of actions. Thus, we now aim at resolving these errors/faults globally.

We adopt the technique introduced in [AKY90, APSVD94] under the name of local checkability and global repair. As it will be explained later, we were lead at defining a slightly different definition of local checkability [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], adapted to our purposes. It worth noting that the new solution in this chapter works under the more general and practical communication model of link register (equivalent to message passing; see the definition in the Model Chapter 3, Section V). A preliminary version of this work has been published in [BBB + 18].

The chapter is organized as follows. We informally present the steps to obtain the new self-stabilizing solution to SMP in Θ(n 2 ) moves, in Section I. Then, in Section II, we describe the local checkability scheme and propose our definition. In Section III, the nonself-stabilizing but distributed asynchronous algorithm solving SMP, called Async-GSA, is designed and its correctness and local checkability property are proved. Afterward, in Section IV, we propose a reset algorithm ResetAlg that runs on a tree (built by a proposed algorithm TreeAlg). Finally, all algorithms are combined in Section V to get the self-stabilizing algorithm CompAlg, which solves SMP in Θ(n 2 ) moves. We conclude this chapter in the last Section VI.

I -Introduction

The issue of transforming a classical distributed algorithm, with a particular initialization, into a self-stabilizing one, has been studied for a very long time and different types of approaches have been proposed. These approaches focus on the notions of locality and globality and follow the same pattern. If an algorithm deviates from a correct behavior (because of transients faults or bad initialization), the incorrectness has first to be detected, and then corrected. For most problems, detection can be made locally. It appears this is also the case for the stable marriage, because an inconsistency implies either an incoherence between the variables of two neighbors or the existence of a blocking pair. Both can be detected by exchanging information only at the local level. Once an incoherence has been detected, one has to repair it, and the reparation can be either local or global. In the case of stable marriage, Knuth's cycle [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF] suggests that local repair does not work. That is why we considered techniques based on local detection and global repair.

Global repair means that a node detecting an inconsistency is activated for propagating a reset wave, which sets each node in the network into an initial state in a synchronized way. Then, staring from such a re-initialized configuration a non-selfstabilizing but distributed algorithm will produce a correct result. However, things are not so simple, having in mind to get an optimal complexity and to keep the preference lists private. First, since the final algorithm has to be self-stabilizing, it must detect faults at any time, in any component of the final combination. Thus, the reset component and the distributed version of GSA have to be executed in parallel and each should stabilize in at most O(n 2 ) moves. Notice that (to our knowledge) there are no studies on the move complexity of such algorithms in the considered model. So we have to provide it to achieve our goal.

Moreover, to obtain an efficient move complexity of the whole composition under an unfair daemon appears to be quite challenging. Such an adversarial scheduler can choose to activate in priority GSA part of the composition, when a reset is ongoing (and conversely), resulting in the multiplication of the move complexities of the two submodules. However, the advantage of the bipartite communication graph coupled with a system of priorities between the algorithm modules allow to propose a combination in which complexity is additive and not multiplicative.

Our starting point is a well known technique introduced in [AKY90, APSVD94] under the name of local checkability and global repair. It was proven in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] that, if an initialized solution satisfies some specific properties, it can be transformed in a self-stabilizing solution. Although [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] assumes the message passing model, the transformation applies to the link register model. Indeed in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] the channel capacity is 1 message and is equivalent to a register in read/write atomicity ([KK15, AKY97]). For the transformation to be correct, the non self-stabilizing algorithm has to be locally checkable [START_REF] Afek | Memory-efficient self stabilizing protocols for general networks[END_REF], i.e., nodes can locally detect if a configuration is incorrect. Correct configurations are in particular those reached by an execution of the given non-self-stabilizing algorithm (here Async-GSA) starting from a correct configuration (here C Async-GSA init -the initial configuration of Async-GSA). Notice however that a configuration in which there is any stable marriage is also correct, even if it cannot be reached by an execution from C Async-GSA init (see Figure 5.4 for an example of a stable marriage that cannot be reached by GSA). Checking is made periodically, locally by each node, verifying the consistency of its state with the values in the shared registers written by its neighbors. Once an incorrect configuration is locally detected, a global reset is launched, setting each variable to a predefined initial (reset) value, while ensuring the required synchronization allowing to reach the initial configuration C Async-GSA init . Then the algorithm behaves as if it has been started from a correct configuration and reaches a terminal configuration with a stable marriage. Note that, in Chapter 6, we also study how the proposed algorithm can be useful for obtaining self-stabilizing solutions to some variants of the stable marriage problem.

II -Local Checkability

For obtaining a self-stabilizing algorithm computing a stable marriage (or solving any other problem) in a general communication model under an unfair demon, weaker than in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], we have to strengthen the original definition (property) of their local checkability in several ways (given in Definition 6 below). By abusing the notation, we keep the name of local checkability for this more restricted property.

To explain the property and the restrictions we add, let us start with the original definition. Basically, in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], an algorithm Alg is locally checkable for a global predicate Π if: (i) Π can be defined by local predicates LP i,j (for every directed link (i, j)) on the state of node i and the shared register value of j that can be read by i, (ii) no action of Alg can turn LP i,j from being satisfied to not, and (iii) there is a configuration in the set of configurations of Alg satisfying Π. The conditions (i) and (ii) correspond to 1 and 3 in Def. 6.

Contrary to (iii), the condition 2 in Def. 6 is restricted to the initial configuration of Alg. Both conditions provide configurations to be restored by the reset. Notice however that (iii) is too weak. For example, Alg reaches configurations containing stable marriage satisfying Π (thus satisfied by (iii)), but it is difficult to reset the variables of every node to obtain the corresponding configuration with a stable marriage. It requires to solve the problem itself in advance. On the contrary, since Alg is an initialized algorithm, it is known how to set the local variables of each node to obtain it, it suffices only to ask that this configuration satisfies Π. One can chose another such configuration reachable in Alg, but the local states (values of the variables) of that configuration should be known in advance (for being able designing the transformer).

The conditions 4 and 5 are completely newly added restrictions in Def. 6, comparing to those in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF]. The condition 5 is introduced for dealing with an unfair daemon. This condition prevents from this adversary to retain the correction process of the reset module, by constantly privileging the actions of Alg. This becomes impossible with such a condition, since Alg is asked to be terminating.

Finally, condition 4 ensures that from any configuration satisfied by Π, even one that cannot be reached in executions of Alg, the problem solved by Alg is nevertheless solved. This condition is required since a reset is not launched in configurations satisfying Π and Π is asked to be stable. Put another way, first notice that condition 4 reduces the class of algorithms to which the reset is applicable. These algorithms must have the special property to be correct, not only when started from their initial configuration, but also from any configuration satisfying the predicate Π. Such configurations may be unreachable from the initial configuration but, as Π is stable, the executions from them may never activate the reset. Then Alg, on top of being correct from its initial configuration, must have the supplementary property to be also correct from all configurations satisfying Π. This condition is lacking in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], resulting in a weaker transformation to behaviors of Alg from any configuration in Π, and not necessary for solving the problem solved by Alg.

Definition 6 (extended from [AKY90, APSVD94]). [Local Checkability] Let Alg be a solution to a problem specification Prob and Π a global predicate on the configurations of Alg. Alg is locally checkable for Π iff the following conditions hold.

1. There exists a set LP of local predicates LP i,j for each i and j where (i, j) ∈ E such that

Π = ∀(i,j)∈E LP i,j .
2. The initial configuration of Alg satisfies Π.

Each LP

i,j is stable, that is, if C is a configuration satisfying LP i,j and C → C' is a transition of Alg, then C' satisfies also LP i,j .
4. Any execution from a configuration satisfying Π satisfies Prob.

5. From any configuration, Alg terminates.

III -Towards a Distributed Asynchronous Version of GSA

We start by presenting the non-distributed algorithm of Gale and Shapley, on which we base our distributed solution with initialization. Then, in Sub-section III.1, we present this non-self-stabilizing distributed solution -algorithm Async-GSA. In Sub-section III.2, we define the local predicates required to prove the local checkability of Async-GSA, together with its correctness and the move complexity upper bound. Gale and Shapley's algorithm executes successive rounds. In every round, each woman proposes to her favorite man (Figure 5.1.a, proposals are represented with turquoise arrows). Doing so ensures that no blocking pair appears in the final matching (and during the whole execution). Each man who receives proposals accepts the best one (according to his preferences) and rejects all the others (Figure 5.1.b). On the figures, accepted marriages are represented with bold edges and names. A woman rejected by a man crosses out his name on her list.

Async-GSA init

defined by variables set to a specific value (see Sub-section III.1.1).

However, the resulting algorithm works very differently from the original version, due to asynchrony. In GSA, executions proceed in synchronous rounds. In alternating rounds, women propose in a round and in the other round men answer. When men answer, they choose right away the best proposal in GSA. But in the proposed algorithm, they consider each received proposition separately at each step, not synchronously with the other received proposals in the same round as in GSA, depending on the particular schedule chosen by the adversary. Furthermore, since GSA is centralized, if a married man accepts a better proposal, the previous marriage is canceled right away and the previous spouse can propose to another man in the next round. With an asynchronous distributed scheduler, information can be delayed and the proposed solution has to take care of that.

Regarding the optimally of the solution, it has been proven in [START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF] that the communication complexity ([Yao79]) of the stable marriage problem is Ω(n 2 ) bits. This result implies an Ω(n 2 / log n) bound in moves in our model (assuming constant size communication registers). This is because in the model here each dedicated link directed from every participant in one set to another allows to not incorporate identities into messages. Communication complexity concerns the amount of information that has to be transferred only over a single bidirectional link between the two parties, called Alice and Bob. In our case, Alice holds the instance input (preference lists) of women and Bob, of men. In any algorithm functioning in such a setting it is required to include the ID of the concerned participant in a transferred message; while this information is encoded in our setting of bipartite network and thus should not be transferred. Nevertheless, the algorithm proposed here can be considered as near optimal. Moreover, we believe that there is a better lower bound of Ω(n 2 ).

III.1.1 -Variables, Constants, Registers and Functions (for a node v)

Variables & Constants.

• pref : v's constant list of its n neighbors in preference order. The priority of the element is the rank, i.e., the i th element has priority i. Thus, the first element is the most preferred neighbor and its priority is 1.

As before pref is a constant list and is kept secret.

• marriage_pref ∈ N (v) Null: if v is a woman, the node to whom v has proposed (and her spouse if additional conditions are satisfied; see below); if v is a man, his spouse identifier. In C

Async-GSA init

, for men, the value of marriage_pref is Null and for women, the first element of v's pref .

Registers.

Recall that var v,u can be read and written by v but only read by u.

• request v,u ∈ {None, Proposal, Yes, No}:

-None: initial value of the variable (in C Async-GSA init ).

-Proposal: only for a woman v to propose to a man u.

-Yes: used by a man to accept a proposal or by a woman to confirm a marriage.

Two nodes v and u are said to be married iff request v,u = request u,v = Yes.

-No: used by a man to refuse a proposal or by a woman to confirm a refusal.

Notice that in the algorithm, v may want access to a variable var v,Null or var Null,v . This variable does not exist and the value None is returned.

Functions

• next(v): returns the element after marriage_pref in the preference list of v and returns Null if marriage_pref is the last element or if marriage_pref = Null.

• priority(v,u): returns the priority (∈ [1, n]) of u in the preference list of v. Note that if u is evaluated to Null, priority(v,u) = n + 1 .

III.1.2 -Async-GSA's Algorithm Predicate

The matching M is defined by so-called married pairs (v, u)

∈ E such that request v,u = Yes ∧ request u,v = Yes ∧ marriage_pref v = u ∧ marriage_pref u = v.
The predicate associated to Async-GSA is

PredAsync-GSA ≡ [∀v ∈ V : Married(v) ∧ ¬BlockingPair(v) ]
where

• Married(v) ≡ (request v,marriage_prefv = Yes) ∧ (request marriage_prefv,v = Yes) ∧ (marriage_pref marriage_prefv = v) • BlockingPair(v) ≡ ∃u ∈N (v): priority(v,marriage_pref v ) > priority(v,u) ∧ priority(u,marriage_pref u ) > priority(u,v).
For a node u that makes BlockingPair(v) satisfied, (v, u) is called a blocking pair. Proposition 4. A configuration C satisfies PredAsync-GSA iff C contains a stable marriage.

Proof. Let us first prove by contradiction the direct implication: if PredAsync-GSA is True in C, then C contains a stable marriage. First, since a node v can only be married with the node marriage_pref v , v cannot be married twice. Now, let v be single. In this case,

request v,marriage_prefv = Yes ∧ request marriage_prefv,v = Yes is False since request v,Null = request Null,v = None.
Then, each node is married with exactly one node. Furthermore, the marriage is reciprocal. Indeed, since request marriage_prefv,v = Yes and the predicate is True for the node marriage_pref v , then marriage_pref marriage_prefv = v. Now, by contradiction, assume that v participates to a blocking pair. So, there exist node u and v which are not married together but prefer each other to their current spouse. But PredAsync-GSA is True, i.e. BlockingPair(v) is False so that u and v do not prefer each other. This leads to a contradiction and thus there is no blocking pair in C. Thus C contains a stable marriage. Now, we prove that if a configuration C contains a stable marriage, it satisfies PredAsync-GSA. Two nodes u and v are married if

request v,u = Yes ∧ request u,v = Yes ∧ marriage_pref v = u ∧ marriage_pref u = v. So, ∀u ∈ V , Married(v)
is True. Furthermore, in a stable marriage, there is no blocking pair. Then, there is no pair (u, v) such that u prefer v to its current spouse and vice versa: the predicates BlockingPair(u) and BlockingPair(v) are false. Hence, PredAsync-GSA is True in C.

III.1.3 -Algorithm

The part of the algorithm executed by women (Algorithm 3) has 3 rules. We start by describing intuitively what those rules do.

• The rule Propose is executed by a woman to propose to the man in her marriage_pref pointer.

• The rule Confirm checks if the man marriage_pref to whom the woman has proposed, has answered positively. If he has, her register is set to Yes.

• The rule Refusal_Management is enabled if the woman's proposal has been rejected by the man marriage_pref . In this case, the value No is set in the register and the marriage_pref pointer is set to the next man in the woman's preference list1 .

Algorithm 3 Async-GSA for w ∈ Women:

∧ marriage_pref = m ∧ request m,w = No} 14: request w,m ← No 15: marriage_pref ← next(w)
The part of the algorithm executed by men (Algorithm 4) consists of 2 rules:

• The rule Accept is enabled if a woman is proposing to the man and if this woman is preferred over the actual spouse of m, i.e., the woman pointed by his marriage_pref pointer. In this case, the man sets its request variable (in the shared register) to Yes and updates his marriage_pref pointer to the identifier of the woman.

• The role of Refuse is the opposite of Accept: if a proposal is received from a less preferred woman than his actual spouse, the man sets its request variable to No.

Algorithm 4 Async-GSA for m ∈ Men:

III.2 -Local Checkability of Async-GSA

We prove that Async-GSA is locally checkable (according to Def. 6), by constructing the local predicate (named LP m,w ) that is checked by each man m. For that, w communicates to m whether it prefers m to its current spouse. With this information, m is able to detect a blocking pair on the edge (m, w) but also an incoherence in the variables. We prove it in Sub-section III.2.2. Notice that the exchange of information between w and m is limited and respects the privacy: preference lists are not communicated.

III.2.1 -Local Predicates

The local predicate LP m,w must detect any deviation in the execution of Async-GSA.

That is why it is built in relation with the guarded rules of Async-GSA. We use the specificity of the communication graph to define the local predicate only on the edges (m, w) where m ∈Men and w ∈Women: LP m,w is checked by (the man) m on his edge (m, w). We build LP m,w step by step. In the sequel we use the terms "to the right" (rep. "to the left") for indicating that the pointer of marriage_pref w has been shifted towards a less (resp. more) preferred man. Note that in the clauses of LP m,w we sometimes have a term marriage_pref w = m or priority(w,marriage_pref w ) < priority(w,m). To enable man m to evaluate these terms we assume that each woman w shares the result of these comparisons (for every neighboring man m) in its shared registers. This assumption is implicit and not implemented in Async-GSA. We describe each sub-predicate in the following. P 0 m,w is a predicate satisfied locally in a configuration C where no proposal/refusal/ acceptance has been made by m or w on the registers of the edge (m, w) and in all configurations reached from it, as long as no rule has been applied by m or w on the registers. In other words, it is satisfied in a configuration where request w,m = request m,w = None, and in all subsequent configurations as long as no rule is applied on (m, w). In these latter configurations, request w,m and request m,w have not been modified but marriage_pref w and marriage_pref m may have been updated by rules applied on other links (marriage_pref w cannot be shifted to the right).

P 0 m,w ≡ request w,m = request m,w = None ∧ priority(w,marriage_pref w ) < priority(w,m) Notice that P 0 m,w is True in C Async-GSA init . P P ropose m,w
is a predicate related to a situation in which a proposal has been made by a woman w. Proposals are made in a configuration satisfying P 0 m,w with Propose. This rule sets request w,m to the value Proposal and marriage_pref w to m.

P P ropose m,w ≡ request w,m = Proposal ∧ request m,w = None ∧ marriage_pref w = m P Accept m,w
is a predicate related to a situation in which a proposal has been made by w to m and m has accepted, i.e., from a configuration in which P P ropose m,w is True, an acceptance is made by m with Accept. The predicate allows to check the priority of marriage_pref w : after Accept, either marriage_pref m points to w or, if m has accepted a new better proposal, to a better ranked woman. Thus, the priority of marriage_pref m is better than that of w.

P Accept m,w ≡ request w,m = Proposal ∧ request m,w = Yes ∧ priority(m,w) ≥ priority(m,marriage_pref m ) ∧ marriage_pref w = m P Conf irm m,w
is a predicate related to a situation in which both nodes have set their request variable to Yes, meaning that they are married. A configuration, in which

P Conf irm m,w
is True is obtained from a configuration satisfying P Accept m,w after a transition with Confirm. For the same reason than for P Accept m,w , the priority of marriage_pref m is checked. is True. Thus, this predicate is related to a situation in which w and m have both refused to be married together.

P Conf irm m,w ≡ request w,m = Yes ∧ request m,w = Yes ∧ priority(m,w) ≥ priority(m,marriage_pref m ) ∧ marriage_pref w = m P Ref use m,w
P R_M m,w ≡ request w,m = No ∧ request m,w = No ∧ priority(w,m) < priority(w,marriage_pref w ) ∧ priority(m,w) > priority(m,marriage_pref m ) P BP
m,w is a predicate used for detecting if the subsystem contains a blocking pair. Recall that there exists a blocking pair if both marriage_pref of w and m variables are not pointing to each other but nodes prefer each other to their actual marriage_pref , for all values of request.

P BP

m,w ≡ priority(w,m) < priority(w,marriage_pref w ) ∧ priority(m,w) < priority(m,marriage_pref m )

Notice that if a woman reaches the end of her preference list with no partner, the situation is detected by this predicate. Indeed, at least one man is single and so a blocking pair is formed (since the nodes' sets are of equal size). are stable comes directly from their construction and their relation to the transitions of Async-GSA. Furthermore, we prove in the following lemma that ¬P BP m,w is also stable. Proof. The only rule updating marriage_pref of w is Refusal_Management. This rule sets the pointer to the next element in the list after marriage_pref and if marriage_pref is the last element, to Null. Notice that if marriage_pref is set to Null, the rule Refusal_Management is not enabled (∀v ∈ V, Null / ∈ N (v)). Thus, the pointer of the women cannot be moved.

III.2.2 -Proof of

Corollary 3. From any configuration, a woman w is activated in an execution at most n times for Refusal_Management.

Proof. By lemma 39, each woman can only be activated once for Refusal_Management for each element in her preference list. Furthermore, since preference lists have n elements, each woman can be activated at most n times for Refusal_Management. Lemma 40. From any configuration, a woman w is eligible in an execution for at most two moves (one Propose and one Confirm) if she is not activated for any Refusal_Management.

Proof. The guards of these two rules contain marriage_pref = m, allowing their activation on the edge (w, m) only (since w is not activated for Refusal_Management). Furthermore, the condition request w,m = Proposal in the guards of Confirm, resp. request w,m / ∈ {Proposal, Yes, No} in Propose's guard, implies that after its activation, Confirm, resp. Propose, is no more enabled. Finally, after the activation of w for Propose, Confirm may be enabled, but after the activation for Confirm, Propose is not enabled.

Thus, Confirm and Propose are activated at most once each on the edge (w, m) if w is not activated for Refusal_Management.

Corollary 4. From any configuration, a woman w is activated in an execution for at most two moves between two activations for Refusal_Management.

Proof. By Corollary 3, w can be activated twice for Refusal_Management and by Lemma 40, w can be activated only twice between these two Refusal_Management. Lemma 41. From any configuration, after at most 3n -2 of her own moves in an execution, a woman w is no more activated for any Async-GSA's rule.

Proof. Let w be a woman. Assume by contradiction that there is a cycle of activations. By Corollary 3 and Corollary 4, this is not possible if Refusal_Management is activated (after two of her own moves, w is no more eligible). Furthermore, by Lemma 40, w can be activated for only two moves without being activated for Refusal_Management.

Thus, after at most 3n-2 of her own moves, w is no more eligible for any Async-GSA rule.

Lemma 42. From any configuration, after at most 2n -1 of his own moves in an execution, a man m is not any more activated for any Async-GSA's rule.

Proof. Let us consider the marriage_pref pointer of m. It can be set only by the rule Accept and, since in the guard there is the priority condition (priority(m,w) < priority(m,marriage_pref )), m can only move its pointer to the left. Thus, since there are n elements in his preference list, m can be activated at most n times for Accept. Now let us consider the rule Refuse. Since request m,w = No, m cannot be activated for Refuse twice in a row. Furthermore, it cannot be activated in alternation with Accept since priority(m,w) > priority(m,marriage_pref ) for Refuse and marriage_pref can only be shifted to the left by Accept. That is why m can only be activated n -1 times for Refuse.

Thus, after at most 2n -1 of his own moves, m cannot be activated any more for any rule of Async-GSA.

Corollary 5. From any configuration, after O(n 2 ) moves in an execution, no rule is enabled, i.e. the configuration is terminal.

Proof. The corollary is a direct consequence of Lemmas 41 and 42. But, since P BP m,w is false on all edges (m, w), BlockingPair(v) is False for all v. This implies that no node has marriage_pref = Null. Notice also that if P Conf irm m,w is satisfied on an edge, we have priority(m,w) = priority(m,marriage_pref m ) (and not priority(m,w) ≥ priority(m,marriage_pref m ), otherwise m would be eligible for Refuse). Hence, each man and woman has one and only one incident edge that satisfies P Conf irm m,w , i.e., each node satisfy Married.

Recall that

PredAsync-GSA≡ [∀ v ∈ V : Married(v) ∧ ¬BlockingPair(v)] where • Married(v) ≡ (request v,marriage_prefv = Yes) ∧ (request marriage_prefv,v = Yes) ∧ (marriage_pref marriage_prefv = v) • BlockingPair(v) ≡ ∃ u ∈ N (v): priority(v,marriage_pref v ) > priority(v,u) ∧ priority(u,marriage_pref u ) > priority(u,v).
Thus, a terminal configuration satisfying Π satisfies also the algorithm predicate PredAsync-GSA of Async-GSA.

Recall that the problem specification Prob defining SMP (defined in Chap. 3, Sec. VI) is satisfied by an execution iff a) the execution reaches a terminal configuration (i.e., a configuration in which no node is eligible), and b) this configuration contains a stable marriage.

Furthermore, notice that this following lemma proves also the correctness of Async-GSA.

Lemma 44. The point 4 of Definition 6 is satisfied, i.e. from any configuration C 0 satisfying Π, any execution of Async-GSA satisfies Prob.

Proof. By Corollary 5, from any configuration satisfying Π, a terminal configuration C 1 is reached. Furthermore from Lemma 38 and the fact that LP m,w is stable, C 1 satisfies Π. Finally, by Lemma 43, C 1 satisfies the algorithm predicate PredAsync-GSA, i.e., contains a stable marriage by Proposition 4. Thus, from any configuration satisfying Π, any execution of Async-GSA satisfies Prob.

Now we can prove that

Async-GSA is locally checkable. Recall that the initial config- uration C Async-GSA init is a configuration where ∀(m, w) ∈ E, request w,m = request m,w = None ∧ marriage_pref m = Null ∧ priority(w,marriage_pref w ) = 1.
Theorem 2. Async-GSA is locally checkable for Π.

Proof. There are five conditions in Def. 6. First, the condition 1 is satisfied by definition of Π and LP m,w . Second, C Async-GSA init satisfies the condition 2 (P 0 m,w is satisfied for all (m, w)). Third, by Corollary 2, the condition 3 is satisfied. Fourth, by Lemma 44, the condition 4 is satisfied. Finally, by Lemmas 41 and 42, the condition 5 is satisfied. So, a man can detect, using the local detection detailed in [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF], whether or not its Async-GSA state satisfies LP m,w . If not (cf. Section IV), it can take some actions. The global composition is presented in Section V.

III.3 -Time Complexity

Async-GSA's Time Complexity. Notice that Corollary 5 proves the worst case complexity of the Async-GSA module: O(n 2 ) moves. This induces also a complexity of O(n 2 ) rounds. Indeed, the definition of a round (see Def. 4) captures the execution rate of the slowest processor in any computation. Since there is at least one move in each round, an upper bound for the move complexity is an upper bound for the round complexity. Thus, the final configuration is reached in at most O(n 2 ) rounds. In the following, we illustrate an execution scenario that reaches this bound, proving that our round and move complexity is tight. Consider a system with n women and n men denoted by w 1 , w 2 , . . . , w n and m 1 , m 2 , . . . , m n (Figure 5.5). The preference list of w x for x > 1 is: [m x , . . . , m n , m 2 , . . . , m x-1 , m 1 ] and w 1 has the same list as w 2 . The preference list of m x is: [w x+1 , . . . , w 1 , w n , . . . , w x+2 ], with x + 1 = 1 and Now, w n is single and proposes to m 2 , . . . , m n-1 until being accepted by m n-1 . So, after 2 • (n -2) rounds, w n is married to m n-1 and w n-1 is single. Thus, each woman makes proposals with the same pattern in 2 • (n -2) rounds and the last woman w 2 ends up (after its own 2 • (n -2) rounds) by proposing to m 1 (Figure 5.8). This leads to a final complexity of Θ(n 2 ) rounds.

x + 2 = 2 if x = n and x + 2 = 1 if x = n -1. w 1 {m 2 , m 3 ,. . . , m n-1 , mn, m 1 } w 2 {m 2 , . . . , mn, m 1 } w n-1 {m n-1 , mn, m 2 , . . . , m n-2 , m 1 } wn {mn, m 2 , . . . , m n-1 , m 1 } m 1 {w 2 ,
w 1 {m 2 , m 3 ,. . . , m n-1 , mn, m 1 } w 2 {m 2 , . . . , mn, m 1 } w n-1 {m n-1 , mn, m 2 , . . . , m n-2 , m 1 } wn { mn, m 2 , . . . , m n-1 , m 1 } m 1 {w 2 ,

IV -Reset

We propose a self-stabilizing distributed and asynchronous reset algorithm (ResetAlg) that, upon request of a node, resets globally a requesting algorithm to a specific configuration. More precisely, this is ensured only if ResetAlg itself is already stabilized to a "correct" configurations. Being self-stabilizing, this algorithm reaches such configurations eventually. We prove that these, as well as the following restored configuration after a reset request, are reached in O(n) moves each. In a similar way to PIF (Propagation of Information with Feedback) algorithms, ResetAlg works with waves propagating up and down a rooted tree values and actions to execute, in a way coordinated (synchronized) by the root. When a node requests a reset, a wave goes up to inform the root. Then, a freeze wave goes down to the leaves to freeze the nodes for the requesting algorithm (such that they are not eligible for it and also for requesting the reset again, as long as the ongoing reset operation is accomplished). Once the leaves are reached, nodes are reset by a wave going up to the root. Finally, the last wave releases the nodes, which have been all reset, and the specific reset configuration reached. Although the general ideas described above, concerning the ResetAlg functioning, apply to any spanning tree, it is necessary to consider a specific tree to obtain such a low complexity, the issue coming from the adversarial unfair scheduler. Indeed, it has the capacity of initiating recursively resets in size increasing sub-trees, terminating none of them but the last one. Thus, the O(n) move complexity is obtained over a bipartite communication graph justified by the definition of SMP. Nevertheless, we present a general complexity analysis of ResetAlg, for any given underlying tree.

The section is organized as follows. In Sub-section IV.1, we present and prove a self-stabilizing spanning tree construction algorithm TreeAlg (Algorithm 5) that builds in O(n) moves a rooted tree of depth 2 on a bipartite graph K n,n . Then, the reset algorithm ResetAlg is presented in Sub-section IV.2. This algorithm is proved to satisfy the specification of the self-stabilizing reset problem (Definition 7) in O(n) moves on a tree of depth 2.

IV.1 -Tree Algorithm TreeAlg

Since a node has a complete preference list, it has the identifiers of the nodes in the opposite set. That allows to build a double fan-shaped tree. The root of the tree is the woman with the minimum identifier, W min . All men are children of W min : this is the first fan. The second fan is composed of the other women that are children of the man with the minimum identifier: M min . Thus the depth of the tree is 2. Since each node holds the identifiers of the other subset in its preference list, W min may learn that she is the root once all men provide her with the correct information regarding the minimality of her identifier. Unfortunately, due to a bad initialization, this information may be incorrect (corrupted). Indeed the construction being an element in the final composition has to be self-stabilizing. That is why we do not consider that the spanning tree is built from the start.

The following figure represents the constructed tree on a bipartite graph K 3,3 . W min is w 1 and M min is m 1 . On the left, the tree is represented on the bipartite graph (bold edges are the links in the tree). On the right, the tree is displayed such that the double-fan construction is visible.

w 1 w 2 w 3 m 1 m 2 m 3 w 1 m 1 m 2 m 3 w 2 w 3 Figure 5
.9: Example of a tree on a graph K 3,3

IV.1.1 -Variables, Constants, Registers and Functions (for a node v)

Variables & Constants.

• parent: the identifier of the parent of v.

If v = W min , eventually parent v = v,
• pref : list of n neighbors in preference order (see the variables of the previous algorithm for more details).

Registers.

• min v,u ∈ {True, False}: True represents the fact that u is the minimum in the pref v , False otherwise.

Functions.

• min(list) → identifier: returns the minimum identifier in the list list.

IV.1.2 -Tree Algorithm Predicate

The algorithm builds a spanning tree rooted in W min . The eventually constructed tree is encoded in the local variables parent. The root of the tree w has parent w = w. All women and men are leaves, except M min and W min . M min is on the paths between W min and the other women. The predicate of the rooted tree construction is:

PredT ≡ ∀ v ∈ V, ∀u ∈N (v): min v,u = (u = min(pref v )) ∧ [(parent v = min(pref v ) ∧ ¬min u,v ) ∨ (parent v = min(pref v ) ∧ min u,v ∧ v ∈Men) ∨ (parent v = v ∧ min u,v ∧ v ∈Women)]
Notice that this definition implies that there is exactly one woman satisfying parent v = v ∧ min u,v , i.e., exactly one W min . Thus, the other women satisfy parent v = min(pref v ) ∧ ¬min u,v and are children of M min . M min satisfies parent v = min(pref v ) ∧ min u,v . Similarly, there is exactly one M min . All other men are children of W min and satisfy . We define the legitimate configurations for the tree algorithm as the configurations satisfying PredT.

IV.1.3 -Algorithm

The self-stabilizing tree algorithm is composed of three rules:

1. The rule I_am_not_root may be enabled for all men and all women except the root. It sets the local variable parent to the minimum identifier of the other set.

2. The rule I_am_root may be enabled for v if v ∈Women and if all v's neighbors u have their communication variable min u,v set to True. In this case, v knows that she is the root of the tree, i.e., W min , and sets her parent pointer to her own identifier.

3. The rule Update updates the link register variables of the adjacent links so that the neighbors could learn whether or not they have the minimum identifier in their set.

Algorithm 5 Tree construction

TreeAlg for v ∈ V 1: I_am_not_root : (* v is not root *) 2: {parent = min(pref ) ∧ [(∃u ∈N (v): ¬min u,v ) ∨ v ∈Men]} 3: parent ← min(pref ) 4: 5: I_am_root : (* v is W min *) 6: {v ∈Women ∧ parent = v ∧ (∀u ∈N (v): min u,v )} 7:
parent ← v Using the constructed tree, the following function computes the children set of a node. This function can be used by any algorithm running on the tree.

• children(v): returns the set of identifiers: returns the v's set of children' identifiers.

if(∀u ∈N (v):

min u,v = True) return N (v)-parent else return ∅

IV.1.4 -Correctness and Complexity Analysis of TreeAlg (Algorithm 5)

Lemma 45. In an execution from any configuration C, each man m is activated at most once for I_am_not_root and at most once for Update.

Proof. A man is eligible only for two rules: Update and I_am_not_root. Indeed, I_am_root is eligible only for women. If m is activated for I_am_not_root, parent takes the value min(pref ). Notice that Update does not change parent. Thus, I_am_not_root cannot be enabled once again. A similar reasoning holds for Update.

Lemma 46. In an execution from any configuration C, each woman w is activated at most once for each rule ( I_am_not_root, I_am_root and Update).

Proof. First the condition of activation of Update is the existence of a variable min u,v (for u ∈N (v)) that is not equal to (min(pref ) = u). Second Update is the only rule setting min. Hence, after one activation of Update, no register satisfies the guard again. Now, notice that a woman cannot be activated twice in a row for I_am_not_root because of the conditions on the variable parent (the same argument holds for I_am_root). Assume that this rules are activated by w more than once but by alternation. Let I_am_not_root be the first activated rule. Thus, before this activation, ∃u 1 ∈N (w): ¬min u 1 ,w but when I_am_root is activated, we know that ∀u ∈N (w): min u,w . Furthermore, between the two activations, at least u 1 has been activated for Update. Now assume that w is activated again for I_am_not_root. This induces that a man u 2 (not u 1 , by Lemma 45) has changed its min u 2 ,w . But, since u 1 has set min u 1 ,v to 1 and all men have the same preference list, u 2 cannot be activated for Update to set the value of min u 2 ,w to 0. Thus, w cannot be activated again for I_am_not_root. The same contradiction can be found if w is activated first for I_am_root and then for I_am_not_root.

Recall that configurations satisfying PredT are legitimate configurations for TreeAlg and that:

PredT ≡ ∀ v ∈ V, ∀u ∈N (v): min v,u = (u = min(pref v )) ∧ [(parent v = min(pref v ) ∧ ¬min u,v ) ∨ (parent v = min(pref v ) ∧ min u,v ∧ v ∈Men) ∨ (parent v = v ∧ min u,v ∧ v ∈Women)]
Lemma 47. Any terminal configuration satisfies PredT, i.e. it is legitimate.

Proof. In a terminal configuration C, ∀ v ∈ V, ∀u ∈N (v): min v,u = (u = min(pref v ))
is necessarily True, otherwise Update would be enabled. Now, assume that C does not satisfy PredT. This implies that at least one edge (v, u) does not satisfies one of these following conditions:

• parent v = min(ref v ) ∧ ¬min u,v • parent v = min(pref v ) ∧ min u,v ∧ v ∈ Men • parent v = v ∧ min u,v ∧ v ∈ Women
Thus (v, u) satisfies at least one of these following conditions:

1. parent v = v ∧ ¬min u,v 2. parent v = min(pref v ) ∧ min u,v ∧ v ∈ Women 3. parent v = v ∧ min u,v ∧ v ∈ Men
Case 1 is not possible in a terminal configuration: v would be eligible for I_am_not_root.

Case 2 is only for women. There are two sub-cases: either all neighbors of v have their min set to 1 or there is at least one neighbor's min variable set to 0. In both sub-cases, a node is eligible: either v is eligible for I_am_root or a neighbor is eligible for Update (u or an other man).

Finally, in case 3, v is eligible for I_am_not_root.

Hence, a terminal configuration satisfies PredT.

IV.2 -Reset Algorithm ResetAlg

In this section, we propose a technique for resetting (under some conditions) a given (so called) basic algorithm BasicAlg into a configuration C

BasicAlg reset

. The technique uses the reset algorithm ResetAlg (Algorithm 6). To request a reset, a reset signal is generated/launched (at any node) by BasicAlg (or some other module controlling the execution of BasicAlg). This triggers the local module of ResetAlg. Launching a signal represents the writing of True by BasicAlg in a boolean variable shared with ResetAlg (called here signal). The reception of the signal is the reading of True in this boolean variable.

Being self-stabilizing, ResetAlg can be started in an arbitrary configuration, but is designed to reach a set of "good/correct" configurations (see C

ResetAlg saf e set defined below). From any such configuration, if finitely many signals are launched by the basic algorithm (and at least one), then the basic algorithm eventually reaches a configuration in C BasicAlg reset . Remark 3. As it is stated in [START_REF] Kulkarni | Multitolerance in Distributed Reset[END_REF], whenever arbitrary states can be reached in the presence of faults, it is impossible to ensure (to design a resetting algorithm such) that every "resetting operation" (invoked by the reset signal in our case) is correct, i.e., necessary results in the predefined resetting configuration ( C BasicAlg reset ). This is because "the faults may perturb the resetting module (the reset algorithm) to a configuration where the reset operation has completed prematurely". Furthermore, notice that all known selfstabilizing reset algorithms ( [GM91, KA98, Var93, APSVD94, AO94, AH93, DH95]) have a similar specification.

The precise specification of the reset problem that we solve is given below. Recall that, for a given sub-algorithm Alg, we denote by C Alg the projection of a configuration C to the variables of Alg. We assume that there is a non-empty set C ResetAlg normal of terminal configurations contained in the set of "good" configurations C

ResetAlg saf e and where each node is in a normal status (i.e., executing no reset actions locally) -see Def. 8. We define a configuration C in C ResetAlg saf e satisfying the following conditions: 1. nodes are consistent (see Sub-section IV.2.1.2 for the definition), 2. either the status of any node is normal and it has no signal or, the status is reset (just executed a reset locally) and, 3. any node with the status normal has only parents with status normal and nodes with status reset have children with only status reset. The formal definition is given in Definition 9. We also assume that a configuration C BasicAlg reset of BasicAlg has been precisely defined. We give the definition of the problem under the form of conditions on executions.

Definition 7 (Specification of the Self-stabilizing Reset Problem).

(Convergence) Starting from an arbitrary configuration, eventually a configuration in C

ResetAlg saf e is reached.

(Termination

IV.2.1 -ResetAlg

In ResetAlg, nodes communicate over a rooted tree. Although we use only the doublefan tree of depth 2 for solving SMP, we present a reset algorithm for any rooted spanning tree. Each node has a variable status. BasicAlg launches or generates a signal by setting a specific boolean variable (signal) to True. When receiving a reset signal, a node, only if its status is set to normal, changes for initiate to inform its parent that a reset is in progress, and so on up to the root. Then, successive waves are initialized by the root. First a freeze wave (changing status to f reeze) goes down to the leaves. During this wave, nodes are inhibited, i.e. they are not eligible for any rule and wait for the next wave. The second wave goes from the leaves to the root: nodes are activated to reset the requested values (through a function reset_BasicAlg_variables() provided by BasicAlg) and switch to reset status to inform their parents. Once the wave reaches the root, all nodes have been activated for the reset and C BasicAlg ). Nodes are now ready to return to the normal status: the third wave (normal status) is initiated by the root. When this wave ends, all nodes are in the normal status and do not change until a possible next reset request.

Notice that during this process, when status = normal, the rules of BasicAlg are not enabled, neither request reset signals are accepted. This is important to allow reaching C BasicAlg reset . Indeed, if BasicAlg could be executed when a node has its status variable set to reset (i.e. just after the execution of the reset function), BasicAlg's variables could be modified before all nodes were activated for the function (because of the asynchronous unfair demon). In this case, C BasicAlg reset would never be reached. Thus, BasicAlg's rules can be executed at a node only when this node has its status variable set to normal.

IV.2.1.1 -Variables, Registers, Predicates, Functions and Procedures

(for a node v)

Variables.

• status: in {normal, initiate, f reeze, reset}.

normal indicates that the node is not aware of any ongoing reset, i.e. the node may be eligible for BasicAlg.

initiate is used to inform the parent that a node wants to launch a reset. This information goes from the initiator of the reset to the root.

f reeze is used by the root to freeze the nodes down to the leaves.

reset is used to inform the parent (and finally the root) that descendants of the node v have already performed the reset.

A node with status = normal is called a normal-node. Similarly, we derive a f reeze-node, a reset-node and an initiate-node.

• parent: written by the spanning tree algorithm and only read by the reset algorithm.

• signal: boolean written by the environment (BasicAlg or other external module) to request a reset (if True). We say that a signal is generated/launched when this variable is set to True.

Registers.

• st v,u ∈ {normal, initiate, f reeze, reset}: aiming to have the copy of the v's status value in the shared register read by u.

Predicates.

The three following predicates are used by the node v to distinguish between root, internal node or leaf :

• I_am_Root ≡ parent v = v.
• I_am_Leaf ≡ children(v) = ∅ (see the next section for the definition of children(v)).

• I_am_Internal ≡ ¬I_am_Root ∧ ¬I_am_Leaf.

Functions & Procedures.

• reset_BasicAlg_variables(): resets variables of the basic algorithm to their values in C

BasicAlg reset .

• children(v): returns the set of children of v. Children are determined by the tree algorithm (Algorithm 5).

• update_variables(new_status): updates the local and shared variables.

status ← new_status if(¬I_am_Root) : st v,parent ← new_status if(¬I_am_Leaf) : ∀u ∈children(v), st v,u
← new_status This procedure is used all along the algorithm to propagate the waves over the tree.

IV.2.1.2 -Additional Definitions

A node v is said consistent (with its shared registers) if ∀u ∈ N (v) : st v,u = status. A configuration is said consistent if every node is consistent. Notice that this property is checked by a node using the rule Variables_Consistency. ). The set of ResetAlg's safe configurations

C ResetAlg saf e
is defined by the following predicate : (status root = normal ∧ ¬signal) ∧ (∀v ∈ V \ {root} : [(status v = status parentv = normal) ∨ (∀u ∈children(v):

status v = status u = reset)] ∧ [(status v = normal ∧ ¬signal) ∨ status v = reset]
) and all nodes are consistent. For example, the figure 5.10 represents a safe configuration on a tree of depth 2, assuming that it is also consistent. Nodes with status = normal are denoted by letter with a n and those with status = reset are denoted by a r.

IV.2.1.3 -Algorithm

The reset algorithm (Algorithm 6) is specified by the rules described below. They are presented by decreasing priority order, Reset_Launch having the highest priority and Back_Normal the lowest. If several rules are enabled for the same node v in a configuration C, the node is only eligible for the rule with the higher priority.

• The rule Reset_Launch is used by a normal-node to check whether the reset signal has been launched by the composition (if signal is True). In this case, variables are set to initiate to launch the waves (explained in the beginning of Section IV).

• The rule Variables_Consistency is used to check whether all shared variables st of the node contain v's status, i.e., this rule checks the consistency of the node. If enabled, the rule sets local and shared status variables to initiate to report the inconsistency.

• The rule Neighbors_Coherence is used by a non-leaf reset-node to check whether its children have also status reset, i.e. to check whether the reset wave is from the leaf to the root. If not, the rule sets local and shared status variables to initiate to report the incoherence between neighbors.

• The rule Initiate is executed either by the root to register that a reset is requested, or by internal normal-nodes to transmit to their parents the reset request of a child by setting its variable st v,parent to initiate.

• The rule Freeze is executed by a node to transmit down the f reeze wave. Since the f reeze wave goes from root to leaves, a node checks if its children are not already in status f reeze or reset. Indeed, if a child has status ∈ {f reeze, reset} this means that there is a rest of an older wave and if the node is activated now for Freeze, there is no guarantee that its children will be activated for Reset. Thus, the node is blocked until all its children have either normal or initiate status.

• The rule Reset is executed by a f reeze-node if either it is a leaf or if all its children are in the status reset (for the root and internal nodes), i.e., have already been activated for Freeze. This rule executes the procedure reset_BasicAlg_variables() of the basic algorithm and propagates the reset wave up to the root.

• The rule Back_Normal is executed by a reset-node to return to the normal status after the reset wave. Thus, it checks if its children have also status reset. This unfreeze wave is launched by the root and goes down to the leaves. Notice that the signal variable is set to False during this transition to delete remaining signals that have not been receipted.

Algorithm 6 Reset Algorithm ResetAlg for v ∈ V 1: Reset_Launch : 2: {status = normal ∧ signal} 3:
update_variables(initiate)

{status / ∈ {f reeze, reset} ∧ (∀u ∈children(v): st u,v / ∈ {f reeze, reset}) ∧ 20: [(¬I_am_Root ∧ st parent,v = f reeze) ∨ (I_am_Root ∧ status = initiate)]} 21:
update_variables(f reeze)

{status = reset ∧ ([(∀u ∈children(v): st u,v = reset) ∧ I_am_Root] 31: ∨ [¬I_am_Root ∧ st parent,v / ∈ {f reeze, reset}])} 32:
update_variables(normal)

33:

signal ← False

IV.2.2 -Correctness and Complexity Analysis of ResetAlg (Algorithm 6)

A sketch of the proof is in Sub-section IV.2.2.1 and the detailed proof in Sub-section IV.2.2.2.

IV.2.2.1 -Sketch

Assume that a rooted spanning tree of any depth has been built. In this section, we sketch the correctness (see Definition 7 for the self-stabilizing reset specification) and complexity proofs of ResetAlg. The full proof can be found in Section IV.2.2.2. Recall that C ResetAlg normal is defined in Definition 8 and C ResetAlg saf e is defined in Definition 9.

First, we prove in Sub-section IV.2.2.2.1 Lemmas 48, 49 and Corollary 6 used all along the proof. These technical lemmas concern some properties of the rules Vari-ables_Consistency and Neighbors_Coherence.

Then, we prove in Sub-section IV.2.2.2.2 that a configuration is terminal iff no node has status or its shared variables set to f reeze, reset or initiate (Lemmas 51, 52 and 53). Hence, a configuration is terminal iff nodes have status and shared variables set to normal (Proposition 5).

After this technical lemmas, the convergence and complexity of ResetAlg are proved.

In Sub-section IV.2.2.2.3, we prove the convergence of ResetAlg from any configuration to C

ResetAlg saf e

. The main idea is to show that the number of moves that a node can make depends on the moves of its parent, i.e. recursively, the total number of moves depends on the number of root's moves. Then, we focus on the root and prove the properties yielding the convergence to C ResetAlg saf e . Thus, we first show that a node is activated for at most 6 moves between two activations of its parent (Lemma 54). Hence in an infinite execution (not terminated), the root is activated infinitely many times too. During such an execution, after the root is activated twice for Reset, a specific configuration in which all nodes are coherent and have status reset is reached (Lemma 55 and Corollary 7). From this configuration, after one root's Back_Normal, a configuration in C

ResetAlg saf e is reached. Hence, during this execution, the root has been activated a constant number of times. Furthermore, since between each two moves of the root, its children are eligible for 6 moves and, recursively, its grandchildren are eligible for 6 2 moves, etc., C ResetAlg saf e is reached after O(n • 6 p ) moves, where p is the depth of the tree (Lemma 56).

Finally, in Sub-section IV.2.2.2.4, the termination of ResetAlg is proved. Using some lemmas of the previous section and with similar arguments, we show that, if there is no signal launched, from any configuration, C ResetAlg normal is reached after O(n • 6 p ) moves (Lemma 58). Indeed, from any configuration, after at most O(n • 6 p ) moves, a terminal configuration is reached, i.e. C ResetAlg normal is reached by Proposition 5. In Sub-section IV.2.2.2.5, we focus on the third point of the definition of the reset problem. Lemma 59 proves that the configuration

C BasicAlg reset is reached in O(n) moves from any configuration in C ResetAlg saf e
in which a signal is launched. Indeed, the waves proceed normally: the initiate wave reaches the root and then, f reeze and reset waves are initiated.

Finally, Theorem 4 concludes by proving that ResetAlg satisfies every condition of the reset specification in O(n•6 p ) moves. More precisely, in every of the three conditions, the configurations specified to be reached are reached in O(n • 6 p ) moves. Notice that on a tree of depth 2, this move complexity is of O(n) moves.

IV.2.2.2 -Detailed Proof

Recall that we assume that a rooted tree of any depth has been built. The proof is divided in five parts.

First, in Sub-section IV.2.2.2.1, technical lemmas (Lemmas 48-50 and Corollary 6) about some properties of the rules Variables_Consistency and Neigh-bors_Coherence are presented.

Then, in Sub-section IV.2.2.2.2, we establish that in the terminal configuration, all nodes are normal-nodes (Lemmas 52 -53). Thus, Proposition 5 states that C ResetAlg normal is the only terminal configuration of ResetAlg.

In Sub-sections IV.2.2.2.3, IV.2.2.2.4 and IV.2.2.2.5, we prove the tree conditions of the reset specification.

Finally, the main Theorem 4 in Sub-section IV.2.2.2.6 states that ResetAlg satisfies each of the three conditions in the reset specification in O(n • 6 p ) moves.

IV.2.2.2.1 -Preliminary Lemmas

This sub-section contains basic lemmas used throughout the proof. The first (Lemma 48) states that any node v is activated at most once for Variables_Consistency in any execution and, if v is not eligible at some point for Variables_Consistency, it never becomes such. Then, we prove that, from a configuration C in which no node has status = initiate and no node is eligible for Variables_Consistency and Neighbors_Coherence, no node becomes eligible for these two rules, as long as a reset signal is launched (Corollary 6). This is done using Lemma 49 in which we prove that, from C, the guard condition of Neighbors_Coherence's rule cannot be True.

Finally Lemma 50 proves that nodes cannot be activated more than once for Neigh-bors_Coherence.

Lemma 48. In any execution, 1. if a node v is not eligible for Variables_Consistency, it will never be eligible for Variables_Consistency and, 2. a node v is activated at most once for Variables_Consistency.

Proof. The only way for a node to change its status and the values of its shared registers is to execute the function update_variables(). Any activation of this function makes the rule Variables_Consistency no more enabled. The function is executed at each rule activation. Thus a node that is eligible for Variables_Consistency becomes not eligible for this rule after its activation and a node that is not eligible remains not eligible after activation of any rule. That proves the lemma.

Lemma 49. Let C be a configuration in which no node is eligible for Vari-ables_Consistency and Neighbors_Coherence. In any execution from C, the rule Neighbors_Coherence is never enabled.

Proof. We recall that the condition for Neighbors_Coherence to be enabled is Cond

= ∃v : ¬I_am_Leaf ∧ status v = reset ∧ (∃c ∈children(v): st c,v = reset).
Notice that Variables_Consistency is not enabled in any execution from C (from Lemma 48 and the lemma's assumptions). We prove the lemma by contradiction and consider the first configuration C' in which Cond is True for a node v.

There are three cases to consider, according to the last move before reaching C'.

1. The child c has status c = reset and v has executed a rule that sets status to reset, 2. v has status v = reset and children c has executed a rule that sets its status to a different value than reset, or 3. both c and v are activated in the same step: v switches to reset while c takes a status different from reset.

Case 1. The only rule that sets the status to reset is Reset. But v is eligible for this rule only if all its children are reset-nodes. Thus Case 1 is not possible.

Case 2. Since v is not eligible for Neighbors_Coherence in C, status c = reset. The only rules that make c's status different from reset are Neighbors_Coherence or Back_Normal. But, Neighbors_Coherence is not enabled in C. Furthermore, since status v = reset, c cannot be eligible for Back_Normal. Thus Case 2 is not possible.

Case 3. The only possibility for v to set status to reset is when executing the rule Reset with status = f reeze. If v is eligible for Reset, status c = reset. Thus, c is possibly eligible only for Back_Normal or Neighbors_Coherence. But it cannot be eligible for Back_Normal because v has status reset and it cannot be eligible for Neighbors_Coherence because C' is the first configuration in which this rule is enabled. Thus Case 3 is not possible.

That ends the proof of Lemma 49. Let us now focus on the execution between C 3 and C 5 and suppose that c, a child of v, is an initiate-child in C 5 . Since before C 3 , c has been activated for Reset and in C 5 , c is an initiate-node, c is activated for Neighbors_Coherence before C 5 , from C 4 . Indeed, others rules that set the status to initiate cannot be enabled (Back_Normal not enabled). Similarly, at least one c's child cc has been activated for Neighbors_Coherence between c activation for Reset and C 4 . Recur-sively, the argument applies on internal nodes (leaves cannot be activated for Neigh-bors_Coherence). Thus, the contradiction arises when an internal node has only leaves as children. It has no child u eligible for Neighbors_Coherence and there is no other possibility to set its status to initiate in this configuration from the status reset.

Thus, nodes are not eligible twice for Neighbors_Coherence.

IV

v = f reeze in C, v cannot be a leaf.
Consider now that v is either the root or an internal node. Since C is terminal, v is not eligible for Reset. Thus, ∃c ∈ children(v) : st c,v = reset. There are two sub-cases: (a) status c ∈ {normal, initiate} or (b) status c = f reeze.

Case (a) is possible only if c is not eligible for Freeze, i.e. c is an internal node (if c is a leaf, it would be eligible for Freeze with no condition) with a child cc with status cc ∈ {f reeze, reset}. If cc is a reset-node, it is eligible for Back_Normal with no condition on its children. Hence, if c is not eligible for Freeze, a c's child cc has status cc = f reeze and is an internal node (leafs cannot have status = f reeze, see the previous paragraph). This leads to the same case as for v, cc is an internal node with at least one child ccc with : st ccc,cc = reset. This pattern of status' values can be repeated with some case (b) in between, but none of the node of the pattern can be a leaf. Hence, case (a) is possible only if the branch of f reeze-nodes ends with at least one case (b) (a node and one of its child with status = f reeze). But since leafs cannot have status = f reeze, this is not possible.

Similarly, case (b), is not possible. First, c cannot be a leaf by the previous paragraph. Hence, v has status v = f reeze only if v is the root or an internal node and if at least one of its children c is an internal node and has status c = f reeze. Recursively, c has at least one child satisfying also these conditions and so on. But since the tree has a finite depth, this is not possible: there is at least one internal node with only leaf children.

Thus, no node has status = f reeze in a terminal configuration.

Lemma 52. In a terminal configuration, no node has status = reset.

Proof. Assume that there exists a node v with status v = reset in a terminal configuration C. In C, nodes are coherent (i.e. shared and local variables are equal) otherwise Variables_Consistency would be enabled. First, let us consider that v is the root. Since C is terminal, ∃c ∈ children(v) : st c,v = reset, otherwise v would be eligible for Back_Normal. But c cannot have status ∈ {normal, initiate, f reeze} because of Neighbors_Coherence. Thus, v cannot be the root in C. Now, let us consider that v is an internal node or a leaf. Let p be its parent. st p,v ∈ {reset, f reeze}, otherwise Back_Normal would be enabled for v. But, by Lemma 51, status p = f reeze. Hence, v has status v = reset only if its parent has status p = reset. Recursively, p's parent pp has also status pp = reset and so on. But the last parent is the root r and by the previous paragraph, status r = reset. Thus, this case is also impossible.

Thus, no node has status = reset in a terminal configuration.

Lemma 53. In a terminal configuration, no node has status = initiate.

Proof. Assume that there exists a node v with status v = initiate in a terminal configuration C. In C, nodes are coherent (i.e. shared and local variables are equal) otherwise Variables_Consistency would be enabled. Furthermore, from Lemmas 51 and 52, no node has status ∈ {f reeze, reset} in a terminal configuration.

If v is the root. v's children may have only status normal and initiate. In both cases, v is eligible for Freeze. Thus, v cannot be the root in C. Now, let us consider that v is an internal node or a leaf. If the parent p of v has status p = normal, p is eligible for Initiate. Thus, p has status p = initiate. Recursively, p's parent pp has also status pp = initiate and so on. But the last parent is the root r and by the previous paragraph, status r = initiate. Thus, this case is also impossible.

Thus, no node may have status = initiate in a terminal configuration.

Proposition 5. A configuration C is terminal iff it satisfies PredRTerm ≡ ∀v ∈ V :

status v = normal ∧ nodes are consistent ∧ ¬signal v , i.e. it is C ResetAlg normal .
Proof. First, notice that C ResetAlg normal is terminal. Indeed, it is easy to see that no rule is enabled.

Let C be a terminal configuration. Since Variables_Consistency checks the consistency of nodes, they are consistent with there shared registers. By Lemmas 51, 52 and 53 no node has status initiate, f reeze or reset. Then they are normal-nodes. Finally, there is no signal: a normal-node with a signal would be eligible for Re-set_Launch. Thus, C satisfies PredRTerm i.e., C is C ResetAlg normal .

IV.2.2.2.3 -Convergence Properties of ResetAlg (Condition 1 of Def. 7)

In this section, we focus on the convergence property of ResetAlg as defined in the reset specification (Definition 7):

(Convergence) Starting from an arbitrary configuration, eventually a configuration in

C ResetAlg saf e is reached.
This part is proved counting the number of moves made by each node. Indeed, we prove first that a node can be activated at most 6 times before its parent is activated once (Lemma 54). We also prove that the root can be activated at most 9 times (Corollary 57) using the fact that it can be activated twice for Reset (Lemma 55). Thus, a node at depth p can be activated 9 • 6 p times. This results in an overall complexity of O(n • 6 p ) moves (Lemma 56). From the configuration reached by the second root's Reset, we prove that a configuration in C ResetAlg saf e is reached in 1 move. We first prove that if a node is not activated, its children are activated for at most 6 moves.

Lemma 54. Let C be any configuration and C' be a configuration from which a node v is activated for any rule. In the execution C * → C', v's children are activated for at most 6 rules.

Proof. Since some rule check the register of the parent and other do not, let us analyze the longest sequence of activations before C' of one v's child c (the figure 5.11 represents the possible transitions from each status value).

Thus, if st v,c = initiate, c can be activated for at most 3 moves (in the order: Reset then Back_Normal and then Initiate or Reset_Launch, when status c = f reeze and c is coherent).

If st v,c = reset, c can be activated for at most 2 moves (first Reset and then Neighbors_Coherence, when status c = f reeze and c is coherent). Indeed, in these cases, Back_Normal nor Freeze can be enabled since st v,c = reset satisfies none of their conditions.

If st v,c = f reeze, c can be activated for at most 6 moves (Initiate or Vari-ables_Consistency or Reset_Launch or Neighbors_Coherence, then Freeze, then Reset, then Neighbors_Coherence, then Freeze and finally Reset, for any value of status c ). Notice that after the second Reset, c cannot be activated again for Neighbors_Coherence. Indeed, since Freeze and Reset check the st values of the children, between Freeze and Reset, c children have been also activated for Freeze and Reset. Thus, recursively, all children of c are coherent and have status = reset when c is activated for Reset, i.e. none of them can change their status to an other value and allowing its father to be activated for Neighbors_Coherence.

Finally, if st v,c = normal, c can be activated for at most 3 moves (Reset, Back_Normal and Initiate, when status c = f reeze and c is coherent).

Thus, if v is activated from C, each of its children may be activated for at most 6 moves.

In the following figures, the possible transitions (from a status to another) are depicted. Edges represent the transitions and the nodes of this diagram the resulting status value after a transition. The rules that can be applied to make a transition are giver over every edge. Some rules are labeled by " " and "1". "1" means that the rule is activated only once (for example Variables_Consistency, by Lemma 48 or Neigh-bors_Coherence by Lemma 50). " " means that this transition is not possible for the leaves. We now consider the root r: if r is activated twice for Reset, we can deduce the configuration reached after r is activated for Reset the second time. In this configuration, all nodes v are coherent and have status v = reset (Lemma 55 and Corollary 7). An illustration of the execution mentioned in the following lemma and the corollary is given in Figure 5.12. First, since status r = f reeze in C', the last activation of r before C' is for Freeze in a configuration C 1 . Thus in C 1 , ∀c ∈ children(r): st c,r / ∈ {f reeze, reset} is True but in C', ∀c ∈ children(r): st c,r = reset. Hence, between C 1 and C', all children of r have been activated to change their variables and the last activation of each of them is for Reset (notice that in C', children are coherent since they have been activated at least once). To be activated for Reset, a node must be a f reeze-node, then its last activation before Reset is for Freeze.

Recursively, the children of a r's child c is also only activated for Freeze and Reset (in that order) between the two activation of its parent for the same reasons. This induces that a node is activated for Reset only if its children are in status reset. Thus, in C', all nodes are in status reset (Neighbors_Coherence not enabled since one of its children must be in status initiate and Back_Normal is enabled if its parent is in status normal and it is in status f reeze).

The following execution is depicted in Figure 5.12. For example, let us consider a tree of depth 2 and a child c of r. Let C 2 , respectively C 5 , be the configuration in which c is activated for the last time for Freeze, resp., for Reset. If c is a leaf, between C 5 and C' c is not eligible, that is, status c = reset and c is coherent in C'.

If c is an internal node, in C 2 ∀cc ∈ children(c): st cc,c / ∈ {f reeze, reset} is True and in C 5 , ∀cc ∈ children(c): st cc,c = reset is True. As for r, the two last activations of any child cc of c before C 5 , are for Freeze and Reset.

As the tree is of depth 2, cc is a leaf. Let C 3 , respectively C 4 , be the configuration from which cc has been activated for Freeze, resp. for Reset. Thus, in C 5 , status cc = st cc,c = reset holds, i.e. cc is coherent. Between C 5 and C', cc is not eligible (no rule can be enabled). After c's Reset from C 5 , c has status c = reset and is coherent. From this configuration, it cannot be eligible for any rule.

Corollary 7. In the conditions of Lemma 55, let C" be the configuration reached from C' by activating Reset at r. In C", all nodes v are coherent and have status v = reset.

Proof. Direct consequence of the r's Reset activation in C'.

Figure 5.12 is a schematic representation of the necessary successive activations analyzed in the proof of Lemma 55 and Corollary 7. For simplicity, we illustrate the scenario only over the double-fan tree, but the proofs work for any rooted tree. The three levels of the double-fan tree are represented vertically (r stands for the root W min , c for its children and cc for the children of M min ). Time runs from left to right and the sequence of configurations considered in the proof are depicted in a chronological order (on the top of the figure). The conditions allowing the activation of the rules are indicated vertically in red: re is for reset, f for f reeze and i for initiate. Thus, for example, on the first horizontal line, the first left bended arrow represents r's activation for Reset during the transition from C. If the reached configuration is used in the proof, it appears in the figure, otherwise it is not. Proof. First, by Lemma 55, the root r is activated at most twice for Reset from C. Let C 1 be the configuration from which r is activated the first time and C 2 the configuration from which r is activated the second time (such that C 1 * → C 2 ). By Corollary 7, all nodes v (except the root) are coherent and have status v = reset in C 2 . This configuration is reached after at most 8 moves: before C 1 , r can be eligible for at most 3 moves (Back_Normal, Initiate or Reset_Launch and then Freeze) and between C 1 and C 2 , r can be activated at most for the 3 same moves.

C C 1 C 2 C 3 C 4 C 5 C' C"
Since by Lemma 54, children of a node v are activated at most 6 times before one v's activation, each children of r are activated at most 8 • 6 = 48 times. Recursively, the grand children are activated at most 8 • 6 • 6 = 288 times. More generally, a node at depth p is activated at most 8 • 6 p times.

By Lemma 55, r is the only eligible node in C 2 . After its activation, all nodes v (r included) are coherent and have status v = reset. In this configuration, r is again the only eligible node (for Back_Normal). After its activation, status r = normal ∧ ¬signal ∧ ∀v ∈ V \ {r} : status v = reset (Back_Normal sets signal to False) and all nodes are coherent (they all have been activated at least once for a rule). Hence, this configuration is in C ResetAlg Proof. First, by Lemma 55, the root is activated at most twice for Reset from C. Let C 1 be the configuration from which the root is activated the first time and C 2 the configuration from which the root is activated the second time (such that C 1 * → C 2 ). By Corollary 7, all nodes v are coherent and have status v = reset in C 2 . Altogether, by Corollary 57, the root is activated at most for 9 rules.

Since by Lemma 54, children of a node v are activated at most 6 times before one v's activation, each children of the root are activated at most 9 • 6 = 54 times. Recursively, the grand children are activated at most 9 • 6 • 6 = 324 times. More generally, a node at depth p is activated at most 9 • 6 p times.

Notice that nodes could be eligible after the last activation of the root but since in C 2 all nodes v are coherent and have status v = reset, the only possible activation for each node is once for Back_Normal (in absence of new signal).

This leads to the conclusion that, if there is no new signal, the algorithm converges to C ResetAlg normal in O(n • 6 p ) moves from any configuration. Recall that when the variable signal is set to True, we say that a signal is generated. Possible moves are analyzed in Lemma 59 in order to prove that, if from any configuration in C

IV.2.2.2.5 -Re-initialization of

ResetAlg saf e at least one signal is generated, then C BasicAlg reset is reached (i.e., each node has executed reset_BasicAlg_variables()). The following lemma is illustrated by Figure 5.14 on a tree of depth 2, but is proven for any rooted tree. In C 1 , v is eligible for Reset_Launch. normal-node are not eligible and resetnodes are eligible for Back_Normal if their parent are normal-nodes. Thus, after at most O(n) Back_Normal, v is activated for Reset_Launch: this is the start of an initiate wave. If several nodes have received a reset signal and have been activated for Reset_Launch, the initiate wave comes from several parts of the tree but an initiate-node cannot be activated several times for Initiate. Since v's parent are all normal-nodes, this wave reaches the root after at most O(n) Initiate. Then, if all children of the root are normal-nodes, the root may transform the initiate wave into a f reeze wave. Notice that, if its children are still reset-nodes, the root waits till its children are activated for Back_Normal (since there is a finite number of other possible rules, its children are activated at some point). The f reeze wave is broadcasted with the same mechanism if some children are reset-nodes. When the f reeze wave reaches the leafs, the reset wave begins and is convergecasted. Hence, after O(n) more moves, a configuration C" in which nodes are all reset-nodes after having executed Reset is reached. Indeed, reset-nodes are neither eligible for Back_Normal (their parents must be normal-nodes) nor for Neighbors_Coherence (Lemma 49). Since all nodes have executed Reset as last rule before C" and that BasicAlg is not eligible while nodes are not normal-nodes,

C BasicAlg reset is reached in C".
The following figure illustrates the execution of Lemma 59: from a configuration in which a node has signal set to True, C BasicAlg reset is reached. We use the same notations as in Figure 5.12. Though this upper bound is high, assuming that the underlying tree is constructed by the algorithm TreeAlg proposed in Section IV.1, that is with p = 2, ResetAlg converges and performs the reset in O(n) moves.

C 2 C 3 C 4 C 5 C 6 C 7 C 8 C"

V -Composition

In this section, we explicitly present the final combination of Async-GSA (Alg. 3 and 4) with the reset module ResetAlg (Alg. 6) composed itself with the tree construction al-gorithm TreeAlg (Alg. 5). All this, for obtaining a self-stabilizing version of Async-GSA (Alg. 7) following the transformation technique by local checking and global reset presented in Section II. Notice that ResetAlg resets an algorithm BasicAlg to a specific configuration called C BasicAlg reset in the previous section. For Async-GSA, this configuration is C Async-GSA init .

The main goal of this section is to analyze the move complexity of the final combination. This analysis is made especially difficult by the assumption of an unfair scheduler. When considering rounds (synchronous or not) under a fair scheduler, the analysis is easier because the notion of round hides the useless actions. That is not the case under an unfair scheduler. A rough worst case analysis in terms of moves results in the product of the stabilization times of the composition modules taken separately, i.e., in O(n 4 ). This is because an unfair scheduler may choose as long as possible to activate nodes in a "wrong order" of modules' rules they are eligible to execute. That is, it may constantly privilege activating nodes executing a module A, while A can correctly execute only after the stabilization of another module B. This "spends" moves which do not "contribute" to advance the stabilization of the whole composition (and implies a multiplication of stabilization times of modules). See the following Section V.2 for more detailed description on this issue.

Despite this difficulty, we make a thorough complexity analysis and obtain, in the worst case, only Θ(n 2 ) moves till the stabilization to a stable marriage, starting from any configuration. We obtain this by establishing priorities between the guarded rules (locally at each node -see Alg. 7), and by relying on the bipartite topology of the underlying graph.

V.1 -Composition Algorithm CompAlg (Alg. 7)

V.1.1 -Variables and Predicates (for a node v)

Variables.

• status: variable of the reset algorithm ResetAlg (Alg. 6), read only in CompAlg.

status ∈ {initiate, f reeze, normal, reset}. CompAlg verify whether or not the value of this variable is normal. That is, the node does not participate in the reset procedure. Only in this case, reset signals can be launched and the rules of Async-GSA executed (lines 12 and 17).

Predicates.

• GuardsTreeAlg: the disjunction of all TreeAlg's rule guards.

• GuardsResetAlg: the disjunction of all ResetAlg's rule guards.

• GuardsAsync-GSA: the disjunction of all Async-GSA's rule guards.

• LP m,w : a predicate defined in Definition 6 to prove the local checkability of Async-GSA; used by men to trigger a reset signal, whenever not satisfied.

• Tree_LC ≡ ∀u 1 , u 2 ∈ N (v): min u 1 ,v = min u 2 ,v . A predicate used to check the coherence of the shared registers of TreeAlg in all the neighbors of v. This is to prevent v from executing other than TreeAlg's rules while tree is not yet stabilized, thus improving move complexity.

V.1.2 -Algorithm

The composition algorithm manages the activations of its modules through the implementation of priorities. The rules are presented and executed in the decreasing priority order: the first rule Comp_Tree has priority over the others and the last rule Comp_SM can be enabled only if neither ResetAlg nor TreeAlg has an enabled rule. These priorities are implemented by mutually exclusive rule guards. Here are the guarded rules of CompAlg:

• Comp_Tree is enabled to execute the rules of TreeAlg if the tree is locally incorrect (i.e., at least on of its rules is enabled), according to GuardsTreeAlg.

• If the tree is locally correct according to GuardsTreeAlg and Tree_LC, Comp_Reset is enabled if GuardsResetAlg is also satisfied.

• The rule Comp_Local_Check is only enabled for men since LP m,w is only checked by men. Moreover, it should be with status = normal, with no tree or reset modules' rules enabled. Note that the checking "w in Women" is equivalent to w ∈ N (v) since v is a men. ∧((v ∈Men ∧ ∀w ∈Women:

LP v,w ) ∨ v ∈ Women) ∧ GuardsAsync-GSA} 17:
Async-GSA execution segment in the figure), while w is of type (1) in the beginning, and of type (2) after its activation for TreeAlg in some configuration C x (blue execution segment in the figure). A node u is of type (2) from the beginning.

C 0 C x C T C ResetAlg saf e C BasicAlg reset C M u w v last TreeAlg's rule of w last TreeAlg's rule of v time O(n 2 ) TreeAlg, ResetAlg, Async-GSA O(n 2 ) ResetAlg, Async-GSA O(n 2 ) ResetAlg, Async-GSA O(n 2 )
ResetAlg, Async-GSA We first prove that nodes of type (1) (like w or v) can be activated for a constant number of moves before their last activation for TreeAlg (Lemmas 60 -66). Thus, after a constant number of its own moves, a node switches to type (2) (like w in C x ).

Then, we prove that a node of type (2) (like u or w after its last activation for TreeAlg) is eligible for O(1) moves of ResetAlg and O(n) moves of Async-GSA before C T is reached, i.e., till PredT becomes satisfied (Lemma 67). Concerning the O(1) moves of ResetAlg, the main argument is that ResetAlg proceeds in "waves" (of broadcast and convergecast) propagated over a tree of depth 2 and coordinated by the root. But since the tree is not stabilized yet before C T , waves cannot be propagated, leading to a constant number of ResetAlg's moves. This implies that each type (2) node can be activated a constant number of times for O(n) moves of Async-GSA, since a node can perform O(n) moves in Async-GSA and partial ResetAlg can reset Async-GSA's variables of the node a constant number of times. Thus, C T is reached after O(n 2 ) moves (Lemma 67).

Concerning the second part, after the tree has been built, in the worst case, an execution is divided into three additional sub-parts: i) an initial sub-part in which a partial reset (propagated on the tree) is executed, ii) a second sub-part during which a reset is performed after being triggered in a safe configuration (see Definitions 7 (self-stabilizing reset problem) and 8 (safe configuration)) and iii) a third sub-part, which corresponds to an execution of Async-GSA with the correct initialization. We discuss upper bounds for each of these three parts.

We first consider the sub-part i) with the partial reset. By Lemma 56, ResetAlg converges to C ResetAlg in which the reset can be triggered by some incoherent nodes (regarding its state and its neighbors' registers) or nodes involved in a blocking pair. The other nodes simply execute rules of Async-GSA (Algorithms 3 (women) and 4 (men)). The longest execution segment of this part is obtained when the unfair scheduler chooses to ignore the incorrect nodes (from executing the enabled rules of the incoherence detection -rule Comp_Local_Check). This may take at most O(n 2 ) moves (of the Async-GSA rules): after a partial stable marriage has been built with the correct nodes (those that do not detect any incoherence) using Async-GSA, these nodes are no more eligible, at least because no woman can make a new proposal, as the end of her preference list has been reached or a partner has been found. The task of building a partial stable marriage takes O(n 2 ), still from Lemma 44. Then, an incorrect node is activated, triggering a reset. The triggered reset ends after O(n) moves, resetting Async-GSA to C This justifies the overall complexity of O(n 2 ) moves (Theorem 5). This bound is also correct in terms of rounds and is tight (see the scenario reaching it in Sub-section III.3).

V.2.1 -Stabilization of the Tree (to PredT)

Lemma 60. From any configuration, a man v is activated for at most 1 move (of TreeAlg) before its last activation for TreeAlg.

Proof. Let C be any configuration. In C, v is either eligible for TreeAlg or not eligible for TreeAlg. Notice that, by Lemma 45, men are eligible for at most 2 moves: Update and I_am_not_root.

If v is not eligible, it cannot become eligible for these two rules. Indeed, these rules check only v's variables (for the men): if these variables are already with the 'good' values, no other rule can change them. Thus, v is never eligible for these rules.

If v is eligible for TreeAlg's rules, it is for Update and/or I_am_not_root. If it is only for one rule, it becomes not eligible after its activation and v is in the previous case: it cannot become eligible for the other rule. If v is eligible for both, it cannot be activated for another rule between the activations. This is because, if I_am_not_root is activated, it is already eligible in C and because the actions of I_am_not_root rule do not affect the variables verified by the guard of Update (and vise versa). Thus, a man v can be activated for at most 1 move before its last TreeAlg's activation.

Lemma 61. Let C be any configuration in which there is a woman w not eligible for TreeAlg and with Tree_LC not satisfied. From C, w is not activated for any move before its last activation for TreeAlg.

Proof. Since w is not eligible for any TreeAlg's rule in C, Update is never enabled for w (shared registers are already consistent and not other rule change their values). Furthermore, since Tree_LC is not satisfied and v is not eligible for TreeAlg in C, I_am_not_root is not the first TreeAlg's move of w.

Hence, w is activated for I_am_root, when all neighbors agree on the min value True. Between the last Update activation of w's neighbors and the activation for I_am_root, Tree_LC is satisfied. But w is already eligible for I_am_root, i.e., w cannot be activated for any other rule before I_am_root (rules's priorities). Furthermore, since men have been activated for Update, this induces that their min value are correct: w is the root. Thus, it cannot be activated for I_am_not_root after I_am_root. I_am_Root is its last TreeAlg's activation, after no other move. Lemma 62. Let C be any configuration in which there is a woman w eligible for TreeAlg and with Tree_LC not satisfied. From C, w is activated for at most 2 moves (of TreeAlg) before its last activation for TreeAlg.

Proof. In C, w is eligible for Update and/or for I_am_not_root (Tree_LC not satisfied). After these activations, either w is no more activated for TreeAlg (the last activation for TreeAlg already happened) or there is a last activation for I_am_root (women are eligible for at most 3 moves, once for each, by Lemma 46). We consider the case in which w will be activated for I_am_root. Since in C, Tree_LC is not satisfied, neighbors are activated for Update and will agree on the min value True in a configuration C 1 . Any other rule is enabled for w during this time: Tree_LC is not satisfied. In C 1 , w is eligible for I_am_root and this is its last activation for TreeAlg.

Thus, after at most 2 moves of TreeAlg, w's next activation is for its last TreeAlg's rule.

Lemma 63. Let C be any configuration with a woman w that is not eligible for TreeAlg and that satisfies Tree_LC. From C, before the first activation of one of its neighbors, w can make at most 5 moves.

Proof. In C, since Tree_LC is satisfied for w, all w's neighbors agree on a min value.

We analyze first the number of moves that w can make with ResetAlg before any activation of its neighbors. If neighbors' min values are True, w "thinks" that she is the root. • Or Tree_LC is not satisfied and w not eligible for TreeAlg (during the same transition, w is activated for I_am_not_root and at least one of its neighbors is (and not all)activated for Update). By Lemma 61, w is only eligible for it last TreeAlg's activation.

• Or Tree_LC is not satisfied and w eligible for TreeAlg (during the same transition, w is activated for I_am_root and at least one of its neighbors (and not all) is activated for Update). By Lemma 62, after at most 2 moves, w is activated for it last activation.

• Or Tree_LC is satisfied and w eligible for TreeAlg. This last case is only possible if during the same transition, w is activated (for I_am_not_root or I_am_root) and all its neighbors are activated for Update. Thus, w is eligible for I_am_root if it has been activated for I_am_not_root earlier or reciprocally. This move is the last TreeAlg's activation since women may be activated at most once for each TreeAlg's rule.

Notice that the same argumentation leads to the same result if w is activated first for I_am_root or I_am_not_root and then for Update.

Thus, after at most 9 moves (2 first TreeAlg's rules + 7 of Lemma 64), w's next activation can only be for its last TreeAlg's rule.

Lemma 66. From any configuration C, a node v is activated for at most 9 moves before its last activation for TreeAlg.

Proof. In C, v can be of four different types:

1. Tree_LC is not satisfied but v is not eligible for TreeAlg, 2. Tree_LC is not satisfied and v is eligible for TreeAlg, Reset_Launch or Neighbors_Coherence). In this case, the initiate wave may possibly reach the root (if it is not blocked at some point) and be transformed in a f reeze broadcast wave. But this wave cannot end and be transformed in a successfully reset wave since the tree is not complete. Furthermore, the next join cannot shift the f reeze-nodes back to initiate.

Furthermore, women that are activated for TreeAlg may be activated for a constant number of Async-GSA's and ResetAlg's moves before their last TreeAlg's activation (men cannot by Lemma 60). But these moves do not influence nodes in S. Indeed, those women are activated for Async-GSA's and Reset only in the context of Lemmas 64 and 65, i.e. they are eligible for those moves when men on the other side are all eligible for TreeAlg thus, are not in S.

Hence, over this (dynamic) forest structure where GuardsTreeAlg is not satisfied (and thus PredT is satisfied) for every node (in the segment from C to C 1 ), at most O(n 2 ) moves are executed by the nodes, by Lemma 68 (including the joining nodes after their own O(1) moves of any type, by Lemma 66). Thus, there is no infinite cycle and after O(n 2 ) moves, the last eligible node for TreeAlg is activated and a configuration C 1 satisfying PredT is reached. : Lemma 56 is proven with no condition on signals. Since each node is activated a constant number of times for ResetAlg's rules and thus is a constant number of times with status = normal, each man can be activated a constant number of times for Comp_Local_Check (Comp_Local_Check changes the status to initiate). That is O(n) additional moves for Comp_Local_Check before C 1 . Furthermore, between C and C 1 , every normal-node (and with all LP True for men) can also be activated for Async-GSA, and all such nodes together for O(n 2 ) moves (by Lemmas 42 and 41). Notice that, since ResetAlg is activated only for O(n) moves, Reset is activated a constant number of times for each node. The activation of a node for Reset does not influence the Async-GSA's moves of other nodes: when a man is activated for Reset, the only incidence is that women may be stuck in the process of proposal/acceptance (since the request's value does not correspond anymore to the process and thus to the rules' guards) and when a woman is activated for Reset, men may be eligible for Comp_Local_Check. Hence, a node may not be restarted for Async-GSA more than a constant number of times. Thus, after O(n 2 ) moves (of all algorithms together) C 1 is reached.

V.2.2 -Convergence after

When

VI -Conclusion

In this chapter, we have presented our second asynchronous self-stabilizing algorithm for SMP. This algorithm is built using the local checkability scheme of [START_REF] Awerbuch | Self-stabilization by local checking and global reset[END_REF] that we adapted to our model and purpose (Definition 6). Local checkability is a wellknow method allowing to compose a non-self-stabilizing algorithm, a local detector and a reset components in order to build a self-stabilizing version of the given initialized algorithm. Though the technique is well known, it had to be adapted in a delicate way. Moreover, neither it provides the move complexity of the composition, nor the components themselves are provided automatically.

For being able to use the adapted version of this technique we first designed a non-self-stabilizing algorithm to be transformed. This is an asynchronous distributed version of GSA (Async-GSA -Alg. 3 and 4) that solves SMP in Θ(n 2 ) moves. Since no self-stabilizing reset algorithm running under an unfair daemon in a link register model was designed and analyzed (for move complexity) before this work, we design also a reset algorithm (ResetAlg -Alg. 6) executed over an underlying rooted tree. Thus, we propose also a tree construction algorithm (TreeAlg -Alg. 5) that builds a rooted tree of depth 2 in O(n) moves. The reset algorithm runs on this tree and its move complexity is O(n).

Then, we compose those algorithms together (Async-GSA, TreeAlg, ResetAlg and the detector into CompAlg -Alg. 7) in a way providing a self-stabilizing version of Async-GSA that solves SMP in Θ(n 2 ) moves. The complexity analysis reaching this bound is intricate and constitutes one of the main contributions of this thesis. Finally note that all algorithms use registers of only few bits, and the confidentiality of the preference lists is always kept. Many variants of the original stable marriage problem were studied. Each corresponds to a particular application domain. We consider some of them and discuss the possibility to obtain self-stabilizing solutions based on the algorithms we proposed (Chapters 4 and 5) for the basic problem. In each case, we study how these algorithms can be adapted. First, the definitions of preference list and consequently of blocking pair and stable matching must be extended. In some cases, the solution is an easy adaptation of the solutions for the basic stable marriage. In some other cases, the algorithms must be more deeply modified, as well as their proofs, but stay relevant. Finally, there are cases where, due to the particularity of the proposed algorithms (e.g., the extensively used phase breakdown or the local checkability), suitable simple adaptations are inappropriate and different approaches are required. These cases are discussed as perspectives in Chapter 7, Section II.

The variants, for which we present a solution, are all mentioned in the reference book of Gusfield and Irving [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF]. Their names are: stable matching with unequal sizes of opposite sets, stable matching with indifference (ties in preference lists), stable matching with unacceptable partners (incomplete lists), many-to-one matching (Hospitals/Residents problem) and many-to-many matching. In the following, each variant is considered separately. It is explained and the required changes to the algorithm and to the proof are indicated. Notice that the modifications for each case are presented in such a way that they can be simply combined together to obtain a general algorithm covering all the different variants. It is also interesting to notice that the changes (when needed) are very similar for both algorithms. This observation comes from the fact that in both cases we use local checking.

We start by extending the basic definition of stable matching, to have a uniform framework for the considered variants.

First, to allow many-to-many (and many-to-one) matchings, each node v must be matched to at most b ≥ 1 partners. In this case, b is called the capacity and v is said to be b-matched if it is matched with exactly b partners 1 Then, the definition of preference list is extended to allow unacceptable partners. Each node v has a preference list of k neighbors (0 ≤ k ≤ n) in preference order. A node u is acceptable for v iff u is in v's preference list, i.e., u ∈ v.pref . A node prefers to stay single rather than to be matched to an unacceptable partner.

The definition of (extended) stable marriage/matching still relies on the absence of BP, whose definition must be extended too.

I -Subsets of unequal Size, b = 1

In this variant, sets of women and men can be of different cardinality. Furthermore, the nodes' capacity is 1. As a consequence, some nodes can be single in the final matching. Adaptation of the Two Phase Algorithm. This is the simplest variant, since there is nothing to change in the basic algorithm. Indeed, if a woman detects no BP and reaches the end of her preference list without finding any match, she is single and no more enabled. Symmetrically, if a man does not receive any proposal, he stays single and not enabled. The time complexity analysis for this extension stays relevant, but depends on the size of the largest subset.

Null, i.e., v is single, priority(v,u) = n + 1).2 This simple adaptation ensures that, for a node v, an unacceptable node u always has the lowest possible priority (even comparing to being single). Thus, u will never be a part of the C v set (set of mutually preferred neighbors of v), used in other predicates of the basic algorithm. Notice that the values of the priority function p are used in C v (Sect. II). This implies that u will be excluded from any action contributing to the creation of matchings, in all the rules of type Propose, women's Confirm and Accept. Note that Confirm for men does not contribute to the creation of a matching, since a man eligible for this rule is already considered as married (m.proposal.marriage = m). Hence, new unacceptable matchings (involving an unacceptable partner) cannot be created. Thus the proof of the basic solution stays relevant, if no unacceptable matching exists due to a "bad" initialization. Notice that the original proof does not make any assumption on the size of the preference list. Moreover, the part of the proof asserting that a terminal configuration with a stable marriage is reached is still valid if some nodes end single.

But what if some unacceptable matchings exist at initialization? They have to be reset using Reset. To ensure that the actions of these rules are launched, the incoherent pointers' predicates (constituting the guards of Reset rules) has to be adapted. This is for detecting whether the pointers of a node v, v.marriage and v.proposal (used to indicate and create matchings) point to unacceptable partners. Thus, both predicates IncoherentPointersW(v) and IncoherentPointersM(v) are modified, each in the same way, by adding the following disjunction: priority(v,v.marriage) = n + 2 ∨ priority(v,v.proposal) = n + 2.

Due to this modification and by the correctness of the original algorithm, in at least O(n 4 ) moves, every node is activated. Thus, all incoherent pointers are reset and never become incoherent again (in the way defined above), as it is explained in the previous paragraphs. Then, a stable matching is reached in at most additional O(n 4 ) moves.

Adaptation of CompAlg.

As for the Ackermann et al. based algorithm, the priority function (see Chapter 5, Section II) must be adapted in the same way to handle unacceptable partners. Hence, for a node u ∈N (v), priority(v,u) = n + 2 iff u / ∈ v.pref (recall that if u = v.marriage_pref = Null, i.e., v is single, priority(v,u) = n + 1). This induces that single nodes prefer to stay single instead of being matched with an unacceptable node.

Note that Async-GSA cannot build a pair with unacceptable partners: a woman cannot propose to an unacceptable partner (he is not in her list) and a man cannot accept a proposition from an unacceptable woman (priority returns n + 2).

As for the first algorithm, there is still a problem if a pair with an unacceptable partner is already present in the initial configuration. The local predicate must detect it but it does not as it is, even with the new value of priority. Hence, we add the following local predicate in a conjunction with the original LP m,w (as defined in Section III.2).

P U nacceptable m,w

≡ ¬[(priority(w,m) = n + 2 ∧ request w,m = None) can appear. For example, let v and u be two members of different sets. Two instances of v can be or can become matched with two instances of u. If the instances of v are the most preferred for u, then no BP will ever appear and change the situation, leaving two same nodes matched twice together.

To avoid this situation, an instance v[i] of v should be prevented to propose to and become matched with a neighboring instance u[k] already matched or having a proposal from another instance v[j] of the same node v. For that, each instance of v computes the set of such "occupied" neighboring instances, denoted Occupied, and excludes them from the set of mutually preferred instances C (see Chapter 4, Section II), at every activation. This implies that the set of instances Occupied v[this] will be excluded from C v[this] at any activation of v[this], and thus from any action contributing to creation of matchings, in all the rules of type Propose, Confirm and Accept (as is necessary by the explanation above).

This modification ensures that no new "double" matchings between the same two nodes are created. However, similarly to the solution for the variant with unacceptable partners, such "double" matchings, existing at initialization, have to be deleted (using Reset). Here again, this can be done by adapting IncoherentPointersW(v[this]) and IncoherentPointersM (v[this]). We present this adaptation together with the adaptation needed to tolerate unacceptable partners (so that the result works for all the considered variants). Each of the two predicates are modified in the same way, by adding the following disjunction: Due to this modification and by the correctness of the original algorithm, in at least O(N 4 ) moves, every node is activated, where N is the overall number of the instances. Thus, all incoherent pointers are reset (by Reset) and never become incoherent again (in the way defined above). Then, a stable matching is reached in at most additional O(N 4 ) moves.

Adaptation of CompAlg.

As for the first algorithm, we apply the transformation described in the previous section to both sides. Hence, each occurrence of v in the preference list of a member on the opposite side is replaced by the sequence v[1], v[2] . . . , v[b] of instances. Then, at each activation of a member v with capacity b, b similar instances of the algorithm are executed one after the other.

The same problem also appears with this algorithm: two instances of a node v may be matched to two different instances of the same node u. Hence, Async-GSA must be modified for avoiding such double matches in the same way. For that, each instance of v computes the set of "occupied" neighboring instances (already matched with v), denoted Occupied, and excludes them from consideration in the preference list pref and Hence, the set of instances Occupied v[this] will be excluded from pref and from N (v) at any activation of v[this] for Async-GSA, and thus from any action contributing to creation of matchings in particular since next(pref ) cannot anymore return these instances. But, as explained before, this "double matchings" may be already build at initialization and the local predicate must detect it. Thus, we add the following local predicate in a conjunction with the original LP m,w (as defined in Section III.2). We include the modification for unacceptable partners to give a global solution for all the variants treated till now. Note that similarly to this predicate, all other local predicates has to be modified using similar notations to manage the different instances. Since Async-GSA cannot fall in such a problematic case defined by P Extensions m[i],w[j] , it remains locally checkable and thus can be composed into CompAlg. Furthermore, the analysis complexity is now depend on the total number N of instances but stays of the same order (since b is constant).

I -Summary

During the design of asynchronous self-stabilizing distributed algorithms solving SMP, we faced different issues. The first is asynchrony, in relation with our goal of efficiency concerning the proposed algorithms. The second issue is the requirement of privacy for the participant's information, leading to keep their preference lists secret. The third issue is the assumption of a strong adversary, under the form of an unfair demon, still in relation with the best possible performances. Nevertheless, we proposed two self-stabilizing distributed algorithms that solves SMP in an asynchronous communication model with an unfair daemon and respecting the privacy (only some binary queries and responses about the preference lists are transmitted).

Based on the Ackermann et al.'s idea (of two phases), we proposed a first algorithm (Chapter 4) that solves SMP in O(n 4 ) moves and rounds in the state reading model. The two phases mechanism uses local detection and correction of BPs. Hence, when a partial stable marriage is already obtained, the algorithm may keep the matched pairs. This can be a huge advantage in the case of a distributed storage of the matching, when only some sites have been hit by failures. But the counterpart is a rather high worst case complexity. This work has been published in [LMB + 17] and is submitted to a journal.

Since the worst case complexity was far from the theoretical lower bound of Ω(n 2 / log n) moves, our next step was to look for an algorithm with a better complexity. As local correction appeared to be costly (due to our first solution) costly, we tried to implement a global correction, by triggering a reset each time a problem was detected locally. For that, we had to modify the original local detection conditions of [APSVD94], while still using the same global reset scheme. The resulting algorithm (Chapter 5) solves SMP in Θ(n 2 ) moves and rounds in the link register model. A preliminary version of this work has been published in [BBB + 18]. The full version is in preparation for submission.

Finally, we studied in Chapter 6 some classical variants of SMP and propose the minor changes to both algorithms to obtain a self-stabilizing algorithm that solves all these variants.

II -Perspectives

We now discuss some perspectives related to the results of the thesis.

Complexity. In [START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF], it has been proven that the communication complexity of SMP is Ω(n 2 ) bits inducing a lower bound of Ω(n 2 / log n) moves in our model (see Section III.1 for explanations). In this work, the best algorithm (CompAlg) has a complexity of Θ(n 2 ) moves, letting a gap open between the best know solution and the lower bound. A natural issue is to close the gap. That can be done either by finding a still more efficient algorithm in terms of moves or by increasing the lower bound.

In [START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF] the lower bound proof uses a particular case of preference lists that can be represented using only O(n 2 ) bits altogether. However in a general case, the preference lists require Θ(n 2 log n) bits to be represented in the two-party setting assumed in the communication complexity analysis (the preference list of each SMP participant is coded by Θ(n log n) bits). We believe it is possible to provide a proof for a more general case of preferences represented by Ω(n 2 log n) bits, resulting in Ω(n 2 ) lower bound of moves in our model. Nevertheless, this is still an open question.

Reset Algorithm. Numerous reset algorithms were known before this work, but no one was precisely designed for the link register model with an unfair scheduler. The reset algorithm that we proposed is adapted to this model and has a move complexity of O(n • 6 p ) (where p is the depth of the rooted spanning tree on which it runs). Hence, if the depth of the tree is known and does not depend on any system parameter (like our tree of depth 2), it has a linear complexity. Otherwise, the complexity is exponential. Natural issues are the questions of the tightness of this bound and the possibility of a better solution. For the tightness of our algorithm's bound, we conjecture that it cannot be improved by other analysis techniques. The reason for the latter is the following.

There are possible cycles of moves that a children of a node in a tree can make from any configuration. These cycles are due to faults that may cause a node to change for initiate status several times, before its parent makes a move, leading to the exponential move complexity. These cycles are not broken until the initiate wave comes to the root and a f reeze wave is launched. Hence, in order to get a better algorithm, an idea would be to avoid such cycles by using more restricted guards.

Self-stabilizing Transformer. In Chapter 5, we have presented the result of the composition of TreeAlg, ResetAlg and Async-GSA as a whole algorithm. As TreeAlg and ResetAlg are largely independent of Async-GSA, one can ask whether such a composition is applicable to other algorithms than Async-GSA. Underlying this approach, there can be proven a general composition theorem, stating that if an initialized algorithm satisfies some properties, related to local checkability, and solves a graph problem Prob, then it can be automatically (syntactically) transformed into a self-stabilizing version (self-stabilizing for Prob). Such a composition theorem would establish the existence of what can be called a self-stabilizing transformer, transforming automatically an algorithm with initialization into a self-stabilizing algorithm solving the same problem. There already exist several such transformers in the literature ([APSV91, APSVD94],

Aknowledgement

Writing a thesis is a tough process. This is why I would like to thank all those who have helped me in one way or another in this task. Even more so in this complicated context of the pandemic, each support has been precious. First and foremost, I would like to thank my supervisors, Joffroy Beauquier, Janna Burman and Thibault Bernard, for their unfailing support and their unvaluable advices during these years. They guided my with patience and taught me the methodology of many things, from writing research papers, to presenting my ideas and results. Thanks to them, I learned to always aim better, without being satisfied with what has already been achieved. I will try in the future to apply their teachings and to produce quality research.

I would like to express my gratitude to Colette Johnen and Volker Tureau for reviewing my manuscript and for their relevant and insightful reviews. I am also thankful to the others members of my thesis committee, Johanne Cohen, Hugues Fauconnier and Sébastien Tixeuil, for attending my defense. I would also like to thank Johanne Cohen, Laurence Pilard and George Manoussakis, the co-authors of my first paper, for our discussions about the stable marriage and the work we produced. I am extremely grateful towards Shay Kutten for hosting me twice at the Technion during my thesis and for our inspiring discussions. At the beginning of my Master, I wasn't sure what I wanted to do. Thus, I am very thankful to Hervé Bredin and Claude Barras for welcoming me at the LIMSI and for introducing me to research during my first internship. Also, I would like to thank my family and especially my parents for their unfailing support and their faith in me and my aunt and uncle in particular for their logistical support. I want to express a special thank to Fabien Dufoulon with whom I shared our advisors but also an office and a coffee machine. We spent (and we still spend) a lot of great time, from lively political debates to precise technical discussions, from incredible games to quiet evenings. I want to thank Chuan for taking part of these times and for putting up with our endless debates. Furthermore, I would like to thank my colleagues (and friends) Amal, Aygul, Antoine, Ian, Yushan, Oguz, Laercio, Timothée, David, Pierre, George and Hay and also my friends "from outside", Marie B., Hélène, Simon, Lucille, Ye, Margaux, Yohann and Marie S.. Finally, I would also like to thank all the colleagues of the LRI and especially the administration team as well the technical support team, for their availability, their kindness and their help. Le point de départ du deuxième algorithme est le schéma de détection locale/correction globale de Awerbuch et al. (DA' 1994). Malheureusement, la dénition de la vériabilité locale de DA' 1994 ne s'applique pas à notre cas (en particulier en raison du démon inéquitable). Nous proposons donc une nouvelle définition. De plus, nous concevons un algorithme de réinitialisation (reset) asynchrone, distribué et autostabilisant. L'algorithme résultant résout le SMP en Θ(n 2 ) moves. plexity, Unfair Daemon, Privacy Abstract: The Stable Marriage Problem (SMP) is a matching problem where participants have preferences over their potential partners. The objective is to nd a matching that is optimal (stable in certain sens) with regard to these preferences. This type of matching has a lot of widely used applications such as the assignment of children to schools, interns to hospitals, kidney transplant patients to donors, as well as taxi scheduling or content delivery on the Internet. Some applications can be solved in a centralized way while others, due to their distributed nature and their complex data, need a dierent treatment.

In order to handle this challenge, we provide two distributed self-stabilizing solutions (i.e., that tolerate transient (or short-lived) failures (e.g., memory or message corruptions) of any nodes). The privacy of the preference lists is guaranteed by the two proposed algorithms: lists are not shared, only some binary queries and responses are transmitted. For both algorithms, executions proceed in atomic steps and a daemon (distributed unfair daemon) conveys the notion of asynchrony. Under this daemon, the stabilization time can be bounded in term of moves (local computations). This complexity metrics allows to evaluate the necessary computational power or the energy consumption of the algorithm's executions.

The rst algorithm, based on the centralized method of Ackermann et al. (SICOMP' 2011), solves the problem in O(n 4 ) moves.

The starting point of the second algorithm is the local detection/global correction scheme of Awerbuch et al. (DA' 1994). Unfortunately, local checkability denition of DA '1994 does not apply to our case (in particular due to the unfair daemon). Consequently, we propose a new denition. Furthermore, we design a distributed self-stabilizing asynchronous reset algorithm. Using it, the resulting composed algorithm solves SMP in Θ(n 2 ) moves in a self-stabilizing way.

  . . . . . . . . . . . . . . . . . . . . . . . 8 II.1 Synchronous Model . . . . . . . . . . . . . . . . . . . . . . . . . . 8 II.2 Asynchronous Model . . . . . . . . . . . . . . . . . . . . . . . . . 9 III Self-stabilizing Solutions . . . . . . . . . . . . . . . . . . . . . 9 III.1 On the Way to Self-stabilizing Stable Marriage Algorithms . . . . 10 III.2 Transformer to Self-stabilizing Solutions . . . . . . . . . . . . . . 10

18 VII

 18 . . . . . . . . . . . . . . . . . . . . . . 15 III.1 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 III.2 Configurations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 IV Execution of Distributed Algorithms . . . . . . . . . . . . . . 16 IV.1 Scheduler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 IV.2 Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 V Communication Models . . . . . . . . . . . . . . . . . . . . . . 17 VI Self-stabilization . . . . . . . . . . . . . . . . . . . . . . . . . . Time Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . 19

Figure 3 . 1 :

 31 Figure 3.1: Distributed bipartite system with the unstable marriage M 1

Figure 3 . 2 :

 32 Figure 3.2: The register model

  stabilizing Solution to SMP . . . . . . . . . . . . . . . . . 25 II.1 Algorithm Implementation . . . . . . . . . . . . . . . . . . . . . . 28 II.1.1 Variables, Constants, Functions and Predicates . . . . . . 28 II.1.2 Algorithm. . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 III Correctness Proof and Time Complexity Analysis . . . . . 34 III.1 Sketch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 III.2 Detailed Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 III.2.1 Properties of the Terminal Configurations . . . . . . . . . 36 III.2.2 Convergence Proof . . . . . . . . . . . . . . . . . . . . . . 40 IV Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

Figure 4 . 1 :

 41 Figure 4.1: Knuth's cycle: first resolution

Figure 4 . 3 :

 43 Figure 4.3: Knuth's cycle: third resolution

  .5.b) with a new BP: (Anna, Scott).

Figure 4 . 5 :

 45 Figure 4.5: First phase of the Ackermann et al.'s algorithm

Figure 4 . 6 :

 46 Figure 4.6: Configuration after the first phase

  Figure 4.7.b).

Figure 4 . 7 :Figure 4 . 8 :

 4748 Figure 4.7: Second phase of the Ackermann et al.'s algorithm

Figure 4 . 9 :

 49 Figure 4.9: Phase transitions in the proposed distributed self-stabilizing version

1:

  Reset : (* Reset pointers of marriage and proposal *) ← Null, w.proposal ← Null 4: BadInit : (* Reset the pointer of proposal *) 5: {¬IncoherentPointersW(w) ∧ w.marriage = Null 6: ∧ w.proposal = Null ∧ ∀ v ∈ N (w) ∪ {w} : v.phase = 2} 7: w.proposal ← Null, w.phase ← 1 8: Propose1 : (* Propose in phase 1 *) 9: {¬IncoherentPointersW(w) ∧ ∀ v ∈ N (w) ∪ {w} : v.phase = 1 10: ∧ BestMarriage(w) = w.proposal ∧ Married(w)} 11: w.proposal ← BestMarriage(w) 12: Confirm1 : (* Confirm a proposal in phase 1 *) 13: {¬IncoherentPointersW(w) ∧ ∀ v ∈ N (w) ∪ {w} : v.phase = 1 14: ∧ Response(w) ∧ Married(w) ∧ BestMarriage(w) = w.proposal} 15: w.marriage ← w.proposal, w.proposal ← Null 16: Propose2 : (* Propose in phase 2*) 17: {¬IncoherentPointersW(w) ∧ ∀ v ∈ N (w) ∪ {w} : v.phase = 2 18: ∧ BestMarriage(w) = w.proposal ∧ w.marriage = Null} 19: w.proposal ← BestMarriage(w) 20: Confirm2 : (* Confirm a proposal in phase 2 *) 21: {¬IncoherentPointersW(w) ∧ ∀ v ∈N (w) ∪ {w} : v.phase = 2 22: ∧ Response(w) ∧ w.marriage = Null 23: ∧ BestMarriage(w) = w.proposal} 24: w.marriage ← w.proposal, w.proposal ← Null 25: ToPhase1.5 : (* To phase 1.5 *) 26: {¬IncoherentPointersW(w) ∧ ∀ v ∈ N (w) ∪ {w} : v.phase = 1 27: ∧ ¬BlockingPairW(w)} 28: w.phase ← 1.5, w.proposal ← Null 29: ToPhase2 : (* To phase 2 *) 30: {¬IncoherentPointersW(w) ∧ ∀ v ∈N (w) ∪ {w} : v.phase = 1.5 31: ∧ ¬BlockingPairW(w)} 32: w.phase ← 2, w.proposal ← Null 33: ToPhase1 : (* To phase 1 *) ∈ N (w): (m.phase = 1 ∧ w.phase = 2) 36: ∨ (m.phase = 2 ∧ w.phase = 1.5)] phase ∈ {2, 1.5} ∧ BlockingPairW(w)} 39:

1:∧

  Reset : (* Reset pointer of marriage *) ← Null, m.phase ← 1 4: Accept : (* Accept a proposal except in phase 1.5 *) BestProposal(m) = Null ∧ ¬AlreadyEngaged(m)} 7: m.proposal ← BestProposal(m) 8: Confirm : (* Confirm a marriage *) 9: {¬IncoherentPointersM(m) ∧ m.proposal = Null 10: ∧ m.proposal.marriage = m ∧ AllCoherentPhase(m) 11: ∧ priority(m,m.proposal) < priority(m,m.marriage)} 12: m.marriage ← m.proposal, m.proposal ← Null 13: ToPhase1.5 : (* To phase 1.5 *) 14: {¬IncoherentPointersM(m) ∧ ∀ w ∈ N (m): w.phase = 1.5 15: ∧ m.phase = 1 ∧ ¬BlockingPairM(m)} 16: m.phase ← 1.5, m.proposal ← Null 17: ToPhase2 : (* To phase 2 *) 18: {¬IncoherentPointersM(m) ∧ ∀ w ∈N (m): w.phase = 2 19: ∧ m.phase = 1.5 ∧ ¬BlockingPairM(m)} 20: m.phase ← 2, m.proposal ← Null 21: ToPhase1 : (* To phase 1 *) w ∈N (m): w.phase ∈ {1.5, 1}) ∧ m.phase = 2] w ∈N (m): w.phase = 1) ∧ m.phase = 1.5]) } 26: m.phase ← 1, m.proposal ← Null

Finally,

  Proposition 1, 2 and 3 altogether imply the main theorem below. Theorem 1. Any execution takes O(n 4 ) moves to reach a terminal configuration where the set of edges {(w, m) ∈ E : w.marriage = m ∧ m.marriage = w} is a stable matching.

, {2}, 0 )Lemma 7 .

 07 Let C be a configuration in C 1M where ∀w ∈Women: w.phase = 2. Any execution starting from C reaches a configuration C' in C 1W in O(n) moves. Proof. In C, a woman w in phase 2, (a) either is eligible for Reset if IncoherentPointersW(w) = True (this rule does not change the phase number).

( a )

 a If all men in phase 1.5 are activated for Reset (at most n -1), the reached configuration is in ({1}, {2}, X) A. and then, in C 1W (see the point A. for explanations) after O(n) moves. (b) If all men in phase 1.5 are activated for ToPhase2 or Reset, the reached configuration is in ({1, 2}, {2}, X) and then in C 1W (see point B. for explanations) after O(n) moves.

( a )

 a If all men in phase 1.5 and 2 are activated for Reset (at most n -2), the reached configuration is in ({1}, {2}, X) A. and then, in C 1W (see the point A. for explanations) after O(n) moves. (b) If all men in phase 1.5 are activated for ToPhase2 or Reset, the reached configuration is in ({1, 2}, {2}, X) and then in C 1W (see point B. for explanations) after O(n) moves. (c) If all men in phase 2 are activated for Reset, the reached configuration is in ({1, 1.5}, {2}, X) and then in C 1W (see point C. for explanations) after O(n) moves. (d) at most n men are activated (for ToPhase2 or Reset) but also at most n women for ToPhase1, the reached configuration is in C 1W after at most O(n) moves. To sum up, from any configuration C ∈ C 1 where ∀ w ∈ Women : w.phase = 2, any execution takes O(n) moves to reach a configuration in ∈ C 1W . Lemma 8. Let C be a configuration in C 1 where ∀w ∈Women : w.phase ∈ {2, 1.5}. Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W .

( a )

 a Either at most n -1 men in phase 2 are activated for ToPhase1 or Reset, that is O(n) moves, and the reached configuration is in ({1}, {1.5, 2}, X). By point A., after O(n) moves, a configuration in C 1W is reached. (b) Or at most n -1 men in phase 2 (for ToPhase1 or Reset) and at most n women are activated (for ToPhase1), that is O(n) moves, and the reached configuration is in C 1W . D. ({1, 1.5, 2}, {1.5, 2}, X ≥ 0): after at most 2n -1 Reset (all men except one in phase 2 and n women), there are four cases. (a) All men in phase 2 and 1.5 (at most n-1) are activated for ToPhase1 or Reset, that is O(n) moves, and the reached configuration is in ({1}, {1.5, 2}, X). By point A., after O(n) moves, a configuration in C 1W is reached. (b) All men in phase 2 (at most n -2) are activated for ToPhase1 or Reset, that is O(n) moves, and the reached configuration is in ({1, 1.5}, {1.5, 2}, X). By point B., after O(n) moves, a configuration in C 1W is reached. (c) All men in phase 1.5 (at most n -2) are activated for Reset, that is O(n) moves, and the reached configuration is in ({1, 2}, {1.5, 2}, X). By point C., after O(n) moves, a configuration in C 1W is reached. (d) At most n men (for ToPhase1 or Reset) and at most n women are activated (for ToPhase1), that is O(n) moves, and the reached configuration is in C 1W . To sum up, from any configuration C ∈ C 1 where ∀w ∈Women : w.phase ∈ {2, 1.5}, any execution takes O(n) moves to reach a configuration in ∈ C 1W . Lemma 9. Let C be a configuration in C 1 where ∀w ∈Women : w.phase = 1.5. Any execution starting from C takes O(n) moves to reach a configuration C' in C 1W or ({1.5}, {1.5}, X) with X ≥ 0.

Lemma 13 .

 13 Let C and C' be configurations in ({1}, {1, 1.5}, X) × ({1, 1.5}, {1.5}, X) × such that C * → C'. Let w be a woman. If w.marriage(C) = w.marriage(C') then priority(w,w.marriage(C)) > priority(w,w.marriage(C')) or w.marriage(C') = Null. Thereby, R w (C) > R w (C'). Furthermore, w cannot be married again with w.marriage(C) before being activated for ToPhase2. Proof. Let w be in Women and m be in Men. Since women are in phase 1, if w.marriage(C) = w.marriage(C'), there are two cases: 1. w.marriage(C) = m and w.marriage(C') = Null or 2. w.marriage(C) = m and w.marriage(C') = m 1 .

Lemma 18 .

 18 In a configuration C in ({1.5}, {2}, 0) {1.5, 2}, {2}, 0), women are only enabled for Reset and men are enabled for rules in {ToPhase2, Reset, Accept, Confirm}. Furthermore if C → C', then the configuration C' is:• in ({1.5}, {2}, 0) {1.5, 2}, {2}, 0) if only Accept (men), Confirm (men) and Reset (women) are activated in the transition.

Lemma 27 .

 27 Let C be a configuration in ({1.5}, {1.5}, 0), such that in C no man is eligible for Reset and ∀w ∈Women: w.marriage.marriage = w ⇒ w.marriage = w.proposal. Every segment of execution starting from C reaches a configuration C' in C 2 . Proof. From C, by Lemma 19, a configuration C 2 in ({2}, {2}, 0) or in C 1 (after the first man's Reset) is reached.

  1. in C, m.marriage = Null or m.marriage = Null and both m.marriage.marriage = m and m.marriage = m.proposal and 2. in C 1 , m.marriage = Null and either m.marriage.marriage = m or m.marriage = m.proposal. Consequently, there are several cases. Let w be a woman. Let T be the transition that reaches C 1 from a configuration C 0 where: 1. m.marriage = Null. Thus, in T, one of the following actions is made: (a) m.marriage ← w with w.marriage = m or, (b) m.marriage ← w and m.proposal ← w or, (c) m.marriage ← m.proposal with m.proposal = Null after the transition; 2. m.marriage = Null and m.marriage.marriage = m. Thus, in T, one of the following actions is made: (a) m.marriage.marriage ← Null or, (b) m.marriage.marriage ← m 1 or, (c) m.proposal ← m.marriage.

  Convergence to a Terminal Configuration Lemma 30. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Assume that in some transition D 0 → D 1 in E a woman w executes a rule. 1. The activated rule belongs to {Reset, Propose2, Confirm2}; 2. ¬Married(w) holds in D 0 ; 3. If w.marriage = Null in D 0 , then the activated rule is either Propose2 or Confirm2; 4. If w.marriage = Null, then the activated rule is Reset.

  Accept or Confirm. 2. If AlreadyEngaged(m) holds in D 0 , then the activated rule is Confirm. Proof. Assume that m executes a rule in D 0 → D 1 . By definition of E, m does not execute ToPhase1, ToPhase1.5, ToPhase2 and Reset during D 0 → D 1 . Assume that AlreadyEngaged(m) holds in D 0 . According to the Accept guard, m cannot execute Accept in D 0 → D 1 .

(a) m 2 =

 2 Null. Then we have: m 1 = Null and m 1 ∈ C w in D 1 . Moreover, since m 2 = BestMarriage(w) in F 0 then m 1 ∈ C w in F 0 . Thus, according to Lemma 34,m 1 executes Confirm in D 1 * → F 0 . (b) m 2 ∈ C w in D 1 . Thus priority(w,m 1 ) < priority(w,m 2 ) and so m 1 = Null. Since m 2 = BestMarriage(w) in F 0 then m 1 / ∈ C w in F 0 while m 1 ∈ C w in D 1 . Thus according to Lemma 34, m 1 executes Confirm in D 1 * → F 0 . (c) m 2 = Null and m 2 ∈ C w in D 1 . Since m 2 = BestMarriage(w) in F 0 then m 2 ∈ C w in F 0 . Thus according to Lemma 34, m 2 executes Confirm in D 1 * → F 0 .Lemma 36. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Let w be in Women.Let C 0 → C 1 , C 2 → C 3 , C 4 → C 5 bethree transitions corresponding to three consecutive rules executed by w. Then w executes Propose2 once between C 0 and C 5 . Proof. Using Lemma 30, w can only execute Propose2, Reset, and Confirm2 in these three transitions. Assume first that in C 0 → C 1 , w executes Confirm2. Then, in C 1 , there exists a man m such that w.marriage(C 1 ) = m. Since w does not execute any rule between C 1 and C 2 , then in C 2 , we have w.marriage(C 2 ) = m. Using point four of Lemma 30, w executes Reset in C 2 → C 3 . Moreover, since in C 3 , w.marriage(C 3 ) = Null and w.proposal(C 3 ) = Null, Lemma 30 implies that w executes Propose2 in transition C 4 → C 5 .

1:

  Propose : (* Proposes to the man pointed by marriage_pref *) 2: {∃m ∈N (w): request w,m / ∈ {Proposal, Yes, No} Confirm : (* Confirms her proposal *) 7: {∃m ∈N (w): request w,m = Proposal 8: ∧ marriage_pref = m ∧ request m,w = Yes} 9: request w,m ← Yes 10: 11: Refusal_Management : (* Manages a refusal *) 12: {∃m ∈N (w): request w,m ∈ {Proposal, Yes} 13:

1:

  Accept : (* Accepts a proposal *) 2: {∃w ∈N (m): request w,m = Proposal 3: ∧ priority(m,w) < priority(m,marriage_pref )} Refuse : (* Refuses a proposal *) 8: {∃w ∈N (m): request w,m ∈ {Proposal, Yes} ∧ request m,w = No 9: ∧ priority(m,w) > priority(m,marriage_pref ) } 10: request m,w ← No Correctness and complexity. The correctness proof and the complexity analysis of Async-GSA are in Section III.2, in relation with the proof of condition 4 of local checkability.

  The complete local predicate checked by m is: LP m,w ≡ (P 0 m,w ∨ P

≡

  is a predicate related to a situation where m is activated for Refuse to refuse w's proposal (from a configuration where P P ropose m,w was True). The rule Refuse is enabled in two different kinds of configuration. First if w has a priority worse than marriage_pref m , then it sets request m,w to No. Second, from a configuration satisfying P Conf irm m,w , if m is activated for Refuse after having accepted. Refuse is enabled if w has a worse priority than marriage_pref m . It sets request m,w to No. This case is possible if, after having accepted the proposal of w, another better ranked woman proposes to m. request w,m ∈ {Proposal, Yes} ∧ request m,w = No ∧ marriage_pref w = m ∧ priority(m,w) > priority(m,marriage_pref m ) Recall that, w shares only the result of priority(w,m) < priority(w,marriage_pref w ) to the man m using a bit. P R_M m,w is satisfied when w is activated for Re-fusal_Management in a configuration in which P Ref use m,w

  Async-GSA's Local Checkability. Now we prove the local checkability of Async-GSA for Π = ∀(m,w)∈E ∧ m∈Men ∧ w∈Women LP m,w .First, we consider the condition 3 of stability in Def. 6. The property that P 0 m,w ,

Lemma 43 .are

 43 A terminal configuration of Async-GSA satisfying Π, satisfies the algorithm predicate PredAsync-GSA.Proof. Let C be a terminal configuration satisfying Π. In C, for all edges (m, w), False (otherwise a rule would be enabled but C is terminal). Thus, since Π is satisfied, ∀(m, w) ∈ E : (P Conf irm m,w ∨ P R_M m,w ∨ P 0 m,w ) ∧ ¬P BP m,w is necessarily True.

Figure 5 . 5 :

 55 Figure 5.5: System before running Async-GSA

Figure 5 . 6 :

 56 Figure 5.6: First two rounds of Async-GSA

  Update : (* Updates min v,u *) 10: {∃u ∈N (v): min v,u = (min(pref ) = u)} 11: ∀u ∈N (v): min v,u ← (min(pref ) = u)

  reset configuration is reached (if the initial reset signal was launched in C ResetAlg saf e

  Figure 5.10: A safe configuration (assuming that the configuration is consistent)

18 :

 18 Variables_Consistency : (* Checks local and shared variables' coherence *) 6: {(¬I_am_Root ∧ st v,parent = status) 7: ∨ (¬I_am_Leaf ∧ (∃u ∈children(v): st v,u = status))} Neighbors_Coherence : (* Checks the neighbors' status coherence *) 11: {status = reset ∧ ¬I_am_Leaf ∧ (∃u ∈children(v): st u,v = reset)} 12: update_variables(initiate) 13: 14: Initiate : (* Propagates the initiate wave to the root *) 15: {status = normal ∧ ¬I_am_Leaf ∧ (∃u ∈children(v): st u,v = initiate)} Freeze : (* Propagates the freeze wave *) 19:

  Reset : (* Resets the variables and propagates the reset wave *) 24: {status = f reeze ∧ [I_am_Leaf 25: ∨ (¬I_am_Leaf ∧ (∀u ∈children(v): st u,v = reset))]} Back_Normal : (* Returns to the normal status *) 30:

Figure 5 . 11 :

 511 Figure 5.11: Rules activations of a node depending on its status

Lemma 55 .

 55 Let C and C' two configurations from which the root r is activated for Reset. Let E be an execution such that C * → C'. Then in C', any node v but the root r satisfies status v = reset ∧ (∀u ∈ children(v): st v,u = reset) ∧ st v,parent = reset and in consequence, r is the only eligible node in C'. Proof. Since Reset is enabled at r in C and C', in both configurations we have (∀c ∈ children(r): st c,r = reset ∧ st r,c = f reeze) ∧ status r = f reeze.

Figure 5 . 12 :

 512 Figure 5.12: Illustration of the execution of ResetAlg in Lemma 55 and Corollary 7

Figure 5 . 13 :

 513 Figure 5.13: Possible sequence of rule's activations

BasicAlg (Condition 3 of Def. 7 )

 7 In this section, we focus on the reset property of ResetAlg as defined in the reset specification (Definition 7):(Reset)Starting from any configuration in C ResetAlg saf e , if a finite number of signals and at least one are launched, C BasicAlg reset is reached.

Lemma 59 .

 59 From any configuration C ∈ C ResetAlg saf e , if at least one reset signal is generated, then C BasicAlg reset is necessarily reached after O(n) moves. Proof. Let v be a node receiving a reset signal and C 1 be the configuration reached from C. In C 1 , v is necessarily a normal-node and others nodes are normal-or reset-nodes distributed on the tree as in a configuration in C ResetAlg saf e . But notice that C 1 is not in C ResetAlg saf e since v has signal set to True. Furthermore, in C 1 nodes are consistent (by Lemma 48, since they are consistent in C).

Figure 5 . 14 :

 514 Figure 5.14: Illustration of the execution of ResetAlg in Lemma 59

Figure 5 . 15 :

 515 Figure 5.15: Illustration of the execution of CompAlg Nodes are of type (1) during the red execution segments, and of type (2)during the blue ones.

  saf e in O(n) moves from any configuration (with stabilized tree of depth 2). This induces that Reset is executed a constant number of time: Async-GSA do not start again and again because of the reset of its variables. Thus after O(n 2 ) moves from C T , C ResetAlg saf e is reached. The sub-part ii) begins from C ResetAlg saf e

  BasicAlg reset and Async-GSA can be executed again. Finally, consider the sub-part iii), Lemma 44 gives the O(n 2 ) moves upper bound in terms of moves from C BasicAlg reset . Furthermore, since Async-GSA est locally checkable, no reset signal can be launched from C BasicAlg reset . Thus, ResetAlg converges to C ResetAlg normal in O(n) moves.Then, from C T , after O(n 2 ) moves, a configuration C M (in which PredAsync-GSA is satisfied) is reached (Lemma 68).

  Size . . . . . . . . . . . . . . . . . . . . . . 120 II Stable Matching with Indifference . . . . . . . . . . . . . . . 121 III Unacceptable Partners . . . . . . . . . . . . . . . . . . . . . . 122 IV Many-to-One (Hospitals-to-Residents Problem) . . . . . . . 124 V Many-to-Many . . . . . . . . . . . . . . . . . . . . . . . . . . . 125

Definition 10 (

 10 Blocking Pair (BP)). Given an extended matching M, a pair (w, m) is a blocking pair iff the following conditions are satisfied: 1. w and m are not matched together, i.e. (w, m) / ∈ M; 2. w and m are acceptable for each other; 3. w is not b-matched ∨ w prefers m to at least one of her b partners, i.e. ∃ m : (w, m ) ∈ M ∧ priority(w,m) < priority(w,m ); 4. m is not b-matched ∨ m prefers w to at least one of his b partners, i.e. ∃ w : (w , m) ∈ M ∧ priority(m,w) < priority(m,w ).

Figure 6 . 1 :

 61 Figure 6.1: Stable marriage in a system with subsets of unequal size

  Let us denote the currently considered instance of v by v[this]. Then,Occupied v[this] = {u[k] ∈N (v[this]) | ∃j = this, ∃i : (v[j].marriage = u[i] ∨ v[j].proposal = u[i])}.

[

  priority(v[this],v[this].marriage) = n + 2 ∨ priority(v[this],v[this].proposal) = n + 2] ∨ [∃i = this : (v[this].marriage = x[j] ∧ v[this].proposal = y[k] ∧ v[i].marriage = z[l] ∧ v[i].proposal = w[m]) ∧ {x, y} ∪ {z, w} {Null}].

  from N (v) (see Chapter 5, Section III), at every activation. Let us denote the currently considered instance of v by v[this] and b u be the capacity of b. Then,Occupied v[this] = {u[k] ∈N (v[this]) | ∃j = this, ∃i : v[j].marriage_pref = u[i]}.

P

  Extensions m[i],w[j] ≡ ¬[(priority(w[j],m[i]) = n + 2 ∧ request w[j],m[i] = None) ∨ (priority(m[i],w[j]) = n + 2 ∧ request m[i],w[j] / ∈ {None, No}) ∨ (∃k = i : m[i].marriage_pref = x[j] ∧ m[k].marriage_pref = z[l] ∧ x = z)]

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 II Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130

Titre:

  Mariage Stable Asynchrone et Auto-stabilisant Mots clés : Algorithmes Distribués, Modèles Asynchrones, Auto-stabilisation, Mariage Stable, Complexité en Moves, Démon inéquitable, Condentialité Résumé : Le Problème du Mariage Stable (SMP) est un problème d'appariement où les participants ont des préférences à propos de leurs partenaires potentiels. L'objectif est de trouver un appariement optimal (stable dans un sens) au regard des préférences. Ce type d'appariement a de très nombreuses applications comme les aectations d'étudiants à des universités (APB ou ParcourSup), celles des internes en médecine aux hôpitaux, les choix des donneurs pour les patients en attente d'organe, la mise en rapport des taxis et de leurs clients ou encore la diusion de contenu sur Internet. Certaines de ces applications peuvent être traitées de manière centralisée tandis que d'autres, de par leur nature distribuée et la complexité de leurs données, nécessitent un traitement diérent. Dans ce contexte, nous proposons deux solutions distribuées auto-stabilisantes (i.e. qui tolèrent les défaillances transitoires (ou de courte durée) de n'importe quels noeuds). Pour ces deux algorithmes, les exécutions se déroulent par pas atomiques et un dé-mon (démon distribué inéquitable ) exprime la notion d'asynchronisme. Avec ce démon, le temps de stabilisation peut être borné en terme de moves (pas locaux). Cette mesure de complexité permet d'évaluer avec précision la puissance de calcul nécessaire ou l'énergie dissipée par les exécutions de l'algorithme. Le premier algorithme, basé sur la méthode centralisée de Ackermann et al. (SICOMP' 2011), résout le SMP en O(n 4 ) moves.

Contents 1 Introduction 2 Related Work I

  Centralized Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . II Distributed Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . II.1 Synchronous Model . . . . . . . . . . . . . . . . . . . . . . . . . . . II.2 Asynchronous Model . . . . . . . . . . . . . . . . . . . . . . . . . . III Self-stabilizing Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . III.1 On the Way to Self-stabilizing Stable Marriage Algorithms . . . . . III.2 Transformer to Self-stabilizing Solutions . . . . . . . . . . . . . . .

	Chapter 1

  Definition 3. A is self-stabilizing for Prob (or solves Prob in a self-stabilizing way) if and only if there exists a non-empty subset L of C of so called legitimate configurations, such that:

1. (Correctness) any execution in E starting from a configuration C in L satisfies

Prob,

2. (Convergence) any execution in E reaches a configuration in L.

  .1.b).

	{Scott, Mark, John}	Jane	John	{Arbitrary list}	{Scott, Mark, John}	Jane	John	{Arbitrary list}
	{Arbitrary list}	Anna	Scott	{Zoe, Jane, Anna}	{Arbitrary list}	Anna	Scott	{Zoe, Jane, Anna}
	{Mark,			{Jane,		{Mark,			{Jane,
	Scott, John}	Zoe	Mark	Zoe, Anna}		Scott, John}	Zoe	Mark	Zoe, Anna}
	(a) Initial configuration with a BP		(b) Configuration after solving the BP
		(Jane, M ark)					.

  Ackermann et al. [AGM + 11]. Both works present completely centralized strategies allowing to solve stable marriage starting from any given matching. The strategy proposed by Roth and Vande Vate stores and consults a global access set of previously resolved BPs and thus is inherently centralized. Differently, the strategy by Ackermann et al. [AGM +

	{Scott, Mark, John}	Jane	John	{Arbitrary list}	{Scott, Mark, John}	Jane	John	{Arbitrary list}
	{Arbitrary list}	Anna	Scott	{Zoe, Jane, Anna}	{Arbitrary list}	Anna	Scott	{Zoe, Jane, Anna}
	{Mark,			{Jane,		{Mark,			{Jane,
	Scott, John}	Zoe	Mark	Zoe, Anna}		Scott, John}	Zoe	Mark	Zoe, Anna}
	(a) Resulting configuration with an other BP:		(b) Configuration after solving the BP
		(Zoe, M ark)					.
		Figure 4.4: Knuth's cycle: fourth resolution
	Notice that the Figure 4.4.b is the same as the Figure 4.1.a, with the same BP and
	no improvement in the matchings. This example shows that a self-stabilizing solution
	cannot be simply obtained by repairing locally the blocking pairs created by transient
	failures.
	After this negative result, a step forward was taken by Roth and Vande Vate [RS90]
	and by

  • C 1 where ∀ w ∈ Women : w.phase ∈ {2, 1.5}. By lemma 8, a configuration in C 1W is reached after O(n) moves. Then after its move, no new marriage is done.

	Since these moves are possible only because of incoherent pointers and each woman
	has only two pointers, there are at most n moves (Accept or Confirm) resulting
	from their incoherent pointers.

• C 1 where ∀ w ∈ Women : w.phase = 1.5. By lemma 9, a configuration in C

1W

or in ({1.5}, {1.5}, X ≥ 0) is reached after O(n) moves.

To sum up, from a configuration in C 1 , after O(n) moves, a configuration in C 1W or ({1.5}, {1.5}, X ≥ 0) is reached. Lemma 11. Let C be a configuration in C 1W . Any execution starting from C takes O(n 2 ) moves to reach a configuration C' in ({1}, {1, 1.5}, X) × ({1.5}, {1.5}, 0). Proof. Let w 1 be the woman in phase 1 (because C ∈ C 1W ). Let us analyze the moves of other nodes. Let m be a node in Men. Independently of its phase number, m can be eligible for Reset. After the move, m.phase = 1. Otherwise, if: 1. m.phase = 2 or m.phase = 1.5, m is only eligible for ToPhase1 if he was not eligible for Reset: one of its neighbors is in phase 1. If a woman in phase 2 proposes/confirms to m, it cannot accept/confirm (AllCoherentPhase(m) is False). 2. m.phase = 1, m can be eligible for different rules. If m is eligible for Accept or Confirm, there are incoherent pointers. Indeed, if a woman w has been activated for Propose1/2 or Confirm1/2, all men are in phase 1. Furthermore, if m is eligible for Accept or Confirm, all women are in phase 1 or 1.5. Then, the configuration is already C'. Now, if m is eligible for Accept because a proposal of a woman w, the pointers of w are incoherent and all women are either in phase 1 or 1.5. But men are not all in phase 1. Then, w is not eligible for Confirm until no man is in phase 1, that is the configuration C'. No new marriage can be done before reaching C'. If m is eligible for Confirm to w, that means that m is already married with w. Then, a man is eligible for at most two rules (Reset or ToPhase1 and Accept or Confirm. That means that in altogether O(n) moves, men are all in phase 1. Let w be a node in Women. Reset is enabled for w. If • w.phase = 1.5, w is eligible for ToPhase1 if w is involved in a BP or if a man is in phase 2. • w.phase = 1, w is eligible for Propose, Confirm or ToPhase1.5 if w is not involved in a BP. • w.phase = 2, w is eligible for Propose or Confirm, BadInit (if no reset) if all men are in phase 2 and for ToPhase1 if a man is in phase 1 or if w is involved in a BP.

  , C 2 is in C 2 . Let C be a configuration in C 1W . Every segment of execution starting from C reaches a configuration D in C 2 .

	Lemma 28.

Proof. From C, by Lemmas 11, 14, 15 and 16, a configuration C 2 in ({1.5}, {1.5}, 0) is reached.

  . m ∈ C w in A 2 implies that priority(m,w) < priority(m,m.marriage(A 2 )). Furthermore, m ∈ C w in A 1 implies that priority(m,w) ≥ priority(m,m.marriage(A 1 )), since w does not change its marriage variable. So m changes its marriage value in A 1 * → A 2 . According to Lemma 31, it can only do that executing Confirm. Let w be in Women. Let E be a sub-execution such that in every configuration of E, all nodes are in phase 2. Between two consecutive executions of Propose2 by w, there exists a man m ∈ Men which executes Confirm.Proof. Let D 0 → D 1 and F 0 → F 1 be two transitions corresponding to two consecutive activations of Propose2 by w. Assume that m 2

	Lemma 35.

that priority(m,w) < priority(m,m.marriage(A 1 )). Furthermore, m ∈ C w in A 2 implies that priority(m,w) ≥ priority(m,m.marriage(A 2 )), since w does not change its marriage variable. So m changes its marriage value in A 1 * → A 2 . According to Lemma 31, it can only do that executing Confirm.

2

  Lemma 38. The predicate ¬P BP m,w is stable for Async-GSA. Proof. Assume that there is an edge (w, m) in C that does not satisfy P BP m,w . If m is activated for Accept, priority(m,w) < priority(m,marriage_pref m ) is True in C. But, since P BP m,w is not satisfied in C, we have priority(w,m) > priority(w,marriage_pref w ) in C and this is still True in C' (Accept does not change marriage_pref w ). Thus, P BP m,w is also False in C'. The rules Propose, Confirm and Refuse do not change the value of marriage_pref of w and m. Thus, in C', P BP m,w is still False. If w is activated for Refusal_Management, in C' marriage_pref w is shifted to the next element to the right. This rule is enabled only if request m,w = No. Thus, in the previous transition m has set her variable to No with the Refuse rule, i.e., priority(m,w) > priority(m,marriage_pref m ) is False in C and is still True in C'. Hence, P BP m,w is still False in C'.

	Corollary 2. LP m,w is stable.
	Proof. This corollary is the direct consequence of:
	1. the construction of P 0 m,w , P P ropose m,w	, P Accept m,w , P Conf irm m,w	, P Ref use m,w	and P	R_M m,w (related
	to the transitions of Async-GSA) and,
	2. the lemma 38 states that ¬P BP m,w is stable.
	Now, we prove the condition 4 of Definition 6.

Lemma 39. From any configuration, a woman w can only shift her pointer marriage_pref one by one to the right with the rule Refusal_Management.

  w 1 , wn, . . . , w 3 }

	m 2	{w 3 , w 2 , w 1 , wn, . . . , w 4 }
	m n-1	{wn, w n-1 , . . . , w 1 }
	mn	{w 1 , wn, . . . , w 2 }

  Theorem 3. From any configuration C, after O(n) moves, a terminal and legitimate configuration is reached. Proof. By Lemmas 45 and 46, each nodes is eligible at most once for each rule. Thus, after O(n) moves, a terminal configuration is reached. Finally, by Lemma 47, this terminal configuration is legitimate.

  ) If a finite number of signals are launched, a configuration in C ResetAlg

					normal
	is reached.
	3. (Reset) Starting from any configuration in C ResetAlg saf e	, if a finite number of signals
	and at least one are launched, C BasicAlg reset	is reached.
	Remark 4. Notice that C	ResetAlg saf e	contains C	ResetAlg normal in the current self-stabilizing im-
	plementation of ResetAlg. We later prove (Proposition 5) that it contains only one
	configuration C

ResetAlg

normal (Def. 8) and it is terminal (if reset signals, and faults, cease).

  ResetAlg normal is the configuration in which all nodes have status = normal, are consistent and no boolean signal is True. We denote by PredRTerm be the predicate defining C

	ResetAlg normal .
	Definition 9 (Safe configurations C ResetAlg saf e

Definition 8 (C ResetAlg normal ). C

  Corollary 6. Let C be a configuration where ∀v : status v = initiate and no node is eligible for Variables_Consistency, Reset_Launch and Neighbors_Coherence. From C, in any execution in which no node is eligible for Reset_Launch, no node is eligible for Variables_Consistency and Neighbors_Coherence. Let us prove this lemma by contradiction: suppose that a node v is activated twice for Neighbors_Coherence from C 1 and C 5 . Notice that v cannot be a leaf since leaves are not eligible for Neighbors_Coherence. This implies two facts: a) in both configurations, at least one v 's child is an initiate-node and b) between C 1 and C 5 , v is activated for Freeze and Reset in this order. Let C 2 be the configuration from which v is activated for Freeze and C 3 the one from which v is activated for Reset. In C 2 , ∀c ∈ children(v), st c,v ∈ {f reeze, reset} and in C 3 , ∀c ∈ children(v), st c,v = reset. Thus, between C 2 and C 3 , all v's children are activated for Freeze and Reset in this order. Recursively, the argument applies up to the leaves: each descendant (children, grandchildren, etc.) of v is activated for Freeze and Reset, in that order, between the two activations (Freeze and Reset) of its parent. This implies that all nodes have been activated at least once before C 3 , i.e. they are no more eligible for Variables_Consistency (by Lemma 48).

	Lemma 50. In any execution, a node is activated at most once for Neigh-
	bors_Coherence.
	Proof.

.2.2.2.2 -C ResetAlg normal is the Unique Terminal Configuration of ResetAlg

  In this sub-section, we prove that, unless a node becomes eligible for Reset_Launch, C ResetAlg normal is terminal and there is no other terminal configuration. In Lemmas 51 -53, we prove that nodes in a terminal configuration are not in status f reeze, reset or initiate. This implies Proposition 5: terminal configurations are those with node's status and shared variables set to normal. Nodes are consistent, otherwise Vari-ables_Consistency would be enabled and the configuration wouldn't be terminal. C ResetAlg normal is the unique configuration satisfying this properties. In a terminal configuration, no node has status = f reeze. Proof. Assume that there exists a node v with status v = f reeze in a terminal configuration C. In C, nodes are coherent (i.e. shared and local variables are equal) otherwise Variables_Consistency would be enabled. First, let us consider that v is a leaf. Node v is eligible for Reset no matter its parent's status. Thus, if status

	Lemma 51.

IV.2.2.2.6 -Main Theorem : ResetAlg Correctness and Complexity

	Recall that the self-stabilizing reset specification is in Definition 7, the configuration
	C	ResetAlg normal in Definition 8 and the safe configuration C	ResetAlg saf e	in Definition 9.
	Theorem 4. Assuming that a tree of depth p is built, ResetAlg satisfies the self-
	stabilizing reset specification (as specified in Definition 7) in O(n • 6 p ) moves, i.e., the
	configurations specified to be reached in every corresponding condition of this specifica-
	tion are each reached in O(n • 6 p ).
	Proof. First, Lemmas 56 proves that from any configuration, a configuration in C ResetAlg saf e is reached in O(n6 p ) moves, i.e. point 1 (Convergence) of the definition is satisfied.
		The Lemma 58 proves that, if there is a finite number of signals, ResetAlg terminates
	(in C ResetAlg normal ) in O(n6 p ) moves: point 2 (Termination) is satisfied.
		Finally, the point 3 (Reset) is proved to be satisfied by Lemma 59 in O(n) moves.

  The longest sequence of ResetAlg's activations that does not require a shared variable update of the neighbors is either: i) Reset and then Back_Normal or ii) Reset_Launch or Vari-ables_Consistency or Initiate and then Freeze Thus, w can be activated at most for 2 moves. If neighbors' min values are False, w "thinks" she is a leaf. Node w can be activated for at most 3 moves: for Variables_Consistency or Reset_Launch, for Freeze and then, for Reset (see Figures 5.11 and 5.13).Furthermore, if status w = normal (after Back_Normal or before Reset_Launch or Variables_Consistency or Initiate, for example), v can be activated for 2 moves of Async-GSA: Refusal_Management and then either Propose or Refuse.Comp_Local_Check is not enabled since w is a woman. Thus, after at most 5 moves (3 of ResetAlg + 2 of Async-GSA), w cannot anymore be activated if its neighbors are not activated. Let C be any configuration in which there is a woman w not eligible for TreeAlg and with Tree_LC satisfied. From C, w is activated for at most 7 moves before its last activation for TreeAlg.Proof. Since w is not eligible for TreeAlg's rules in C, its shared registers are consistent and thus Update is never enabled for w. Moreover, since Tree_LC is satisfied in C, its neighbors are coherent: their shared variables min have the same value True or False. If w's neighbors are not activated for Update, w is not anymore eligible for TreeAlg. If some w's neighbors are activated for Update, this means that all its neighbors' min have a wrong value: all w's neighbors will be activated for Update. In this case, w will be activated either for I_am_root (if in C the values are False) or I_am_not_root (if in C the values are True) in a configuration C 1 . The execution can be divided into two parts: before the first w's neighbors' activation and after this activation. In the following, we analyze each part.Before the first neighbor's activation, by Lemma 63, w can make at most 5 moves. After at least one w's neighbors' activation for Update, w is either i) still not eligible for TreeAlg and with Tree_LC not satisfied (min values were False and not all men have been activated) or ii) eligible for TreeAlg (I_am_not_root) and with Tree_LC not satisfied (min values were True and not all men have been activated) or iii) eligible for TreeAlg (I_am_root or I_am_not_root) and with Tree_LC satisfied (all men have been activated for Update in the same step). Notice that the case in which w is still not eligible for TreeAlg and with Tree_LC satisfied is not possible.If w is in case i), by Lemma 61, it cannot make any move before C 1 . If w is in case ii), by Lemma 62, it can make at most 2 moves before C 1 . Finally, if w is in case iii), it is eligible either for I_am_root (if min values are True) or I_am_not_root (if min values are False). Since by Lemma 46 men are activated once for Update, the min values will not change again. Thus, w's next activation can only be for its last TreeAlg's rule.Thus, after at most 7 moves, w's next activation can only be for its last TreeAlg's rule. Let C be any configuration in which there is a woman w eligible for TreeAlg and with Tree_LC satisfied. From C, w is activated for at most 9 moves before its last activation for TreeAlg.Proof. In C, w is eligible for any of the 3 TreeAlg's rules and, by Lemma 46, it is eligible at most once for each rule. The order of activation depends on the neighbors shared values.In C, w is eligible for at most 2 moves: either one Update and one I_am_root (if neighbors' min values are True in C) or Update and I_am_not_root (if neighbors' min values are False). Let suppose that w is activated for Update and is also eligible for I_am_root or I_am_not_root. After this move, Tree_LC may be not satisfied if at least one neighbor has also been activated for Update in the same transition. In this case, by Lemma 61 and Lemma 62, after at most 2 moves, w is activated for its last activation. If after the w's activation for Update, Tree_LC is still satisfied, w is still eligible for either I_am_root or I_am_not_root. Notice that, before the next w's activation, Tree_LC can be not anymore satisfied. If so, again by Lemma 61 and Lemma 62, after at most 2 moves, w is activated for its last TreeAlg's rule. Consider now that w is activated for either I_am_root or I_am_not_root. After this activation, there are several cases. • Either Tree_LC is still satisfied and w not eligible for TreeAlg (no neighbor's Update during the same transition). By Lemma 64, after at most 7 moves, w is activated for it last TreeAlg's rule.

	Lemma 64. Lemma 65.

PredT is satisfied Lemma 68.

  Starting from a configuration C where PredT is satisfied, CompAlg reaches a terminal configuration in O(n 2 ) moves where PredAsync-GSA is satisfied too. Proof. Since in C PredT is satisfied, by Lemma 56, in O(n) moves, a configuration C 1 in C , men with status = normal and with a local predicate LP false can be activated for Comp_Local_Check. This new signal does not interrupt the convergence of ResetAlg to C ResetAlg

	ResetAlg saf e	is reached.
	Between C and C 1 saf e

  C 1 is reached, if Comp_Local_Check is activated (at most once per man, since reset signal launch changes the status of a node to initiate and that ResetAlg satisfies the specification 7), a reset is launched and C BasicAlg reset is reached in additional O(n) moves (by Lemma 59). During this convergence to C BasicAlg reset , normal-nodes may be activated for Async-GSA for O(n 2 ) moves together (by Lemmas 42 and 41 and the f reeze wave is propagated normally -the reset and the tree are stabilized -from the root to the leafs interrupting all nodes before resetting). By definition of C BasicAlg reset , by Corollary 5, a terminal configuration (a projection on Async-GSA) C 3 satisfying PredAsync-GSA is reached after O(n 2 ) additional moves (since Async-GSA is locally checkable and by Lemma 43). At that moment, a terminal configuration of the whole composition CompAlg is reached. The algorithm CompAlg solves the stable marriage problem in O(n 2 ) moves. Proof. By Lemma 67, from any configuration in which PredT is not satisfied, after O(n 2 ) moves, a configuration C in which PredT is satisfied is reached. From C, by Lemma 68, after O(n 2 ) moves, a terminal configuration where PredAsync-GSA is satisfied is reached.

	BasicAlg reset	(here, C BasicAlg reset	is C Async-GSA init	), Π is now satisfied and since Async-GSA is lo-
	cally checkable, Comp_Local_Check cannot be enabled anymore. Then, in O(n)
	moves, C ResetAlg normal -a terminal configuration projected on ResetAlg -is reached. From
	C
	Theorem 5.

Notice e.g. the tolerance demanding problem of scheduling charging points to electric vehicles on route, described in the previous section).

Notice that constants, like IDs or preference lists, are assumed to be incorruptible.

A node v only communicates to its neighbor u the priority it gives to u, and the priority of its actual spouse.

If the last man refuses the proposal, this rule cannot be enabled.

For simplicity, we have a constant b for every node, but this can be easyly adapted to the case where each node u has its individual capacity bu.

Recall that it is assumed that node u communicates to v ∈N (u) the value of priority(u,v). Thus, together with the previous assumptions, it is required that u communicates the priority priority(u,v) = n + 2 to an unacceptable node v.

One assumes that the capacity b is known in advance by the residents or that they can read it in a register.

Université Paris-Saclay Espace Technologique / Immeuble Discovery Route de l'Orme aux Merisiers RD 128 / 91190 Saint-Aubin, France

Proof. Let m be a man and let w be a woman. According to Lemma 31, m can only execute Confirm or Accept in E. In the same way, according to Lemma 30, w can only execute Reset, Confirm2 or Propose2 in E. We count the maximum number of rules that can be executed.

Confirm: according to Lemma 32, between two consecutive executions of Confirm by m, m updates its marriage preference. Thus a man executes O(n) Confirm. So the number of Confirm in E is in O(n 2 ).

Propose2: according to Lemma 35, between two consecutive executions of Propose2 by w, there exists a man that executes Confirm. So, a woman executes O(n 2 ) Propose2. Thus the number of Propose2 in E is in O(n 3 ).

The Reset and Confirm2: according to Lemma 36, between three consecutive executions of any rule of w, w executes at least one Propose2. So, a woman executes

The Accept: we consider all Accept executed by m in E. They can be divided into three types: (i) the first Accept, (ii) an Accept such that m executed at least one rule between this Accept and the previous one and (iii) an Accept such that m did not execute any rule between this Accept and the previous one. We count the number of Accept of each type. First, Accept of type (i) appears once. Accept of type (ii): By Lemma 31, the rule m executed between this Accept and the previous one is a Confirm. The number of Confirm executed by a man is in O(n), thus the number of Accept of type (ii) executed by a man is in O(n) too. Accept of type (iii): By Lemma 37, between this Accept and the previous one, both executed by m, there exists a woman that has executed a rule. The number of rules executed by some woman is in O(n 3 ) so the number of Accept of type (iii) executed

by men is in O(n 3 ) too. We finally obtain that the number of Accept executed by men is in O(n 3 ) and so the number of Accept is in O(n 4 ).

Then the number of rules executed in E is in O(n 4 ).

IV -Conclusion

In this chapter, we presented the first asynchronous self-stabilizing algorithm [LMB + 17] for SMP. This algorithm (Alg. 1 and 2) is a distributed asynchronous self-stabilizing adaptation of the Ackermann et al.'s algorithm [AGM + 11]. Their algorithm works with two different phases in which different nodes are eligible to perform actions. It implies that the algorithm needs some synchronization between nodes. This is the main difficulty especially since the unfair distributed daemon can chose nodes that do not make the system progress. Thus, useless moves can delay the convergence to the stable marriage.

In particular, we notice that in the first phase women detect blocking pairs and solve them by local repairs (in getting married with the blocking partner). Since the system is asynchronous and distributed, O(n 2 ) moves are needed to resolve one BP. An instance of SMP contains O(n 2 ) BPs. Thus, we proved a time complexity of O(n 4 ) moves and this is also an upper bound in term of rounds.

The lower bound of Ω(n 2 ) boolean queries [START_REF] Gonczarowski | A Stable Marriage Requires Communication[END_REF] rises the following question: is it possible to build an algorithm with a better time complexity? This question is relevant since we show that resolving a BP locally in distributed settings is costly. In an other hand, the local detection is efficient: in one move, a node is aware of its involvement in a BP. Since applications need low time complexity, it is pertinent to search time improvement on BP's repairs. One way to solve this problem is to repair globally the system after a local BP detection. This is the subject of the next chapter. Note that the obtained matching is not the only stable marriage. There are others that cannot be obtained by this algorithm. See an example in Figure 5.4. Thus, we consider executions in which there is no reset signal launched, i.e., the environment does not set signal to True. By Lemma 55, the root can be activated twice for Reset in any execution (with or without signal). Nodes in the reached configuration after the second Reset's activation are all reset-nodes and they are coherent. This allows us to prove that, from any configuration, the root can be activated at most 9 times (Lemma 57 -the figure 5.13 represents the possible transitions after each rule) if there is no new signal. Using the fact that a node is activated for at most 6 moves between 2 successive moves of its parent, we show that a node at depth p can be activated 9 • 6 p times. This results in an overall complexity of O(n • 6 p ) moves (Lemma 58). This implies that ResetAlg converges and thus reaches a terminal configuration (where no node is eligible), which is necessarily C ResetAlg normal by Proposition 5.

Lemma 57. From any configuration C, the root r is activated for at most 9 rules in any execution with no new signal.

Proof. By Lemma 55 and Corollary 7, from any configuration, r can be activated twice for Reset (in C and C 1 ) and after the second activation, all nodes v are coherent and have status v = reset. Before C, r can be activated for at most 3 rules (Back_Normal, Initiate and Freeze -the figure 5.13 represents the possible sequence of rules). Between C and C 1 , r is activated for at most 3 rules (Back_Normal, Initiate and Freeze). From this configuration, this is easy to see that, since there is no new signal, each node is activated once for Back_Normal. Since no node is anymore eligible, this is a terminal configuration, i.e. the terminal configuration C ResetAlg normal (Proposition 5). Thus, from any configuration, the root is activated at most 9 times. We provide the following figure5.13 adapted to the proof of Lemma 57. It depicts the sequence of rule's activations. Similar labels as in Figure 5.11 are used. "1" means that the rule is only activated once (for example Variables_Consistency, by Lemma 48 or Neighbors_Coherence by Lemma 50). " " means that this transition is not possible for the leaves. We add a label " " to denote a transition which is not applied to the root.

V.2 -Correctness and Complexity Analysis of CompAlg (Algorithm 7)

Contrary to the classical time analysis in terms of rounds (asynchronous or synchronous) where the overall complexity of a composition is normally obtained by summing up the complexities of the modules, in case of moves, this complexity is upper-bounded by the multiplication of the modules' complexities. This is because with a distributed (asynchronous), and especially unfair, daemon, some nodes can be retained from being activated for a very long time (even though, they are eligible). Imagine a composition of two algorithms

, respectively, while executed in a stand alone mode. Moreover, to stabilize, A 2 assumes that A 1 has already stabilized to a correct configurations (satisfying the specification). That is, the composition of A 1 and A 2 stabilizes only after A 2 has stabilized, following the stabilization of A 1 . Now, notice that the considered daemon may privilege to activate the nodes eligible for A 2 rules, while retaining from the execution those eligible for A 1 , as long as possible.

In a distributed setting, nodes executed for A 2 may not be aware that A 1 is not yet stabilized. Their moves thus may add an overhead of O(f 1 (n)) to each move executed by A 1 (each such move may restart the computation of A 2 ). That is why the rough move complexity analysis of the composition results in the multiplication

). We will perform a tighter time analysis proving an O(n 2 ) move complexity for CompAlg. This analysis is complex due to several reasons. One is because we cannot ignore moves that are done out of the order needed by the modules for their respective stabilization (like those of A 2 above, executed before A 1 has been stabilized). In addition, the communication model by registers allows nodes to communicate different information to their neighbors, making the stabilization analysis more complex. Another reason is the quite complex interleaving of the CompAlg's modules: ResetAlg runs on a stabilized tree (assuming PredT is satisfied) and the rule Comp_Local_Check checks the variables of Async-GSA (local predicate LP) to trigger a reset signal sent to ResetAlg.

The latter reason leaded us to analyze the CompAlg's convergence in two parts. We first prove that, from any configuration C 0 , a configuration C T in which PredT is satisfied, i.e., where the tree is stabilized, is reached, while analyzing the corresponding time complexity. In the second part, we analyze the stabilization time from C T until a terminal configuration C M in which PredAsync-GSA (global predicate for a stable marriage with Async-GSA), PredT (global predicate of the tree built by TreeAlg) and PredRTerm (global predicate of the terminal configuration of ResetAlg), are all satisfied.

In the first part of the analysis, we consider two types of nodes: (1) nodes that will be activated for TreeAlg between C 0 and C T and (2) nodes that are already stabilized for the tree (they are no anymore eligible for any TreeAlg's rule). Notice that nodes which are activated for the last time for a TreeAlg's rule change from type (1) to type (2). The main idea of the proof is to analyze how much moves can be made by a node before C T , depending on its type. Figure 5.15 illustrates (using similar conventions as in Figure 5.12) a possible coexistence of such types of nodes during the segment between C 0 and C T . The last activated node for TreeAlg is v so, it is of type (1) (during the red 3. Tree_LC is satisfied and v is not eligible for TreeAlg or, 4. Tree_LC is satisfied but v is eligible for TreeAlg.

First, by Lemma 60, if v is a man, no matter the type, it can make at most 1 move before its last activation. Now, let v be a woman. Women of type 1, 2, 3 and 4, make 0, 2, 7 and 9 moves respectively, by Lemma 61, Lemma 62, Lemma 64 and Lemma 65, respectively.

Thus, after at most 9 of it own moves, v is only eligible for its last TreeAlg's rule.

Lemma 67. Let C be any configuration in which PredT is not satisfied. From C, a configuration C 1 in which PredT is satisfied is reached in at most O(n 2 ) moves.

Proof. Assume that such a configuration C 1 is never reached. There are tree possibilities:

1. either no node is eligible for TreeAlg but PredT is not satisfied, or 2. some nodes are infinitely often activated for TreeAlg, but PredT is never reached, or 3. at least one node u that is eligible (or will be eligible) for TreeAlg, is never activated.

By Lemma 47 (any terminal configuration (of TreeAlg) satisfies PredT) and the fact that TreeAlg is activated in Comp_Tree with no restriction (first priority in CompAlg), case 1 is not possible.

Furthermore, by Lemmas 45 and 46, each node is eligible at most 3 times for TreeAlg and by Lemma 47, when all nodes have been activated for TreeAlg, C 1 is reached. Thus, case 2 is also not possible. Now, let us consider case 3. We show that, between C and C 1 , the set of other (than u) nodes (those not activated for TreeAlg) are eligible for at most O(n 2 ) moves in overall. This implies that u cannot stay unactivated, i.e. C 1 (in which PredT is satisfied) is reached.

Let us thus analyze the move complexity, during the execution segment from C till C 1 , of the set S of nodes which are never eligible for TreeAlg rules, i.e., for which GuardsTreeAlg is not satisfied during the whole execution. These nodes form a forest that is part of the future tree. Other nodes, eligible for TreeAlg, may join the sub-trees (forest), but a cycle (of parent pointers) can never be formed, since this requires for a node in S to be activated for TreeAlg. Such joins are made after the last TreeAlg's move of those nodes, i.e. after their O(1) moves (of any type). Thus, a leaf v still eligible for TreeAlg is not in the forest. Notice that ResetAlg uses convergecasts and broadcasts to propagate the waves. Thus, M min and W min wait for answers from their children before being eligible, i.e., v's parent cannot run the algorithm to convergecast a wave. Similarly, if M min or W min are not in the tree, broadcast waves cannot be completed. Hence, while not all nodes are in this tree (PredT is not satisfied), waves are blocked. But when nodes (eligible for TreeAlg) are activated for their last action (for TreeAlg), they "take their place" in the tree and participate to the current blocked wave. Furthermore, when joining the tree, nodes cannot "disturb" the waves: either the nodes already have the required (by the current wave) status or it shifts to initiate (Variables_Consistency, Adaptation of CompAlg. This is also the easiest variant for CompAlg since it needs no change. Indeed, the only problematic point is the the presence of singles (a woman reaching the end of its list or a man receiving no proposal) in the final matching. In this situation no reset signal should be launched since matching is stable. In this matching, nodes in the opposite set of the singles are all matched to a better ranked partner than the singles (since the matching is stable). Hence, as each time preferences are checked using the local predicates, no reset signal can indeed be launched.

II -Stable Matching with Indifference (preference lists with ties), b = 1

In this variant, ordering in the preference lists is not required to be strict. In the literature studying this variant (e.g., [IMM99, BM06, IMO09]), several sub-variants are considered. These variants affect the stability of the required matching, and depend on the definition of BP. There are three ways to extend Definition 10 of a BP (w, m). In all of them, points 1 and 2 in Def. 10 remain the same. Points 3 and 4 may be kept or slightly modified:

(a) w and m strictly prefer each other (like in Def. 10), (b) w strictly prefers m and w is not worse than the actual partner of m, or reciprocally (that is replacing in 3 or 4 < should be replaced respectively by ≤), (c) m is not worse than the actual respective partner of w and reciprocally (that is replacing in 3 and 4 < by ≤).

Depending on the choice, the type of matching stability changes. With (a) it is called weakly stable, with (b) strongly stable and with (c) super stable. With (b) and (c), there is no guarantee that a stable marriage exists [START_REF] Irving | Stable marriage and indifference[END_REF].

Jane

Adaptation of both Algorithms to Condition (a).

It suffices to remark that, when breaking the ties arbitrarily, a matching stable with condition (a) is a stable marriage (as noticed in [START_REF] Irving | Stable marriage and indifference[END_REF]). Thus only a slight modification of the proposed algorithms is needed. The ties are arbitrarily broken in advance, and the corresponding preference lists are appropriately adjusted. There is no change in the complexity analysis of both algorithms.

Conditions (b) and (c)

Both cases raise a general issue concerning problems for which there is not always a stable matching. If their specification only concerns terminating executions (in a configuration with a stable matching), both solutions are still relevant. If their specification asks also for detecting the absence of stable matching, the issue is complicated (in particular, non-terminating executions are possible). We delay its discussion to the last chapter on perspectives (Chapter 7, Section II).

III -Unacceptable Partners (incomplete preference lists), b = 1

In this variant, some partners can be unacceptable for some nodes. This means that a node prefers to stay single rather than to be matched to an unacceptable partner. This is expressed in the preference list so that unacceptable partners are absent. In other words, they are not ranked. As mentionned in [START_REF] Irving | Stable marriage and indifference[END_REF], some nodes can be single in a final stable marriage. However, a stable marriage always exists (possibly with single nodes) [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF].

Jane

The first part of this predicate detects the cases where the woman is proposing to an unacceptable partner. Indeed, if a man is unacceptable for a woman, the woman cannot propose to this man. Thus, if request w,m = None, this is because of a bad initialization.

The second part allows to detect when men accept unacceptable partners. Note that, since P U nacceptable m,w only read local variables or registers and the Async-GSA rules cannot create states not satisfying this predicate, Async-GSA is still locally checkable. Furthermore, this does not change Async-GSA's complexity, neither the global complexity of CompAlg.

IV -Many-to-One (Hospitals-to-Residents Problem)

This variant, introduced by Gale and Shapley in their seminal work [START_REF] Gale | College Admissions and the Stability of Marriage[END_REF], considers two sets of members, hospitals and residents, of different sizes. Each hospital can be matched with several residents, up to its capacity b ≥ 1, and each resident can be matched to a single hospital. The sum of capacities has not to be equal to the number of residents. Adaptation for both Algorithms. A reduction from the many-to-one case to the one-to-one case is known [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF]. At the algorithm level, each occurrence of a hospital h in the preference list of a resident is replaced by the sequence h

Jane

of hospital instances (the ties between this instances are broken arbitrarily) 3 . Then, at each activation of a hospital h with capacity b, b similar instances,

of the algorithm are executed sequentially. In this transformation, a hospital node is eligible if at least one of the rules of any of its b instances is enabled. Then, it can be activated, if chosen by the scheduler. The resulting stable matching corresponds to the many-to-one matching. For the time complexity of this extension, refer to the complexity of the more general many-to-many variant.

V -Many-to-Many

The many-to-many extension of the stable marriage and its variants have been intensivelystudied in the literature (e.g., [Sot99, BAM03, MMNO04, BAM07, FGS10, EO16]). Maybe the reason is that the formulation of the problem corresponds to real situations involving markets. There are many variations of the many-to-many stable matching. Some formulations use preference lists of subsets and do not assume any compatibility (for instance the subset {v 1 } can be more preferred than the larger subset {v 1 , v 2 }).

In all generality, a stable matching does not always exist. These variants are far from the solution that we gave and we will only focus here on the case of responsive preferences [START_REF] Roth | Two-sided Matching: A Study in Game-Theoretic Modeling and Analysis[END_REF][START_REF] Alkan | On the properties of stable many-to-many matchings under responsive preferences[END_REF], that is when preferences over subsets are consistent with the individual preferences over nodes (e.g., for example,

Thus, simple sequences of nodes specify preference lists. This also implies that our extended definition of stable marriage (in this chapter) includes this variant of SMP with responsive preferences. It is known that a stable marriage always exist with responsive preferences, and in the case where initialization of the nodes is allowed, an iterative variant of the Gale and Shapley algorithm can be used (see [START_REF] Alkan | On the properties of stable many-to-many matchings under responsive preferences[END_REF]). Here, we focus on the basic case having possibly two different size sets and unacceptable partners. Their members are commonly named workers and firms and each one can be matched multiple times (up to its capacity b ≥ 1). ...), and we base our second solution on them. The originality of the one that we suggest is the consideration of the unfair demon, as well as the fact that a tight bound on the moves complexity for the transformed algorithm could be obtained (as a function of the move complexity of the initialized algorithm). In the context of this thesis, a privileged application domain of such a syntactic transformer would be the different variants of SMP that have been studied, and received solutions, for some of them, in a centralized setting. Most of them seem to satisfy the local checkability property and thus be liable for the general transformation. An issue appears with variants that do not always have a solution. We discuss them in the next paragraph.

Jane

Problematic Variants. Beside the variants that we listed in Chapter 6, there are other variants, for which getting a self-stabilizing solution seems unattainable, with the techniques that we proposed. We list in the following variants that seem difficult to solve by a simple adaptation of any of the two types of solutions we gave (two phases and composition with a reset), thus presenting open questions. These variants are stable roommates, incomplete bipartite graph, 3-dimensional matching, strongly and super stable matching with indifference. They appear in the reference book [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF] and are among the twelve research directions suggested by Knuth [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF]. We explain the general reasons why the solutions we developed cannot be applied to these variants. Recall that, by [START_REF] Irving | Stable marriage and indifference[END_REF], stable marriage is not guaranteed in these cases (there is no super stable marriage in the system of Figure 7.1). Section II describes a simple self-stabilizing solution that does not detect the case lacking a stable marriage. Implementing such detection in a self-stabilizing manner is indeed not simple and previous existing solutions are not appropriate.

Strongly and super stable matching with indifference. These two variants

They are centralized, initialized and detect the lack of a stable marriage as follows. If a node exhausts all the possible partners in its preference list during an execution, it reaches a state s, encoding the fact it can conclude that no stable marriage exists [START_REF] Irving | Stable marriage and indifference[END_REF]. However, when self-stabilization is required (convergence from any initial configuration), such an approach is inappropriate. For example, if a node starts in state s, it can incorrectly conclude that no stable marriage exists. Hence, both our solutions do not extend to strongly and super stable matching with indifference (but, if only instances in which a stable matching exists are proposed, it seems feasible to extend them). Amira10

Stable roommates problem. Contrary to the stable marriage, this problem is defined on a complete communication graph, where each node has a preference list over all other nodes. The problem consists to build a stable matching, which is a complete matching without blocking pairs. In this context, a pair (u, v) is a blocking pair iff (u, v) / ∈ M and u and v prefer each other to their actual matching, with no restriction over sets. Building a stable matching is not always possible, like in the following example (the matching is represented in black and the blocking pairs in red): In [START_REF] Gusfield | The Stable Marriage Problem: Structure and Algorithms[END_REF], a centralized algorithm is given to determine whether a given instance admits a stable matching, and if so finds one. Intuitively, this determination is done similarly to the technique used in [START_REF] Irving | Stable marriage and indifference[END_REF] for detecting the lack of stable marriage, by verifying that a node has exhausted all the possible partners in its preference list. As before, this approach is inappropriate for self-stabilization.

Moreover, the communication graph being complete, the two phases technique of Ackermann et al., based on two distinct sets, is not appropriate either. 3-dimensional matching. This last variant has been proposed by Knuth in [START_REF] Knuth | English translation in Stable Marriage and its Relation to Other Combinatorial Problems[END_REF] as a generalization of the stable marriage problem to three dimensions (e.g., to the 3-gender stable matching problem with men, women and dogs). In [START_REF] Alkan | Nonexistence of stable threesome matchings[END_REF], Alkan defines the problem (participants are allowed to express preferences over all pairs they could possibly join), shows an example for which there is no solution and generalizes the result to k-dimensional graphs. Ng and Hirschberg in [START_REF] Ng | Three-dimensional Stable Matching Problems[END_REF] prove that this problem is NPcomplete.

As for the stable roommates problem, the communication graph is not bipartite. Thus, the Ackermann et al.'s technique based on two distinct sets is not appropriate. Furthermore, there is no known distributed algorithm for this problem, i.e. the basic element in the composition is missing.

Incomplete bipartite graph.

Several types of systems can be considered under this variant. In the main studied version (considered in [START_REF] Kipnis | A Note on Distributed Stable Matching[END_REF] for example), preferences are related to the graph topology, in the sense that two non-neighbors are unacceptable partners. In this case , even if the graph is not connected, a solution is feasible, but requires an important modification to the given solutions. We start by describing briefly the modifications to bring to the two phase algorithm of Chapter 4. For ensuring correct transitions between phases, nodes have to know in which phases the opposite set nodes are. But, as a complete broadcast cannot be directly (in one step) performed if the graph is incomplete, one solution would be to combine the presented algorithm with a self-stabilizing rooted tree construction (e.g., [AG90, AKM + 07]) in each connected component. This is for propagating an information along the tree (upward to and downward from the root), regarding the types of phases' states (for each of the two opposite sets). In this way every node could have (a possibly outdated) information about the type of phases in the other set. But the changes in phases cannot be propagated immediately, causing a different behavior comparing to the original algorithm variant. Neither the proof nor the complexity analysis of the basic algorithm apply to this case.

Concerning the solution based on local checkability and reset, the main issue is the tree. Indeed, since the graph is not complete, in the worst case, the tree is of depth n, increasing considerably the global complexity. Any known spanning tree construction can be used to obtain this tree.