Synthesis of mutual exclusion solutions based on binary semaphores

A graphical form of the mutual exclusion problem is considered in which each vertex represents a process and each edge represents a mutual exclusion constraint between the critical sections of the processes associated with its endpoints. An edge semaphore solution for mutual exclusion problems is defined, and those graphs which are edge solvable are characterized in terms of both a forbidden subgraph and a graph grammar. Finally, an efficient algorithm is given which generates the entry and exit sections for all processes in an edge-solvable problem     

Superstabilizing mutual exclusion

Summary. A superstabilizing protocol is a protocol that i is self-stabilizing, meaning that it can recover from an arbitrarily severe transient fault; and ii can recover from a local transient fault while satisfying a passage predicate during recovery. This paper investigates the possibility of superstabilizing protocols for mutual exclusion in a ring of processors, where a local fault consists of any transient fault at a single processor; the passage predicate specifies that there be at most one token in the ring, with the single exception of a spurious token colocated with the transient fault. The first result of the paper is an impossibility theorem for a class of superstabilizing mutual exclusion protocols. Two unidirectional protocols are then presented to show that conditions for impossibility can independently be relaxed so that superstabilization is possible using either additional time or communication registers. A bidirectional protocol subsequently demonstrates that superstabilization in O(1) time is possible. All three superstabilizing protocols are optimal with respect to the number of communication registers used. Received: August 1996 / Accepted: March 1999     

Randomized mutual exclusion with sub-logarithmic RMR-complexity

Mutual exclusion is a fundamental distributed coordination problem. Shared-memory mutual exclusion research focuses on local-spin algorithms and uses the remote memory references (RMRs) metric. Attiya, Hendler, and Woelfel (40th STOC, 2008) established an Ω(log N) lower bound on the number of RMRs incurred by processes as they enter and exit the critical section, where N is the number of processes in the system. This matches the upper bound of Yang and Anderson (Distrib. Comput. 9(1):51–60, 1995). The upper and lower bounds apply for algorithms that only use read and write operations. The lower bound of Attiya et al., however, only holds for deterministic algorithms. The question of whether randomized mutual exclusion algorithms, using reads and writes only, can achieve sub-logarithmic expected RMR complexity remained open. We answer this question in the affirmative by presenting starvation-free randomized mutual exclusion algorithms for the cache coherent (CC) and the distributed shared memory (DSM) model that have sub-logarithmic expected RMR complexity against the strong adversary. More specifically, each process incurs an expected number of O(log N / log log N) RMRs per passage through the entry and exit sections, while in the worst case the number of RMRs is O(log N).     

Adaptive mutual exclusion with local spinning

We present an adaptive algorithm for N-process mutual exclusion under read/write atomicity in which all busy waiting is by local spinning. In our algorithm, each process p performs O(k) remote memory references to enter and exit its critical section, where k is the maximum “point contention” experienced by p. The space complexity of our algorithm is Θ(N), which is clearly optimal. Our algorithm is the first mutual exclusion algorithm under read/write atomicity that is adaptive when time complexity is measured by counting remote memory references.A preliminary version of this paper was presented at the 14th International Symposium on Distributed Computing [6].     

Nonatomic mutual exclusion with local spinning

We present an N-process local-spin mutual exclusion algorithm, based on nonatomic reads and writes, in which each process performs Θ(log N) remote memory references to enter and exit its critical section. This algorithm is derived from Yang and Anderson's atomic tree-based local-spin algorithm in a way that preserves its time complexity. No atomic read/write algorithm with better asymptotic worst-case time complexity (under the remote-mem-ory-refer-ences measure) is currently known. This suggests that atomic memory is not fundamentally required if one is interested in worst-case time complexity.The same cannot be said if one is interested in fast-path algorithms (in which contention-free time complexity is required to be O(1)) or adaptive algorithms (in which time complexity is required to depend only on the number of contending processes). We show that such algorithms fundamentally require memory accesses to be atomic. In particular, we show that for any N-process nonatomic algorithm, there exists a single-process execution in which the lone competing process accesses Ω(log N/log log N) distinct variables to enter its critical section. Thus, fast and adaptive algorithms are impossible even if caching techniques are used to avoid accessing the processors-to-memory interconnection network.This paper was invited for inclusion in the special issue of this journal based on selected papers presented in PODC '02 (Distributed Computing 18(1)).It appears separately because of a publication delay. Yong-Jik Kimreceived a B.S. degree in Physics/Computer Science from Korea Advanced Institute of Science and Technology in 1998, and a Ph.D.degree in Computer Science from the University of Notrh Carolina at Chapel Hill in 2003. He currently works for the RDBMS group in Tmax Soft, and is otherwise occupied with his newborn daughter Darum, which means “difference” in Korean. James H. Anderson is a professor in the Department of Computer Science at the University of North Carolina at Chapel Hill. He received a B.S.degree in Computer Science from Michigan State University in 1982, an M.S. degree in Computer Science from Purdue University in 1983, and a Ph.D. degree in Computer Sciences from the University of Texas at Austin in 1990. Before joining UNC-Chapel Hill in 1993, he was with the Computer Science Department at the University of Maryland between 1990 and 1993. Dr.Anderson's main research interests are within the areas of real-time systems and concurrent and distributed computing.     

