Verifying Parallel Dataflow Transformations with Model Checking and its Application to FPGAs

Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, Andrew Wallace

Research output: Contribution to journalArticle

1 Citation (Scopus)
17 Downloads (Pure)

Abstract

Dataflow languages are widely used for programming real-time embedded systems. They offer high level abstraction above hardware, and are amenable to program analysis and optimisation. This paper addresses the challenge of verifying parallel program transformations in the context of dynamic dataflow models, where the scheduling behaviour and the amount of data each actor computes may depend on values only known at runtime.

We present a Linear Temporal Logic (LTL) model checking approach to verify a dataflow program transformation, using three LTL properties to identify cyclostatic actors in dynamic dataflow programs. The workflow abstracts dataflow actor code to Fiacre specifications to search for counterexamples of the LTL properties using the Tina model checker. We also present a new refactoring tool for the Orcc dataflow programming environment, which applies the parallelising transformation to cyclostatic actors. Parallel refactoring using verified transformations speedily improves FPGA performance, e.g. 15.4×  speedup with 16 actors.
Original languageEnglish
Article number101657
JournalJournal of Systems Architecture
Volume101
Early online date23 Oct 2019
DOIs
Publication statusPublished - Dec 2019

Keywords

  • Dataflow
  • FPGAs
  • Model checking
  • Parallelism
  • Program transformation

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Verifying Parallel Dataflow Transformations with Model Checking and its Application to FPGAs'. Together they form a unique fingerprint.

Cite this