A decentralized deadlock detection and resolution algorithm for generalized model in distributed systems

We propose a new distributed algorithm for detecting generalized deadlocks in distributed systems. It records the consistent snapshot of distributed Wait-For Graph (WFG) through propagating the probe messages along the edges of WFG. It then reduces the snapshot by eliminating the unblocked processes to determine the set of deadlocked processes. However, the reducibility of each blocked process is arbitrarily delayed until a node collects the replies in response to all probes, unlike the earlier algorithms. We also prove the correctness of the proposed algorithm. It has a worst-case time complexity of 2d time units and the message complexity of 2e, where d is the diameter and e is the number of edges of the WFG. The significant improvement of proposed algorithm over other algorithms is that it reduces the data traffic complexity into constant by using fixed sized messages. Furthermore, it minimizes additional messages to resolve deadlocks.     

A partially distributed deadlock detection algorithm

In this paper, a partially distributed deadlock detection algorithm [PDDDA] with multiple outstanding requests is presented for use in distributed database systems. This algorithm allows a process to request many resources simultaneously and uses a central controller for detecting multisite deadlocks. The detection of local deadlocks and the maintenance of local deadlock information are performed at each of the local sites. This partially distributed algorithm alleviates the problem of congestion at the central controller in a centralized algorithm and needs fewer messages and smaller storage space than a fully decentralized algorithm. A set of criteria for comparing deadlock detection algorithms are also given and then used to compare PDDDA with a fully decentralized algorithm proposed by Isloor and Marsland.Research reported herein was supported by US Army CECOM, Ft. Monmouth, New Jersey, under Contract No. DAAB07-83-K-K542. The views, opinions, and/or findings contained in this paper are those of the authors and should not be construed as an official Deportment of the Army position, policy or decision.     

A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.     

A trace-based service semantics guaranteeing deadlock freedom

We revise the accordance preorder in the context of deadlock freedom for asynchronously communicating services. Accordance considers all controllers of a service—that is, all environments that can interact with the service without deadlocking. A service Impl accords with a service Spec if every controller of Spec is also a controller of Impl. We model finite-state and infinite-state services as Petri nets and formalize the semantics of such models with a traditional concurrency semantics, a trace-based semantics. As benefits, we get an easier characterization of the accordance preorder, prove that it is a fully abstract precongruence, and present an algorithm to decide refinement of two finite-state services. Previously, operating guidelines have been introduced to study the behavior of finite-state services; they characterize all controllers of a given service and can be used to decide accordance. An operating guideline is a finite automaton annotated with Boolean formulae that describes the semantics of a service from the perspective of its controllers rather than from the perspective of the service. We show that our trace-based semantics can be translated back and forth into operating guidelines, thereby providing a more conceptual understanding of operating guidelines.     

A specification technique based on predicate transformers

Summary This paper proposes a formal specification technique based on the notion of predicate transformers. Several approaches to showing the completeness are investigated. A method for proving the correctness of an implementation with respect to a formal specification is described.The work presented in this paper was performed while the author was with the University of Hamburg, Germany     

Distributed deadlock detection

We describe a simple and efficient algorithm to detect deadlocks in distributed systems. In our model, processes requestN resources from a pool of sizeM. This is a generalization of the well-knownAND-OR request model. The algorithm is incrementally derived and proven correct. Its communication, computational, and space requirements are lower than those of the best previously known algorithms for the simplerAND-OR model.Gabriel Bracha received his B.Sc. Degree in Mathematics (Computer Science option) from Tel-Aviv University, Israel, in 1980, and his Ph.D. degree in Computer Science from Cornell University, Ithaca, NY, in 1985.In 1985, he joined Daisy System, in Tel-Aviv, Israel, where he is currently a Senior Researcher His current research interests include computational geometry, distributed computing, and fault-tolerance.Partial support for this work was provided by the National Science Foundation under grant MCS 83-03135For photograph and biography see Distributed Computing (1987) 2:80–94     

A deadlock detection tool for concurrent Java programs

This paper presents some issues related to the design and implementation of a concurrency analysis tool able to detect deadlock situations in Java programs that make use of multithreading mechanisms. An abstract formal model is generated from the Java source using the Java2Spin translator. The model is expressed in the PROMELA language, and the SPIN tool is used to perform its formal analysis. The paper mainly focuses on the design of the Java2Spin translator. A set of experiments, carried out to evaluate the performances of the analysis tool, is also presented. Copyright © 1999 John Wiley & Sons, Ltd.     

A VLSI structure for the deadlock avoidance problem

In this paper we present two VLSI structures implementing the banker's algorithm for the deadlock avoidance problem, and we derive the area x (time)² lower bound for such an algorithm. The first structure is based on the VLSI mesh of trees. The second structure is a modification of the first one, and it approaches more closely the theoretical lower bound.     

A methodology for constructing predicate transition net specifications

In this paper, a methodology for constructing hierarchical and structured predicate transition net specifications is developed, which includes new systematic notation extensions for supporting various transformation techniques upon predicate transition nets and several rules for applying such transformation techniques. The levelling technique in data-flow diagrams is adapted in the refinement and the abstraction techniques, and the state decomposition idea in state-charts is employed in designing various label formulation operators. The methodology is illustrated through the specification of a lift system. The methodology can significantly reduce the constructing complexity and enhance the comprehensibility of large predicate transition net specifications.     

Symbolic modular deadlock analysis

Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in an unsafe manner. This is frequently a cause of deadlocks. Given a concurrent library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments. In this work, we focus on deriving contracts that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding scheme for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signaling primitives such as wait-notify for cooperative synchronization. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of client code.     

A cost-effective approach to deadlock handling in wormhole networks

