A Formal Model For Real-Time Parallel Computation
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 su...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1301.0040v1 |
| _version_ | 1811266233874513920 |
|---|---|
| author | Peter Hui Satish Chikkagoudar |
| author_facet | Peter Hui Satish Chikkagoudar |
| author_sort | Peter Hui |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-12T20:38:24Z |
| format | Article |
| id | doaj.art-9264dbeb55d64fbf9476569530b84ecc |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T20:38:24Z |
| publishDate | 2012-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-9264dbeb55d64fbf9476569530b84ecc2022-12-22T03:17:29ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-12-01105Proc. FTSCS 2012395510.4204/EPTCS.105.4A Formal Model For Real-Time Parallel ComputationPeter HuiSatish ChikkagoudarThe 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.http://arxiv.org/pdf/1301.0040v1 |
| spellingShingle | Peter Hui Satish Chikkagoudar A Formal Model For Real-Time Parallel Computation Electronic Proceedings in Theoretical Computer Science |
| title | A Formal Model For Real-Time Parallel Computation |
| title_full | A Formal Model For Real-Time Parallel Computation |
| title_fullStr | A Formal Model For Real-Time Parallel Computation |
| title_full_unstemmed | A Formal Model For Real-Time Parallel Computation |
| title_short | A Formal Model For Real-Time Parallel Computation |
| title_sort | formal model for real time parallel computation |
| url | http://arxiv.org/pdf/1301.0040v1 |
| work_keys_str_mv | AT peterhui aformalmodelforrealtimeparallelcomputation AT satishchikkagoudar aformalmodelforrealtimeparallelcomputation AT peterhui formalmodelforrealtimeparallelcomputation AT satishchikkagoudar formalmodelforrealtimeparallelcomputation |