Detection of Global Predicates in Distributed Programs

这个项目的目标是研究评估通用Globel谓词和分布式软件功能的理论和实践问题。作为研究技术的应用，该项目将重点研究分布式容错监控系统。一个检测全局谓词的例子出现在实现监视系统的最基本命令时：当谓词为真时停止程序。要停止程序，必须检测谓词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.