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.