Verifying parallel dataflow transformations with model checking and its application to FPGAs - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Article Dans Une Revue Journal of Systems Architecture Année : 2019

Verifying parallel dataflow transformations with model checking and its application to FPGAs

Résumé

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.

Dates et versions

hal-02347401 , version 1 (05-11-2019)

Identifiants

Citer

Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, et al.. Verifying parallel dataflow transformations with model checking and its application to FPGAs. Journal of Systems Architecture, 2019, 101, pp.101657. ⟨10.1016/j.sysarc.2019.101657⟩. ⟨hal-02347401⟩
85 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More