Efficient distributed detection of conjunctions of local predicates

Global predicate detection is a fundamental problem in distributed systems and finds applications in many domains such as testing and debugging distributed programs. This paper presents an efficient distributed algorithm to detect conjunctive-form global predicates in distributed systems. The algorithm detects the first consistent global state that satisfies the predicate even if the predicate is unstable. Unlike previously proposed run-time predicate detection algorithms, our algorithm does not require the exchange of control messages during the normal computation. All the necessary information to detect predicates is piggybacked on computation messages of application programs. The algorithm is distributed because the predicate detection efforts as well as the necessary information are equally distributed among the processes. We prove the correctness of the algorithm and compare its performance with respect to message, storage and computational complexities with that of the previously proposed run-time predicate detection algorithms     

Techniques and applications of computation slicing

Writing correct distributed programs is hard. In spite of extensive testing and debugging, software faults persist even in commercial grade software. Many distributed systems should be able to operate properly even in the presence of software faults. Monitoring the execution of a distributed system, and, on detecting a fault, initiating the appropriate corrective action is an important way to tolerate such faults. This gives rise to the predicate detection problem which requires finding whether there exists a consistent cut of a given computation that satisfies a given global predicate.Detecting a predicate in a computation is, however, an NP-complete problem in general. In order to ameliorate the associated combinatorial explosion problem, we introduce the notion of computation slice. Formally, the slice of a computation with respect to a predicate is a (sub)computation with the least number of consistent cuts that contains all consistent cuts of the computation satisfying the predicate. Intuitively, slice is a concise representation of those consistent cuts of a computation that satisfy a certain condition. To detect a predicate, rather than searching the state-space of the computation, it is much more efficient to search the state-space of the slice.We prove that the slice of a computation is uniquely defined for all predicates. We also present efficient algorithms for computing the slice for several useful classes of predicates. For an arbitrary predicate, we establish that the problem of computing the slice is NP-complete in general. Nonetheless, for such a predicate, we develop an efficient heuristic algorithm for computing an approximate slice. Our experimental results demonstrate that slicing can lead to an exponential improvement over existing techniques for predicate detection in terms of time and space.Received: 19 November 2003, Revised: 29 July 2004, Published online: 7 February 2005Vijay K. Garg: Supported in part by the NSF Grants ECS-9907213, CCR-9988225, Texas Education Board Grant ARP-320, an Engineering Foundation Fellowship, and an IBM grant.Parts of this paper have appeared earlier in conference proceedings [GM01,MG01a,MG03a].     

Detection of weak unstable predicates in distributed programs

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     

Intractability results in predicate detection

It has been shown that global predicate detection in a distributed computation is an NP-complete problem in general. However, efficient predicate detection algorithms exist for some subclasses of predicates, such as stable predicates, observer-independent predicates, conjunctions of local predicates, channel predicates, etc. We show here that the problem of deciding whether a given predicate is a member of any of these tractable subclasses is NP-hard in general.We also explore the tractability of linear and regular predicates. In particular, we show that, unless RP=NP, there is no polynomial-time algorithm to detect for linear and regular predicates B.     

Detection of global predicates: Techniques and their limitations

Summary. 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 non-deterministic 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.     

Distributed predicate detection in series-parallel systems

This paper addresses the problems of state space decomposition and predicate detection in a distributed computation involving asynchronous messages. We introduce a natural communication dependency which leads to the definition of the communication graph. This abstraction proves to be a useful tool to decompose the state lattice of a distributed computation into simpler structures, known as concurrent intervals. Efficient algorithms have been proposed in the literature to detect special classes of predicates, such as conjunctive predicates and bounded sum predicates. We show that more general classes of predicates can be detected when proper constraints are imposed on the underlying computations. In particular, we introduce a class of predicates, defined as separable predicates, that properly includes the above-mentioned classes. We show that separable predicates can be efficiently detected on distributed computations whose communication graphs satisfy the series-parallel constraint     

基于谓词检测方法的上下文感知案例研究

