ITR: Techniques for Dynamic Verification of Parallel Distributed Systems

最近，人们提出了一种新的复杂超标量处理器的运行时验证方法。在这种方法中，每一次计算都由硬件使用完全归纳的形式进行动态验证。本项目致力于将归纳动态验证的概念扩展到并行分布式系统的一般情况。研究了并行语义的动态归纳检查原理。这包括对系统的特征和属性的理解，在那里可以有效地使用该方法。用于开发这种技术的最初工具是共享内存多处理器中的高速缓存一致性和对顺序一致性的支持问题。作为本研究的自然延伸，本课题提出了一种适用于一般情况的状态机抽象方法。该方法依赖于体系结构状态与附加实现状态的分离，以及仅对应于体系结构状态中的变化的状态转换子集的标识。

Recently, a novel approach for runtime verification of complex superscalar processors has been proposed. In this approach, every computation is dynamically verified by hardware using a form of complete induction. This project focuses on extending the notion of inductive dynamic verification to the general case of parallel distributed systems. The principles of dynamic inductive checking for parallel semantics are investigated. This includes an understanding of the characteristics and properties of systems, where the approach can be used effectively. The initial vehicles used for developing such techniques are the problems of cache coherence and support for sequential consistency in shared-memory multiprocessors. As a natural extension of this research, the project formulates a method for state machine abstraction, which can be applied in the general case. This method rests on the separation of architected state from additional implementation state, and the identification of that subset of state transitions that correspond to changes in the architected state only.