Closing the complexity gap between FCFS mutual exclusion and mutual exclusion

First-Come-First-Served (FCFS) mutual exclusion (ME) is the problem of ensuring that processes attempting to concurrently access a shared resource do so one by one, in a fair order. In this paper, we close the complexity gap between FCFS ME and ME in the asynchronous shared memory model where processes communicate using atomic reads and writes only, and do not fail. Our main result is the first known FCFS ME algorithm that makes O(log N) remote memory references (RMRs) per passage and uses only atomic reads and writes. Our algorithm is also adaptive to point contention. More precisely, the number of RMRs a process makes per passage in our algorithm is Θ(min(k, log N)), where k is the point contention. Our algorithm matches known RMR complexity lower bounds for the class of ME algorithms that use reads and writes only, and beats the RMR complexity of prior algorithms in this class that have the FCFS property.     

Asynchronous group mutual exclusion

Abstract. Mutual exclusion and concurrency are two fundamental and essentially opposite features in distributed systems. However, in some applications such as Computer Supported Cooperative Work (CSCW) we have found it necessary to impose mutual exclusion on different groups of processes in accessing a resource, while allowing processes of the same group to share the resource. To our knowledge, no such design issue has been previously raised in the literature. In this paper we address this issue by presenting a new problem, called Congenial Talking Philosophers, to model group mutual exclusion. We also propose several criteria to evaluate solutions of the problem and to measure their performance. Finally, we provide an efficient and highly concurrent distributed algorithm for the problem in a shared-memory model where processes communicate by reading from and writing to shared variables. The distributed algorithm meets the proposed criteria, and has performance similar to some naive but centralized solutions to the problem. Received: November 1998 / Accepted: April 2000     

Queue based mutual exclusion with linearly bounded overtaking

The queue based mutual exclusion protocol establishes mutual exclusion for N>1 threads by means of not necessarily atomic variables. In order to enter the critical section, a competing thread needs to traverse as many levels as there are currently competing threads. Competing threads can be overtaken by other competing threads. It is proved here, however, that every competing thread is overtaken less than N times, and that the overtaking threads were competing when the first one of them exits.     

A mutual exclusion algorithm with optimally bounded bypasses

