Temporal logic-based deadlock analysis for Ada

A temporal logic-based specification language and deadlock analyzer for Ada is described. The deadlock analyzer is intended for use within Timebench, a concurrent system-design environment with support for Ada. The specification language, COL, uses linear-time temporal logic to provide a formal basis for axiomatic reasoning. The deadlock analysis tool uses the reasoning power of COL to demonstrate that Ada designs specified in COL are systemwide deadlock-free: in essence, it uses a specialized theorem prover to deduce the absence of deadlock. The deadlock algorithm is shown to be decidable for finite systems and acceptable otherwise. It is also shown to have a worst-case computational complexity that is exponential with the number of tasks. The analyzer has been implemented in Prolog. Numerous examples are evaluated using the analyzer, including readers and writers, gas station, five dining philosophers, and a layered communications system. The results indicate that analysis time is reasonable for moderate designs in spite of the worst-case complexity of the algorithm     

Syntactic reductions for efficient deadlock analysis

A well‐known problem in the verification of concurrent systems based on model checking is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. A reduction technique to reduce state explosion in deadlock checking is presented. The method is based on an automatic syntactic simplification of a calculus of communicating systems (CCS) specification, which keeps the parts of the program structure that may lead to a deadlock and deletes the other parts. Copyright © 2002 John Wiley & Sons, Ltd.     

Efficient deadlock analysis of component-based software architectures

Component-based development (CBD) is a promising approach to master the design complexity of huge software products. In addition, knowledge about the architecture of such component systems can help in establishing important system properties, which in general is computationally hard because of the state space explosion problem. Extending previous work, we here investigate the novel class of disjoint circular wait free component systems and show how we can use the architectural information to establish a condition for the property of deadlock-freedom in polynomial time. Furthermore, we emphasize the importance of this class by showing how to transform an arbitrary system into a disjoint circular wait free one in linear time and in a property preserving way and by providing various computational complexity results. A running example is included. We use the framework of interaction systems, but our results carry over to other CBD models.     

Performance analysis of distributed deadlock detection algorithms

The paper presents a probabilistic performance analysis of a deadlock detection algorithm in distributed systems. Although there has been extensive study on deadlock detection algorithms in distributed systems, little attention has been paid to the study of the performance of these algorithms. Most work on performance study has been achieved through simulation but not through an analytic model. Min (1990), to the best of our knowledge, made the sole attempt to evaluate the performance of distributed deadlock detection algorithms analytically. Being different from Min's, our analytic approach takes the time-dependent behavior of each process into consideration rather than simply taking the mean-value estimation. Furthermore, the relation among the times when deadlocked processes become blocked is studied, which enhances the accuracy of the analysis. We measure performance metrics such as duration of deadlock, the number of algorithm invocations, and the mean waiting time of a blocked process. It is shown that the analytic estimates are nearly consistent with simulation results     

Symbolic object code analysis

Software model checkers quickly reach their limits when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This article introduces a novel technique for checking pointer safety violations, called symbolic object code analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Extensive experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to modern source-code model checkers, scales well when applied to real operating systems code and pointer safety issues, and effectively explores niches of pointer-complex software that current software verifiers do not reach.     

An admissible-behaviour-based analysis of the deadlock in Petri-net controllers

This paper addresses the problem of verifying the discrete control logic that is typically implemented by programmable controllers. Not only are the logical properties of the controller studied during verification, the behaviour of the overall controlled system is also examined. An approach that combines the calculation of the safety-oriented interlock controllers in terms of supervisory control theory (SCT), the corresponding calculation of the admissible behaviour of the system, and the specification of the desired system operation by Petri nets is proposed. A potential deadlock in the controlled system is then verified by taking the admissible-behaviour model as a process model. The analysis of the simultaneously operated supervisory-control-based interlock controller and the Petri-net-based sequential controller is performed with a C-reachability graph. The paper focuses on the calculation of the graph, and the approach is illustrated with an example of a simple manufacturing cell.     

State space reduction by non-standard semantics for deadlock analysis

In recent years many techniques have been developed for automatically verifying concurrent systems and most of them are based on the representation of the concurrent system by means of a transition system. State explosion is one of the most serious problems of this approach: often the prohibitive number of states renders the verification inefficient and, in some cases, impossible.

We propose a method for reducing the state space of the transition system corresponding to a CCS process that suites deadlock analysis. The reduced transition system is generated by means of a non-standard operational semantics containing a set of rules which are, in some sense, an abstraction, preserving deadlock freeness, of the inference rules of the standard semantics. Our method does not build the standard transition system, but directly generates an abstract system with a fewer number of states, so saving memory space. We characterize a class of processes whose abstract transition system is not exponential in the number of parallel components.     

Symbolic analysis via semantic reinterpretation

The paper presents a novel technique to create implementations of the basic primitives used in symbolic program analysis: forward symbolic evaluation, weakest liberal precondition, and symbolic composition. We used the technique to create a system in which, for the cost of writing just one specification—an interpreter for the programming language of interest—one obtains automatically generated, mutually-consistent implementations of all three symbolic-analysis primitives. This can be carried out even for languages with pointers and address arithmetic. Our implementation has been used to generate symbolic-analysis primitives for the x86 and PowerPC instruction sets.     

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     

Symbolic analysis of linear polyhedra

