In this paper, we discuss the feasibility of monitoring partially synchronous distributed systems to detect latent bugs, i.e., errors caused by concurrency and race conditions among concurrent processes. We present a monitoring framework where we model both system constraints and latent bugs as Satisfiability Modulo Theories (SMT) formulas, and we detect the presence of latent bugs using an SMT solver. We demonstrate the feasibility of our framework using both synthetic applications where latent bugs occur at any time with random probability and an application involving exclusive access to a shared resource with a subtle timing bug. We illustrate how the time required for verification is affected by parameters such as communication frequency, latency, and clock skew. Our results show that our framework can be used for real-life applications, and because our framework uses SMT solvers, the range of appropriate applications will increase as these solvers become more efficient over time.
The fundamental challenge in distributed predicate detection lies in causality induced by inherent non-determinism @cite_4 . Most existing distributed system monitoring works have focused on asynchronous systems that use vector clocks (VCs) @cite_2 @cite_19 and @cite_9 @cite_7 @cite_10 @cite_11 @cite_8 make minimal assumptions about the underlying system. Unfortunately, asynchronous monitors have several sources of inefficiency that limit their scalability and impede their adoption in real systems. First, general predicate detection with asynchronous monitors is NP-complete @cite_11 , although polynomial time algorithms exists for special cases of predicate detection such as linear predicates and conjunctive predicates @cite_11 @cite_9 . Second, asynchronous monitors require @math space VC timestamps to track all causalities @cite_8 in the system where @math is the number of processes. Thus, each message has linear size in the system which limits scalability of asynchronous monitors.
@cite_4 @cite_7 @cite_8 @cite_9 @cite_19 @cite_2 @cite_10 @cite_11
1981173460 2071933194 2160800498 1652742168 2116746874 2016720263 2052995544
The paper shows that characterizing the causal relationship between significant events is an important but non-trivial aspect for understanding the behavior of distributed programs. An introduction to the notion of causality and its relation to logical time is given; some fundamental results concerning the characterization of causality are presented. Recent work on the detection of causal relationships in distributed computations is surveyed. The issue of observing distributed computations in a causally consistent way and the basic problems of detecting global predicates are discussed. To illustrate the major difficulties, some typical monitoring and debugging approaches are assessed, and it is demonstrated how their feasibility is severely limited by the fundamental problem to master the complexity of causal relationships. This paper discusses detection of global predicates in a distributed program. Earlier algorithms for detection of global predicates proposed by Chandy and Lamport (1985) work only for stable predicates. A predicate is stable if it does not turn false once it becomes true. Our algorithms detect even unstable predicates, without excessive overhead. In the past, such predicates have been regarded as too difficult to detect. The predicates are specified by using a logic described formally in this paper. We discuss detection of weak conjunctive predicates that are formed by conjunction of predicates local to processes in the system. Our detection methods will detect whether such a predicate is true for any interleaving of events in the system, regardless of whether the predicate is stable. Also, any predicate that can be reduced to a set of weak conjunctive predicates is detectable. This class of predicates captures many global predicates that are of interest to a programmer. The message complexity of our algorithm is bounded by the number of messages used by the program. The main applications of our results are in debugging and testing of distributed programs. Our algorithms have been incorporated in a distributed debugger that runs on a network of Sun workstations in UNIX. > A distributed system can be characterized by the fact that the global state is distributed and that a common time base does not exist. However, the notion of time is an important concept in every day life of our decentralized world" and helps to solve problems like getting a consistent population census or determining the potential causality between events. We argue that a linearly ordered structure of time is not (always) adequate for distributed systems and propose a generalized non-standard model of time which consists of vectors of clocks. These clock-vectors are partially ordered and form a lattice. By using timestamps and a simple clock update mechanism the structure of causality is represented in an isomorphic way. The new model of time has a close analogy to Minkowski's relativistic spacetime and leads among others to an interesting characterization of the global state problem. Finally, we present a new algorithm to compute a consistent global snapshot of a distributed system where messages may be received out of order. Timestamping is a common method of totally ordering events in concurrent programs. However, for applications requiring access to the global state, a total ordering is inappro­ priate. This paper presents algorithms for timestamping events in both synchronous and asynchronous n1essage-passing programs that allow for access to the partial ordering in­ herent in a parallel system. The algorithms do not change the con1munications graph or require a central timestamp issuing authority. In an asynchronous distributed system, a number of processes communicate with each other via message passing that has a finite but arbitrary long delay. There is no global clock in that system. Predicates, denoting the states of processes and their relations, are often used to specify the information of interest in such a system. Due to the lack of a global clock, the temporal relations between the states at different processes cannot be uniquely determined, but have multiple possible circumstances. Existing works of predicate detection are based on the definitely modality or the possibly modality, denoting that a predicate holds in all of the possible circumstances or in one of them, respectively. No information is provided about the probability that a predicate will hold, which hinders the taking of countermeasures for different situations. Moreover, the detection is based on single occurrence of a predicate, so the results are heavily affected by environmental noise and detection errors. In this paper, we propose a new approach to predicate detection to address these two issues. We generalize the definitely and possibly modalities to an occurrence probability to provide more detailed information, and further investigate how to detect multiple occurrences of a predicate. We propose a unified algorithm framework for detecting various types of predicates and demonstrate the use of it for three typical types of predicates, including simple predicates, simple sequences, and interval-constrained sequences. Theoretical proofs and simulation results show that our approach is effective and outperforms existing approaches. We show that the problem of predicate detection in distributed systems is NP-complete. In the past, efficient algorithms have been developed for special classes of predicates such as stable predicates, observer independent predicates, and conjunctive predicates. We introduce a class of predicates, semi-linear predicates, which properly contains all of the above classes. We first discuss stable, observer independent and semi-linear classes of predicates and their relationships with each other. We also study closure properties of these classes with respect to conjunction and disjunction. Finally, we discuss algorithms for detection of predicates in these classes. We provide a nondeterministic detection algorithm for each class of predicate. We show that each class can be equivalently characterized by the degree of non-determinism present in the algorithm. Stable predicates are defined as those that can be detected by an algorithm with the most non-determinism. All other classes can be derived by appropriately constraining the non-determinism in this algorithm.