当前,开发灵活的适应环境变化的上下文感知应用较为复杂。在上下文感知应用开发过程中,很多未知情况无法事先被充分考虑到,实际的开发又需要处理很多意外情形,因此有效地表示和处理上下文尤为重要。谓词检测作为实现上下文感知的重要方法之一,能够有效对上下文信息进行建模,但在实际应用中对于真实物理设备的支持如何在很大程度上仍然是未知的。为了应对以上问题,通过构建一个简单的物理场景,将谓词检测方法应用于真实的机器小车上,支持其在一个既定轨道上完成运行任务。在该场景下对原始的上下文环境进行建模,将环境特性逐步规约成特定的快照谓词和序列谓词,并在案例研究中,对规约化的谓词进行检测,将谓词检测应用于真实的机器小车实验上。实验分析的结果表明,谓词检测的方法能有效检测小车的上下文特性并成功支撑小车完成既定的行走目标。     

Automatic string test data generation for detecting domain errors

Domain testing is designed to detect domain errors that result from a small boundary shift in a path domain. Although many researchers have studied domain testing, automatic domain test data generation for string predicates has seldom been explored. This paper presents a novel approach for the automatic generation of ON–OFF test points for string predicate borders, and describes a corresponding test data generator. Our empirical work is conducted on a set of programs with string predicates, where extensive trials have been done for each string predicate, and the results are analysed using the SPSS tool. Conclusions are drawn that: (i) the approach is promising and effective; (ii) there is a strong linear relationship between the performance of the test generator and the length of target string in the predicate tested; and (iii) initial inputs, no shorter than the target string and with characters generated randomly, may enhance the performance in the test data generation for string predicates. Copyright © 2009 John Wiley & Sons, Ltd.     

Detecting global predicates in distributed systems with clocks

Summary. This paper proposes a framework for detecting global state predicates in systems of processes with approximately-synchronized real-time clocks. Timestamps from these clocks are used to define two orderings on events: “definitely occurred before” and “possibly occurred before”. These orderings lead naturally to definitions of 3 distinct detection modalities, i.e., 3 meanings of “predicate held during a computation”, namely: (“ possibly held”), (“ definitely held”), and (“ definitely held in a specific global state”). This paper defines these modalities and gives efficient algorithms for detecting them. The algorithms are based on algorithms of Garg and Waldecker, Alagar and Venkatesan, Cooper and Marzullo, and Fromentin and Raynal. Complexity analysis shows that under reasonable assumptions, these real-time-clock-based detection algorithms are less expensive than detection algorithms based on Lamport's happened-before ordering. Sample applications are given to illustrate the benefits of this approach. Received: January 1999 / Accepted: November 1999     

Efficient Implementation Techniques for Topological Predicates on Complex Spatial Objects

Topological relationships like overlap, inside, meet, and disjoint uniquely characterize the relative position between objects in space. For a long time, they have been a focus of interdisciplinary research as in artificial intelligence, cognitive science, linguistics, robotics, and spatial reasoning. Especially as predicates, they support the design of suitable query languages for spatial data retrieval and analysis in spatial database systems and geographical information systems. While, to a large extent, conceptual aspects of topological predicates (like their definition and reasoning with them) as well as strategies for avoiding unnecessary or repetitive predicate executions (like predicate migration and spatial index structures) have been emphasized, the development of robust and efficient implementation techniques for them has been largely neglected. Especially the recent design of topological predicates for all combinations of complex spatial data types has resulted in a large increase of their numbers and stressed the importance of their efficient implementation. The goal of this article is to develop correct and efficient implementation techniques of topological predicates for all combinations of complex spatial data types including two-dimensional point, line, and region objects, as they have been specified by different authors and in different commercial and public domain software packages. Our solution consists of two phases. In the exploration phase, for a given scene of two spatial objects, all topological events like intersection and meeting situations are summarized in two precisely defined topological feature vectors (one for each argument object of a topological predicate) whose specifications are characteristic and unique for each combination of spatial data types. These vectors serve as input for the evaluation phase which analyzes the topological events and determines the Boolean result of a topological predicate (predicate verification) or the kind of topological predicate (predicate determination) by a formally defined method called nine-intersection matrix characterization. Besides this general evaluation method, the article presents an optimized method for predicate verification, called matrix thinning, and an optimized method for predicate determination, called minimum cost decision tree. The methods presented in this article are applicable to all known complete collections of mutually exclusive topological predicates that are formally based on the well known nine-intersection model.

Distributed Breakpoint Detection in Message-Passing Programs