Peterson's algorithm [G.L. Peterson, Myths about the mutual exclusion problem, Inform. Process. Lett. 12 (3) (1981) 115-116] for mutual exclusion has been widely studied for its elegance and simplicity. In Peterson's algorithm, each process has to cross n−1 stages to access the shared resource irrespective of the contention for the shared resource at that time, and allows unbounded bypasses. In [K. Block, T.-K. Woo, A more efficient generalization of Peterson's mutual exclusion algorithm, Inform. Process. Lett. 35 (1990) 219-222], Block and Woo proposed a modified algorithm that transforms the number stages to be crossed from fixed n−1 to t, where 1?t?n, and bounds the number of possible bypasses by n(n−1)/2. This paper proposes a simple modification that reduces the bound on the number of possible bypasses to optimal n−1.     

Space-efficient FCFS group mutual exclusion

In the group mutual exclusion problem [Y. Joung, Asynchronous group mutual exclusion, Distrib. Comput. 13 (2000) 189], which generalizes mutual exclusion [E. Dijkstra, Solution of a problem in concurrent programming control, Comm. ACM 8 (9) (1965) 569], a process chooses a session when it requests entry into the Critical Section. A group mutual exclusion algorithm must ensure that the mutual exclusion property holds: if two processes are in the Critical Section at the same time, then they request the same session. In addition to mutual exclusion, lockout freedom, bounded exit, and concurrent entering are basic properties that are desirable in any group mutual exclusion algorithm.Hadzilacos in [Proc. 20th Annual Symp. on Principles of Distributed Computing, 2001, pp. 100-106] first introduced a fairness condition, called first-come-first-served (FCFS), for group mutual exclusion. The only known FCFS group mutual exclusion algorithm is due to Hadzilacos [Proc. 20th Annual Symp. on Principles of Distributed Computing, 2001, pp. 100-106], and requires Θ(N²) bounded shared registers, where N is the number of processes. We present a FCFS group mutual exclusion algorithm that uses only Θ(N) bounded shared registers. (The existence of such an algorithm was posed as an open problem by Hadzilacos.)     

Adaptive and efficient mutual exclusion

Summary. This paper presents adaptive algorithms for mutual exclusion using only read and write operations; the performance of the algorithms depends only on the point contention, i.e., the number of processes that are concurrently active during the algorithm execution (and not on n, the total number of processes). Our algorithm has O(k) remote step complexity and O(logk) system response time, wherek is the point contention. The remote step complexity is the maximal number of steps performed by a process where a wait is counted as one step. The system response time is the time interval between subsequent entries to the critical section, where one time unit is the minimal interval in which every active process performs at least one step. The space complexity of this algorithm is O(N logn), where N is the range of processes' names. We show how to make the space complexity of our algorithm depend solely on n, while preserving the other performance measures of the algorithm. Received: March 2001 / Accepted: November 2001     

Long-distance mutual exclusion for planning

Mutual exclusion (mutex) is a powerful mechanism for search space pruning in planning. However, a serious limitation of mutex is that it cannot specify constraints relating actions and facts across different time steps. In this paper, we propose a new class of mutual exclusions that significantly generalizes mutex and can be efficiently computed. The proposed long-distance mutual exclusion (londex) can capture constraints over actions and facts not only at the same time step but also across multiple steps. As a generalization, londex is much stronger than mutex, and provides a general and effective tool for developing efficient planners.We propose two levels of londex. The first level, londex₁, is derived from individual domain transition graphs (DTGs), and the second level, londex_m, is derived from multiple DTGs by taking into account the interactions among them. Londex constraints provide stronger pruning power but also require a large amount of memory. To address the memory problem, we further develop a virtual realization mechanism in which only a small proportion of londex constraints are dynamically generated as needed during the search. This scheme can save a huge amount of memory without sacrificing the pruning power of londex.For evaluation purposes, we incorporate londex into SATPlan04 and SATPlan06, two efficient SAT-based planners. Our experimental results show that londex_m can significantly improve over londex₁ since the former exploits causal dependencies among DTGs. Our experimental results for various planning domains also show significant advantages of using londex constraints for reducing planning time.     

Verifying mutual exclusion and liveness properties with split preconditions

This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson‘s distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness,and lockout-freedom have also been presented.     

Quorum-based algorithms for group mutual exclusion

We propose a quorum system, which we referred to as the surficial quorum system, for group mutual exclusion. The surficial quorum system is geometrically evident and is easy to construct. It also has a nice structure based on which a truly distributed algorithm for group mutual exclusion can be obtained and processed loads can be minimized. When used with Maekawa's algorithm, the surficial quorum system allows up to /spl radic/2n/m(m-l) processes to access a resource simultaneously, where n is the total number of processes and m is the total number of groups. We also present two modifications of Maekawa's algorithm so that the number of processes that can access a resource at a time is not limited to the structure of the underlying quorum system, but to the number that the problem definition allows.     

A fair distributed mutual exclusion algorithm

This paper presents a fair decentralized mutual exclusion algorithm for distributed systems in which processes communicate by asynchronous message passing. The algorithm requires between N-1 and 2(N-1) messages per critical section access, where N is the number of processes in the system. The exact message complexity can be expressed as a deterministic function of concurrency in the computation. The algorithm does not introduce any other overheads over Lamport's and Ricart-Agrawala's algorithms, which require 3(N-1) and 2(N-1) messages, respectively, per critical section access and are the only other decentralized algorithms that allow mutual exclusion access in the order of the timestamps of requests     

A queue based mutual exclusion algorithm

A new elegant and simple algorithm for mutual exclusion of N processes is proposed. It only requires shared variables in a memory model where shared variables need not be accessed atomically. We prove mutual exclusion by reformulating the algorithm as a transition system (automaton), and applying simulation of automata. The proof has been verified with the higher-order interactive theorem prover PVS. Under an additional atomicity assumption, the algorithm is starvation free, and we conjecture that no competing process is passed by any other process more than once. This conjecture was verified by model checking for systems with at most five processes.     

互斥协议的安全性分析

安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。