计算切片技术及其应用
Techniques and Applications of Computation Slicing
摘要：
编写正确的分布式程序很难。尽管进行了广泛的测试和调试，但即使在商业级软件中，软件故障也会持续存在。许多分布式系统，特别是那些在安全关键环境中使用的系统，即使在软件故障的情况下也应该能够正常运行。监视分布式系统的执行，并在检测到故障时启动适当的纠正措施是容忍此类故障的重要方法。这就产生了谓词检测问题，它需要找到一个满足给定全局谓词（如果存在）的给定计算的一致切割。然而，在计算中检测谓词是一个NP完全问题。为了改善相关的组合爆炸问题，我们引入了计算切片的概念。形式上，相对于谓词的计算的切片是具有最少数量的一致切割的（子）计算，其包含满足谓词的计算的所有一致切割。为了检测谓词，搜索切片的状态空间要比搜索计算的状态空间有效得多。我们证明了片存在，是唯一定义的所有谓词。我们提出了有效的切片算法的几个有用的类的谓词。我们开发了有效的启发式算法计算的近似切片的谓词，计算切片，否则证明棘手。我们的实验结果表明，切片可以导致一个指数级的改进，在时间和空间方面的谓词检测现有的技术。
英文摘要：
Writing correct distributed programs is hard. In spite of extensive testing and debugging, software faults persist even in commercial grade software. Many distributed systems, especially those employed in safety-critical environments, 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 a consistent cut of a given computation that satisfies a given global predicate, if it exists. Detecting a predicate in a computation is, however, an NP-complete problem. 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. 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 exists and is uniquely defined for all predicates. We present efficient slicing algorithms for several useful classes of predicates. We develop efficient heuristic algorithms for computing an approximate slice for predicates for which computing the slice is otherwise provably intractable. Our experimental results show that slicing can lead to an exponential improvement over existing techniques for predicate detection in terms of time and space.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