The ability to set breakpoints stands, along with the possibility of deterministic reexecution, as one of the most important issues in the debugging of message-passing programs. We consider in this paper the design of fully distributed algorithms for the detection of breakpoints in such programs, and provide four algorithms, one for each different type of breakpoint. One of the algorithms detects the occurrence of unconditional breakpoints, while the other three detect the occurrence of breakpoints on disjunctive predicates, stable conjunctive predicates, and generic conjunctive predicates. All the algorithms we present detect breakpoints in the form of earliest global states with respect to the particular property involved. In the case of unconditional breakpoints, such an earliest global state must coincide exactly with the requested local unconditional breakpoints for the processes that do actually participate in the breakpoint. In the case of the other (conditional) breakpoints, what is detected is the earliest global state at which either the disjunctive or the conjunctive predicate under consideration is true. In order to actually halt the computation at the exact global state the algorithms detect, we suggest as a first approach the use of checkpointing and rollback-recovery techniques.     

Predicate control: synchronization in distributed computations with look-ahead

The predicate control problem involves synchronizing a distributed computation to maintain a given global predicate. In contrast with many popular distributed synchronization problems such as mutual exclusion, readers writers, and dining philosophers, predicate control assumes a look-ahead, so that the computation is an off-line rather than an on-line input. Predicate control is targeted towards applications such as rollback recovery, debugging, and optimistic computing, in which such computation look-ahead is natural.We define predicate control formally and show that, in its full generality, the problem is NP-complete. We find efficient solutions for some important classes of predicates including “disjunctive predicates”, “mutual exclusion predicates”, and “readers writers predicates”. For each class of predicates, we determine the necessary and sufficient conditions for solving predicate control and describe an efficient algorithm for determining a synchronization strategy. In the case of “independent mutual exclusion predicates”, we determine that predicate control is NP-complete and describe an efficient algorithm that finds a solution under certain constraints.     

Towards the construction of distributed detection programs,with an application to distributed termination

Summary Methodological design of distributed programs is necessary if one is to master the complexity of parallelism. The class of control programs, whose purpose is to observe or detect properties of an underlying program, plays an important role in distributed computing. The detection of a property generally rests upon consistent evaluations of a predicate; such a predicate can be global, i.e. involve states of several processes and channels of the observed program. Unfortunately, in a distributed system, the consistency of an evaluation cannot be trivially obtained. This is a central problem in distributed evaluations. This paper addresses the problem of distributed evaluation, used as a basic tool for solution of general distributed detection problems. A new evaluation paradigm is put forward, and a general distributed detection program is designed, introducing the iterative scheme ofguarded waves sequence. The case of distributed termination detection is then taken to illustrate the proposed methodological design. Jean-Michel Hélary is currently professor of Computer Science at the University of Rennes, France. He received a first Ph.D. degree in Numerical Analysis in 1968, then another Ph.D. Degree in Computer Science in 1988. His research interests include distributed algorithms and protocols, specially the methodological aspects. He is a member of an INRIA research group working at IRISA (Rennes) on distributed algorithms and applications. Professor Jean-Michel Hélary has published several papers on these subjects, and is co-author of a book with Michel Raynal. He serves as a PC member in an international conference. Michel Raynal is currently professor of Computer Science at the University of Rennes, France. He received the Ph.D. degree in 1981. His research interests include distributed algorithms, operating systems, protocols and parallelism. He is the head of an INRIA research group working at IRISA (Rennes) on distributed algorithms and applications. Professor Michel Raynal has organized several international conferences and has served as a PC member in many international workshops, conferences and symposia. Over the past 9 years, he has written 7 books that constitute an introduction to distributed algorithms and distributed systems (among them: Algorithms for Mutual Exclusion, the MIT Press, 1986, and Synchronization and Control of Distributed Programs, Wiley, 1990, co-authored with J.M. Hélary). He is currently involved in two european Esprit projects devoted to large scale distributed systems.This work was supported by French Research Program C³ on Parallelism and Distributed ComputingAn extended abstract has been presented to ISTCS '92 [12]     

Detection of strong unstable predicates in distributed programs

This paper discusses detection of global predicates in a distributed program. A run of a distributed program results in a set of sequential traces, one for each process. These traces may be combined to form many global sequences consistent with the single run of the program. A strong global predicate is true in a run if it is true for all global sequences consistent with the run. We present algorithms which detect if the given strong global predicate became true in a run of a distributed program. Our algorithms can be executed on line as well as off line. Moreover, our algorithms do not assume that underlying channels satisfy FIFO ordering     

