One of the long-standing research problems on logic programming is to treat the cut predicate in a logical, high-level way. We argue that this problem can be solved by adopting linear logic and choice-disjunctive goal formulas of the form G0 ⊕ G1 where G0, G1 are goals. These goals have the following intended semantics: choose the true disjunct Gi and execute Gi where i (= 0 or 1), while discarding the unchosen disjunct. Note that only one goal can remain alive during execution. These goals thus allow us to specify mutually exclusive tasks in a high-level way. Note that there is another use of cut which is for breaking out of failure-driven loops and efficient heap management. Unfortunately, it is not possible to replace cut of this kind with use of choice-disjunctive goals.

Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol*.

This paper presents a novel method for optimal control of timed Petri nets, introducing a novel temporal logic based constraint called a generalized mutual exclusion temporal constraint (GMETC). The GMETC is described by a metric temporal logic (MTL) formula where each atomic proposition represents a generalized mutual exclusion constraint (GMEC). We formulate an optimal control problem of the timed Petri nets under a given GMETC and solve the problem by transforming it into an integer linear programming problem where the MTL formula is encoded by linear inequalities. We show the effectiveness of the proposed approach by a numerical simulation.

Petri Net (PN) is a frequently-used model for deadlock detection. Among various detection methods on PN, reachability analysis is the most accurate one since it never produces any false positive or false negative. Although suffering from the well-known state space explosion problem, reachability analysis is appropriate for small- and medium-scale programs. In order to mitigate the explosion problem several kinds of techniques have been proposed aiming at accelerating the reachability analysis, such as net reduction and abstraction. However, these techniques are for general PN and do not take the particularity of application into consideration, so their optimization potential is not adequately developed. In this paper, the feature of mutual exclusion-based program is considered, therefore several strategies are proposed to accelerate the reachability analysis. Among these strategies a customized net reduction rule aims at reducing the scale of PN, two marking compression methods and two pruning methods can reduce the volume of reachability graph. Reachability analysis on PN can only report one deadlock on each path. However, the reported deadlock may be a false alarm in which situation real deadlocks may be hidden. To improve the detection efficiency, we proposed a deadlock recovery algorithm so that more deadlocks can be detected in a shorter time. To validate the efficiency of these methods, a prototype is implemented and applied to SPLASH2 benchmarks. The experimental results show that these methods accelerate the reachability analysis for mutual exclusion-based deadlock detection significantly.

Multiple-way (N-way) asynchronous arbitration is an important issue in asynchronous system design. In this paper, novel implementation methods of N-way asynchronous arbiters are presented. We first present N-way rectangle mesh arbiters using 2-way mutual exclusion elements. Then, N-way token-ring arbiters based on the non-return-to-zero signaling is also presented. The former can issue grant signals with the same percentage for all the arriving request signals while the latency is proportional to the number of inputs. The latter can achieve low latency and low energy arbitration for a heavy workload environment and a large number of inputs. In this paper, we compare their performances using the 28nm FD-SOI process technologies qualitatively and quantitatively.

Group mutual exclusion is an interesting generalization of the mutual exclusion problem. This problem was introduced by Joung, and some algorithms for the problem have been proposed by incorporating mutual exclusion algorithms. Group mutual exclusion occurs naturally in a situation where a resource can be shared by processes of the same group, but not by processes of a different group. It is also called the congenial talking philosophers problem. In this paper we propose two algorithms based on ticket orders for the group mutual exclusion problem on the asynchronous shared memory model. These algorithms are some modifications of the Bakery algorithm. They satisfy lockout freedom and a high degree of concurrency performance. Each of these algorithms uses single-writer shared variables together with two multi-writer shared variables that are never concurrently written. One of these algorithms has another desirable property, called smooth admission. By this property, during the period that the resource is occupied by the leader (called the chair), a process wishing to join the same group as the leader's group can be granted use of the resource in constant time.

