实时的并行计算的形式化模型
A Formal Model For Real-Time Parallel Computation
摘要：
对并行计算环境（特别是高性能集群计算系统）施加实时的【形】约束，对系统时序特性的形式化验证提出了各种挑战。在本文中，我们简要地激发了这样一个系统的需要，我们介绍了一个自动机为基础的方法来执行这样的形式化验证。我们定义了一个一致的并行定时系统的概念：一个混合动力系统组成的一组时间自动机（具体来说，定时Buchi自动机以及标准有限自动机的定时变体），旨在模拟一个表现良好的实时的【形】并行系统的定时特性。最后，我们给出了一个简短的案例研究来证明本文中的概念：一个并行矩阵乘法内核，它在可证明的时间上界内运行。我们给出了所使用的算法，相应的一致的并行定时系统，和实证结果表明，该系统在指定的时间约束下运行。
英文摘要：
The imposition of real-time constraints on a parallel computing environment- specifically high-performance, cluster-computing systems- introduces a variety of challenges with respect to the formal verification of the system's timing properties. In this paper, we briefly motivate the need for such a system, and we introduce an automaton-based method for performing such formal verification. We define the concept of a consistent parallel timing system: a hybrid system consisting of a set of timed automata (specifically, timed Buchi automata as well as a timed variant of standard finite automata), intended to model the timing properties of a well-behaved real-time parallel system. Finally, we give a brief case study to demonstrate the concepts in the paper: a parallel matrix multiplication kernel which operates within provable upper time bounds. We give the algorithm used, a corresponding consistent parallel timing system, and empirical results showing that the system operates under the specified timing constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