This paper concerns several analytical problems related to linear polyhedra in euclidean three-dimensional-space. Symbolic formulas for line, surface, and volume integration are given, and it is shown that domain integrals are computable in polynomial time. In particular, it is shown that mass, first and second moments, and products of inertia are computable inO(E) time, whereE is the number of edges of the boundary. Simple symbolic expressions for the normal derivatives of domain integrals are also derived. In particular, it is shown that they are closely linked to the topology of the integration domain, as well as that they are expressible as combinations of domain integrals over lower-order domains (faces, edges, and vertices). The symbolic results presented in this paper may lead to an easy incorporation of integral constraints, for example, concerning mass and inertia, in the engineering designing process of solid objects.     

A generalized deadlock predicate

Satisfiability of the deadlock predicate constructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. Clarke (1980) has developed a technique, based on a view of resource invariants as fixed points of a functional, for constructing a deadlock predicate such that satisfiability is a necessary and sufficient condition for total deadlock. We describe a technique for synthesizing a generalized deadlock predicate such that satisfiability is a necessary and sufficient condition for both total and partial deadlock. Our method constructs a strongest resource invariant using Clarke's fixed point functional. We then use this strongest resource invariant and a predicate transformer to construct a generalized deadlock predicate.     

Symbolic predictive analysis for concurrent programs

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.     

Approximate analysis of product-form type queueing networks with blocking and deadlock

A numerical procedure for analyzing exactly closed exponential queueing networks with finite queues is presented first. Due to the finiteness of these queues, blocking and deadlock may occur. Deadlocks are assumed to be detected and resolved instantaneously. The numerical procedure is then incorporated in an approximation algorithm for analyzing closed exponential queueing networks of the product-form type, in which some of the queues are finite. These finite queues are assumed to be linked together to form a single subnetwork. The approximation algorithm is based on a variant of Norton's theorem. Comparisons between the approximate results and exact numerical results were carried out and the relative error was observed to be small.     

A comparative performance analysis of deadlock avoidance control algorithms for FMS

A deadlock condition for flexible manufacturing systems is characterized by a set of parts, which have been processed but cannot be discharged by a set of machines or buffers. To avoid such problems, it is necessary to adopt suitable control policies which limit the resource allocation in the system, thus affecting the overall system performance. In the present work, we address the problem of evaluating and comparing the performance of deadlock avoidance control policies applied to FMS. The problem is discussed for both untimed and timed models, and for models both with and without deadlock avoidance control policies. Different control algorithms, among the most common in the literature, have been considered. Imperfect deadlock avoidance control policies are also considered. In addition, some indices are proposed to assess the structural properties of FMS with respect to deadlock occurrence and their performance. Two different application examples are analyzed, with the help of a commercial simulation package. Finally, an adaptive algorithm which can learn from system evolution to avoid deadlocks is illustrated.     

Petri net modeling and deadlock analysis of parallel manufacturing processes with shared-resources

Multiple resource-sharing is a common situation in parallel and complex manufacturing processes and may lead to deadlock states. To alleviate this issue, this paper presents the method of modeling parallel processing flows, sharing limited number of resources, in flexible manufacturing systems (FMSs). A new class of Petri net called parallel process net with resources (PPNRs) is introduced for modeling such FMSs. PPNRs have the capacity to model the more complex resource-sharing among parallel manufacturing processes. Furthermore, this paper presents the simple diagnostic and remedial procedures for deadlocks in PPNRs. The proposed technique for deadlock detection and recovery is based on transition vectors which have the power of determining the structural aspects as well as the process flow condition in PPNRs. Moreover, the proposed technique for dealing with deadlocks is not a siphon-based thus the large-scale PPNRs for real-life FMSs can be tackled. Finally, the proposed method of modeling and deadlock analysis in the FMS having parallel processing is demonstrated by a practical example.     

密码协议的符号模型检测及分析

对密码协议模型检测的方法作了理论上的研究,并用SMV检测工具给出了一个实际分析的例子。结果表明,利用符号模型检测方法分析并发现密码协议重放攻击的漏洞是一种行之有效的方法。     

Symbolic data analysis tools for recommendation systems

Recommender systems have become an important tool to cope with the information overload problem by acquiring data about user behavior. After tracing the user’s behavior, through actions or rates, computational recommender systems use information- filtering techniques to recommend items. In order to recommend new items, one of the three major approaches is generally adopted: content-based filtering, collaborative filtering, or hybrid filtering. This paper presents three information-filtering methods, each of them based on one of these approaches. In our methods, the user profile is built up through symbolic data structures and the user and item correlations are computed through dissimilarity functions adapted from the symbolic data analysis (SDA) domain. The use of SDA tools has improved the performance of recommender systems, particularly concerning the find good items task measured by the half-life utility metric, when there is not much information about the user.     

Fifo nets without order deadlock

Summary We introduce a generalisation of free choice nets to fifo. These fifo nets are free from deadlocks caused by the order of messages in fifo queues. We describe some tools for their analysis, using the fact that they are weakly monotonous, and that there is a narrow relation between their languages and those of the associated coloured nets. Therefore, quasi-liveness, finite termination and liveness are decidable properties.     

Fifo nets without order deadlock

Summary We introduce a generalisation of free choice nets to fifo. These fifo nets are free from deadlocks caused by the order of messages in fifo queues. We describe some tools for their analysis, using the fact that they are weakly monotonous, and that there is a narrow relation between their languages and those of the associated coloured nets. Therefore, quasi-liveness, finite termination and liveness are decidable properties.