We propose two simple algorithms based on bounded tickets for the mutual exclusion problem on the asynchronous single-writer/multi-reader shared memory model. These algorithms are modifications of the Bakery algorithm. An unattractive property of the Bakery algorithm is that the size of its shared memory is unbounded. Initially we design a provisional algorithm based on bounded tickets. It guarantees mutual exclusion in the case where a certain condition is satisfied. To remove the condition, we use an additional process that does not correspond to any user. The algorithm with the additional process is a lockout-free mutual exclusion algorithm on the asynchronous single-writer/multi-reader shared memory model. We then modify this algorithm to reduce the shared memory size with the cost of using another additional process. The maximum waiting time using each of the algorithms proposed in this paper is bounded by (n-1)c+O(nl), where n is the number of users, l is an upper bound on the time between two successive atomic steps, and c is an upper bound on the time that any user spends using the resource. The shared memory size needed by the first algorithm and the second algorithm are (n+1)(1+log (4n)) bits and n(1+log (4n-4))+2 bits, respectively.

Most conventional studies on self-stabilization have been indifferent to the vulnerability under convergence. This paper investigates how mutual exclusion property can be achieved in self-stabilizing rings even for illegitimate configurations. We present a new method which uses a state with a large state space to detect faults. If some faults are detected, every process is reset and not given a privilege. Even if the reset values are different between processes, our protocol mimics the behavior of Dijkstra's unidirectional K-state protocol. Then we have a fast and safe mutual exclusion protocol. Simulation study also examines its performance.

The mobile computing system is a set of functions on a distributed environment organized to support mobile hosts. In this environment, mobile hosts should be able to move without any constraints and should remain connected to the network even while moving. Also, they should be able to get necessary information regardless of their current location and time. Distributed mutual exclusion methods for supporting distributed algorithms have hitherto been designed for networks only with static hosts. However, with the emergence of mobile computing environments, a new distributed mutual exclusion method needs to be developed for integrating mobile hosts with underlying distributed systems. In the sense, many issues that should be considered stem from three essential properties of mobile computing system such as wireless communication, portability, and mobility. Thus far, distributed mutual exclusion methods for mobile computing environments were designed based on a token ring structure, which has the drawback of requiring high costs in order to locate mobile hosts. In this paper, we propose not only a distributed mutual exclusion method that can reduce such costs by structuring the entire system as a tree-based logical structure but also recovery schemes that can be applied when a node failure occurs. Finally, we evaluate the operation costs for the mutual exclusion scheme and the recovery scheme.

The k-mutual exclusion problem is the problem of guaranteeing that no more than k computing nodes enter a critical section simultaneously. The use of a k-coterie, which is a special set of node groups, is known as a robust approach to this problem. In general, k-coteries are classified as either dominated or nondominated, and a mutual exclusion mechanism has maximal availability when it employs a nondominated k-coterie. In this paper, we propose two new schemes called VOT and D-VOT for constructing nondominated k-coteries. We conduct a comparative evaluation of the proposed schemes and well-known previous schemes. The results clearly show the superiority of the proposed schemes.

A coterie is a set of quorums such that any two quorums intersect each other, and is used in a quorum based algorithm for solving the mutual exclusion problem. The availability of a coterie is the probability that the algorithm (adopting the coterie) tolerates process and/or link failures. Constructing an optimal coterie in terms of the availability is therefore important from the view of fault tolerance, but unfortunately, even calculating the availability is known to be #P-hard. Recently Harada and Yamashita proposed several heuristic methods for improving the availability of a coterie. This letter first evaluates their performance and then proposes a practical method for constructing a semi-optimal coterie by using one of the heuristic methods as a main component.

We propose two lockout-free (starvation-free) mutual exclusion algorithms for the asynchronous multi-writer/reader shared memory model. The first algorithm is a modification of the well-known tournament algorithm for the mutual exclusion problem. By the modification we can speed up the original algorithm. The running time of the modified algorithm from the entrance of the trying region to the entrance of the critical region is at most (n-1)c+O(nl), where n is the number of processes, l is an upper bound on the time between successive two steps of each process, and c is is an upper bound on the time that any user spends in the critical region. The second algorithm is a further modification of the first algorithm. It is designed so that some processes have an advantage of access to the resource over other processes.