Self-stabilizing distributed queuing

Distributed queuing is a fundamental coordination problem arising in a variety of applications, including distributed shared memory, distributed directories, and totally ordered multicast. A distributed queue can be used to order events, user operations, or messages in a distributed system. This paper presents a new self-stabilizing distributed queuing protocol. This protocol adds self-stabilizing actions to the arrow distributed queuing protocol, a simple path-reversal protocol that runs on a spanning tree of the network. We present a proof that the protocol stabilizes to a stable state irrespective of the (perhaps faulty) initial state, and also present an analysis of the time until convergence. The self-stabilizing queuing protocol is structured as a layer that runs on top of any self-stabilizing spanning tree protocol. This additional queuing layer is guaranteed to stabilize in time bounded by a constant number of message delays across an edge, thus establishing that the stabilization time for distributed queuing is not much more than the stabilization time for spanning tree maintenance. The key idea in our protocol is that the global predicate defining the legality of a protocol state can be written as the conjunction of many purely local predicates, one for each edge of the spanning tree.     

基于谓词切片的字符串测试数据自动生成

字符串谓词使用相当普遍，如何实现字符串测试数据的自动生成是一个有待解决的问题，针对字符串谓词，讨论了路径Path上给定谓词的谓词切片的动态生成算法，以及基于谓词切片的字符串测试数据自动生成方法，并给出了字符串间距离的定义，利用程序DUC（Definithon-Use-Control)表达式，构造谓词的谓词切片，对任意的输入，通过执行谓词切片，获取谓词中变量的当前值，进而对谓词中变量的每一字符进行分支函数极小化，动态生成给定字符串谓词边界的ON－OFF测试点，实验表明，该方法是行之有效的。     

汉语谓词组合范畴语法词库的自动构建研究

谓词词库是深层语法模型分析和理解的核心资源。近年来的常规方法是人工构建或从标注语料库中自动获取,标注规模和信息容量的扩大受制于巨大的人工投入量和标注库体系设计。该文提出了一种多资源融合自动构建汉语谓词组合范畴语法(CCG)词库的新方法。从知网、北大语法信息词典和大规模事件句式实例中提取汉语谓词的不同句法语义分布特征,融合形成CCG原型范畴表示,将它们指派给各资源信息完全重合的谓词形成核心词库。然后通过自动分类和隶属度分析相结合方法对其他谓词的CCG范畴进行预测,并对两者结果进行融合得到扩展词库,最终合并形成包含约15,000个词条的汉语谓词CCG词库。通过在随机均匀抽样的1000个谓词上通过多人独立标注形成的标准测试库上进行不同角度的性能分析实验,表明该词库的预期准确率达到了96.3%。
     

基于与状态无关的激活集的包含派生谓词的规划问题求解

派生谓词是PDDL2．2语言的新特性之一。在2004年的规划大赛IPC-4上，许多规划系统都无法求解包含派生谓词的两个标准竞赛问题。在经典规划中，派生谓词是指不受领域动作直接影响的谓词，它们在当前状态下的真值是在封闭世界假设中由某些基本谓词通过领域公理推导出来的。本文提出一种新的方法来求解包含派生谓词的规划问题，即用与状态无关的激活集来取代派生谓词用于放宽式规划中。     

Techniques to tackle state explosion in global predicate detection

Global predicate detection, which is an important problem in testing and debugging distributed programs, is very hard due to the combinatorial explosion of the global state space. The paper presents several techniques to tackle the state explosion problem in detecting whether an arbitrary predicate Φ is true at some consistent global state of a distributed system. We present space efficient online algorithms for detecting Φ. We then improve the performance of our algorithms, both in space and time, by increasing the granularity of the execution step from an event to a sequence of events in each process     

基于概率和条件逻辑的PKI信任模型推理

提出一种基于概率和条件谓词逻辑来表示和推导PKI信任模型的方法．该方法用3个二元条件谓词表示不同个体之间的关系,并给出了实体认证规则、信任规则和信任扩展规则，对信任度定义了一个概率模型，该模型能反映约束条件如何影响信任度．概率模型加条件谓词逻辑能够对一个PKI信任模型进行更精确的描述．