Wormhole networks have traditionally used deadlock avoidance strategies. More recently, deadlock recovery strategies have begun to gain acceptance. In particular, progressive deadlock recovery techniques allocate a few dedicated resources to quickly deliver deadlocked packets. Deadlock recovery is based on the assumption that deadlocks are rare; otherwise, recovery techniques are not efficient. Measurements of deadlock occurrence frequency show that deadlocks are highly unlikely when enough routing freedom is provided. However, networks are more prone to deadlocks when the network is close to or beyond saturation, causing some network performance degradation. Similar performance degradation behavior at saturation was also observed in networks using deadlock avoidance strategies. In this paper, we take a different approach to handling deadlocks and performance degradation. We propose the use of an injection limitation mechanism that prevents performance degradation near the saturation point and, at the same time, reduces the probability of deadlock to negligible values. We also propose an improved deadlock detection mechanism that uses only local information, detects all deadlocks, and considerably reduces the probability of false deadlock detection over previous proposals. In the rare case when impending deadlock is detected, our proposal consists of using a simple recovery technique that absorbs the deadlocked message at the current node and later reinjects it for continued routing toward its destination. Performance evaluation results show that our new approach to handling deadlock is more efficient than previously proposed techniques     

A deadlock detection interface to a commercial simulation language

In this research, issues related to deadlock detection in discrete event simulation models and the feasibility of interfacing a deadlock detection algorithm to a commercial simulation language have been explored. For the purpose of this research, a deadlock detection algorithm has been designed, developed and interfaced to the SIMAN commercial simulation language. Both the algorithm and the interface have been validated using a set of sample scenarios. The details of the deadlock detection algorithm, the interface to the chosen commercial simulation language and the validation scenarios are discussed in this paper, along with the lessons learned and recommendations for future enhancements.     

A distributed deadlock resolution algorithm for the AND model

Previous proposals for Distributed Deadlock Detection/Resolution algorithms for the AND model have the main disadvantage of resolving false deadlocks, that is, nonexisting or currently being resolved deadlocks. This paper provides an algorithm free of false deadlock resolutions, A simple specification for a safe deadlock resolution algorithm is introduced, and the new distributed solution is developed in a hierarchical fashion from its abstract specification. The algorithm is probe-based, uses node priorities, and coordinates the actions of resolvers so that false deadlocks are not resolved. The solution is formally proven correct by using the input-output Automata Model. Finally, a study about the liveness of the algorithm is provided     

A general theory for deadlock avoidance in wormhole-routed networks

Most machines of the last generation of distributed memory parallel computers possess specific routers which are used to exchange messages between nonneighboring nodes in the network. Among the several technologies, wormhole routing is usually preferred because it allows low channel-setup time and reduces the dependency between latency and internode distance. However, wormhole routing is very susceptible to deadlock because messages are allowed to hold many resources while requesting others. Therefore, designing deadlock-free routing algorithms using few hardware facilities is a major problem for wormhole-routed networks. In this paper, we describe a general theoretical framework for the study of deadlock-free routing functions. We give a general definition of what can be a routing function. This definition captures many specific definitions of the literature (e.g., vertex dependent, input-dependent, source-dependent, path-dependent etc.). Using our definition, we give a necessary and sufficient condition which characterizes deadlock-free routing functions. Our theory embraces, at a high level, most of the theories related to deadlock avoidance in wormhole-routed networks previously derived in the literature. In particular, it applies not only to one-to-one routing, but also to one-to-many routing. The latter paradigm is used to solve the multicast problem with the path-based or tree-based facility     

A deadlock avoidance approach for nonsequential resource allocation systems

The paper concentrates on the deadlock-avoidance problem for a class of resource allocation systems modeling manufacturing systems. In these systems, a set of production orders have to be executed in a concurrent way. To be executed, each step of each production order needs a set of reusable system resources. The competition for the use of these resources can lead to deadlock problems. Many solutions, from different perspectives, can be found in the literature for deadlock-related problems when the production orders have a sequential nature [sequential resource allocation systems (S-RAS)]. However, in the case in which the involved processes have a nonsequential nature [nonsequential resource allocation systems (NS-RAS)], the problem becomes more complex. In this paper, we propose a deadlock avoidance algorithm for this last class of systems. We also show the usefulness of the proposed solution by means of its application to a real system.     

A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.     

A decision procedure for common Lisp''sSUBTYPEP predicate

Common Lisp [25],[26] includes a dynamic datatype system of moderate complexity, as well as predicates for checking the types of language objects. Additionally, an interesting predicate of two type specifiers—SUBTYPEP—is included in the language. Thissubtypep predicate provides a mechanism with which to query the Common Lisp type system regarding containment relations among the various built-in and user-defined types. Whilesubtypep is rarely needed by an applications programmer, the efficiency of a Common Lisp implementation can depend critically upon the quality of itssubtypep predicate: the run-time system typically calls uponsubtypep to decide what sort of representations to use when making arrays; the compiler calls uponsubtypep to interpret userdeclarations, on which efficient data representation and code generation decisions are based.As might be expected due to the complexity of the Common Lisp type system, there may be type containment questions which cannot be decided. In these casessubtypep is expected to return can't determine, in order to avoid giving an incorrect answer. Unfortunately, most Common Lisp implementations have abused this license by answering can't determine in all but the most trivial cases.In particular, most Common Lisp implementations of SUBTYPEP fail on the basic axioms of the Common Lisp type system itself [25][26]. This situation is particularly embarrassing for Lisp-the premier symbol processing language—in which the implementation of complex symbolic logical operations should be relatively easy. Sincesubtypep was presumably included in Common Lisp to answer thehard cases of type containment, this lazy evaluation limits the usefulness of an important language feature.