This paper proposes a mutual exclusion method that is unified for the parallel and distributed systems. The method partially serializes requests into partial queues of requests, which are next totally serialized into a main queue. A request in the main queue is authorized to enter the critical section (CS) when the request receives the privilege token from the previous request in the queue. In the distributed system of N sites that each is a parallel system, mutual exclusion is performed by cooperation of two algorithms based on the same method. The algorithm for the distributed system works on a logical network (that is a directed tree) of S ( N) sites. The algorithm for each site produces a local-main queue of requests. The chunk of requests in the local queue is concatenated at a time to the partial queue of the distributed system. The the cost of mutual exclusion -- the number of intersite messages required per CS entry -- is reduced to O(1) (between 0 and 3).

We discuss properties of acyclic graph evolution driven by node-firing. The research background and basic concepts of acyclic graph evolution are from the mutual exclusion problem in distributed environments. We proposed in our previous work a mutual exclusion protocol which is based on the notion of evolution trajectories of acyclic graphs. In this paper, we analyze firing concurrency and periodicity of the acyclic graph evolution, from graph theoretical point of views, and investigate topological conditions for assuring the number of firable nodes below a some fixed constant, at any instance of the evolution trajectory. A marked graph, a subclass of Petri nets, is often utilized as a proof tool in analysis.

With advances in the speed, bandwidth and reliability of telecommunications networks and in the performance of workstations, distributed processing has become widespread. Information sharing among distributed nodes and its mutual exclusion are of great importance for efficient distributed processing. This paper systematizes and quantitizes a shared memory called Data-Cyclic Shared Memory (DCSM) from the viewpoints of memory organization and access mode. In DCSM, the propagation delay of transmission lines and the data relaying delay in each node are used for information storage, and memory information encapsuled in the form of "memory cells" circulates infinitely in a logical ring type network. The distinctive feature of DCSM, in addition to the way data is stored, is that data and the access control are completely distributed, which contrasts with existing memory where both are centralized. Therefore, there are no performance bottlenecks caused by concentrating memory access. Distributed Shared Memory (DSM), which has a scheme similar to DCSM's, has also been proposed for distributed environments. In DSM, the data is also distributed but the control for accessing each data is centralized. From the viewpoints of memory organization and the access method, DCSM is very flexible. For instance, word length can be spatially varied by defining data size at each address, and each node can be equipped with mechanisms for special functions such as the content address specification and asynchronous report of change in contents. Because of this flexibility, it can be called a "software-defined memory." The analysis also reveals that DCSM has the disadvantages of large access delay and small memory capacity. The capacity can be enlarged by inserting FIFO type queues into the circulation network, and the delay can be shortened by circulating replicas of original memory cells. However, there is a trade off between the maximal capacity and the mean access time. DCSM has many potential applications, such as in the mutual exclusion control of distributed resources.

This paper treats mutual exclusion of a single shared-resource in distributed autonomous environments. The most important property of the autonomous network treated in this paper is its membership variability, that is, frequent occurrence of entries of new nodes and exits of old nodes. Thus, when the network is large-scale, it is not possible for each node to keet up the information of all other nodes. We in this paper design a mutual exclusion algorithm for distributed environments of autonomous nodes based on Chandy-Misra protocol for Dining Philosopher (diners) problems, which realizes a distributed implementation of the token ring method. We consider requirements of the communication topology that makes mutual exclusion possible, and propose entry and exit protocols for each node to perform them individualistically and autonomously.

This paper presents a destributed algorithm that uses weak copy consistency to create mutual exclusion in a distributed computer system. The weak copy consistency is deduced from the uncertainty of state which occurs due to the finite and unpredictable communication delays in a distributed environment. Also the method correlates outdated state information to current state. The average number of messages to enter critical section in the algorithm is n/2 to n messages where n is the number of sites. We show that the algorithm achieves mutual exclusion and the fairness and liveness of the algorithm is proven. We study the performance of the algorithm by simulation technique.