A Formal Model For Real-Time Parallel Computation

TL;DR

This paper introduces a formal automaton-based model for verifying real-time constraints in parallel high-performance computing systems, demonstrated through a case study on matrix multiplication.

Contribution

It proposes a novel hybrid automaton model for formal verification of timing properties in real-time parallel systems.

Findings

The model accurately captures timing behaviors of parallel systems.

The case study confirms the system operates within specified time bounds.

Abstract

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.