Detection of Global Predicates in Distributed Programs

本项目的目的是研究分布式软件通用全局谓词和功能评估中的理论和实践问题。作为该研究技术的应用，本项目将重点研究分布式容错监控系统。检测全局谓词的一个例子出现在监控系统的最基本命令的实现中：“当谓词为真时停止程序”。要停止程序，必须检测谓词q，如果q需要访问全局状态，这不是一项简单的任务。该项目有三个组成部分：理论、算法和实现。有两个问题将在理论方面进行研究。首先，对可有效检测的全局谓词进行分类。这也需要研究有效检测全局谓词的限制。其次，将开发一种适合于高效检测全局谓词的谓词逻辑。在开发逻辑后，将设计高效的分散算法来检测逻辑公式的出现。这项工作将基于PI开发的集中检查程序的使用。最后，利用去中心化算法设计一个实验性的分布式监控系统。

The objective of this project is to study theoretical and practical issues in the evaluation of general globel predicates and functions of distributed software. As an application of the techniques of the research, the project will focus on distributed monitoring systems for fault tolerance. An example of detecting a global predicate arises in implementing the most basic command of a monitoring system: `stop the program when the predicate is true`. To stop the program it is necessary to detect the predicate q, which is not a trivial task if q requires access to the global state. There are three components to the project: theory, algorithms and implementation. There are two questions that will be investigated in terms of theory. First, the class of global predicates that are efficient to detect will be classified. This will also entail studying the limits of efficient detection of global predicates. Second, a predicate logic which is suitable for efficient detection of global predicates will be developed. After developing the logic, efficient decentralized algorithms for detecting occurrence of logic formulas will be designed. This work will be based on the use of a centralized checker process developed by the PI. Finally, the decentralized algorithm will be used to design an experimental distributed monitoring system.