Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata

W. Ahmad, Robert de Groote, P.K.F. Holzenspies, Mariëlle Ida Antoinette Stoelinga, Jan Cornelis van de Pol

Research output: Book/ReportReportProfessional

11 Citations (Scopus)
58 Downloads (Pure)

Abstract

Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and in a multiprocessing context. Efficient schedules are essential to obtain maximal throughput under the constraint of available number of resources. This paper presents an approach to schedule SDF graphs using a proven formalism of timed automata (TA). TA maintain a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe a compositional translation of SDF graphs to TA, and analysis and verification in the Uppaal state-of-the-art tool. This approach does not require any transformation of SDF graphs and helps to find schedules with a compromise between the number of processors required and the throughput. It also allows quantitative model checking and verification of user-defined properties such as the absence of deadlocks, safety, liveness and throughput analysis. This translation also forms the basis for future work to extend this analysis of SDF graphs with new features such as stochastics, energy consumption and costs.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages32
Publication statusPublished - 21 Jan 2014

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology
No.TR-CTIT-13-17
ISSN (Print)1381-3625

Keywords

  • Throughput
  • Timed Automata
  • IR-89077
  • EC Grant Agreement nr.: FP7/318490
  • Synchronous Dataflow Graph
  • Scheduling
  • EWI-23670
  • METIS-303965
  • Multiprocessor
  • Heterogeneous
  • EC Grant Agreement nr.: FP7/2007-2013

Cite this

Ahmad, W., de Groote, R., Holzenspies, P. K. F., Stoelinga, M. I. A., & van de Pol, J. C. (2014). Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. (CTIT Technical Report Series; No. TR-CTIT-13-17). Enschede: Centre for Telematics and Information Technology (CTIT).
Ahmad, W. ; de Groote, Robert ; Holzenspies, P.K.F. ; Stoelinga, Mariëlle Ida Antoinette ; van de Pol, Jan Cornelis. / Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT Technical Report Series; TR-CTIT-13-17).
@book{aa281c6ab5a441b3b42cfa54684cf397,
title = "Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata",
abstract = "Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and in a multiprocessing context. Efficient schedules are essential to obtain maximal throughput under the constraint of available number of resources. This paper presents an approach to schedule SDF graphs using a proven formalism of timed automata (TA). TA maintain a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe a compositional translation of SDF graphs to TA, and analysis and verification in the Uppaal state-of-the-art tool. This approach does not require any transformation of SDF graphs and helps to find schedules with a compromise between the number of processors required and the throughput. It also allows quantitative model checking and verification of user-defined properties such as the absence of deadlocks, safety, liveness and throughput analysis. This translation also forms the basis for future work to extend this analysis of SDF graphs with new features such as stochastics, energy consumption and costs.",
keywords = "Throughput, Timed Automata, IR-89077, EC Grant Agreement nr.: FP7/318490, Synchronous Dataflow Graph, Scheduling, EWI-23670, METIS-303965, Multiprocessor, Heterogeneous, EC Grant Agreement nr.: FP7/2007-2013",
author = "W. Ahmad and {de Groote}, Robert and P.K.F. Holzenspies and Stoelinga, {Mari{\"e}lle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
note = "Technical report accompanying the ACDS 2014 submission",
year = "2014",
month = "1",
day = "21",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-17",
address = "Netherlands",

}

Ahmad, W, de Groote, R, Holzenspies, PKF, Stoelinga, MIA & van de Pol, JC 2014, Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. CTIT Technical Report Series, no. TR-CTIT-13-17, Centre for Telematics and Information Technology (CTIT), Enschede.

Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. / Ahmad, W.; de Groote, Robert; Holzenspies, P.K.F.; Stoelinga, Mariëlle Ida Antoinette; van de Pol, Jan Cornelis.

Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT Technical Report Series; No. TR-CTIT-13-17).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata

AU - Ahmad, W.

AU - de Groote, Robert

AU - Holzenspies, P.K.F.

AU - Stoelinga, Mariëlle Ida Antoinette

AU - van de Pol, Jan Cornelis

N1 - Technical report accompanying the ACDS 2014 submission

PY - 2014/1/21

Y1 - 2014/1/21

N2 - Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and in a multiprocessing context. Efficient schedules are essential to obtain maximal throughput under the constraint of available number of resources. This paper presents an approach to schedule SDF graphs using a proven formalism of timed automata (TA). TA maintain a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe a compositional translation of SDF graphs to TA, and analysis and verification in the Uppaal state-of-the-art tool. This approach does not require any transformation of SDF graphs and helps to find schedules with a compromise between the number of processors required and the throughput. It also allows quantitative model checking and verification of user-defined properties such as the absence of deadlocks, safety, liveness and throughput analysis. This translation also forms the basis for future work to extend this analysis of SDF graphs with new features such as stochastics, energy consumption and costs.

AB - Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and in a multiprocessing context. Efficient schedules are essential to obtain maximal throughput under the constraint of available number of resources. This paper presents an approach to schedule SDF graphs using a proven formalism of timed automata (TA). TA maintain a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe a compositional translation of SDF graphs to TA, and analysis and verification in the Uppaal state-of-the-art tool. This approach does not require any transformation of SDF graphs and helps to find schedules with a compromise between the number of processors required and the throughput. It also allows quantitative model checking and verification of user-defined properties such as the absence of deadlocks, safety, liveness and throughput analysis. This translation also forms the basis for future work to extend this analysis of SDF graphs with new features such as stochastics, energy consumption and costs.

KW - Throughput

KW - Timed Automata

KW - IR-89077

KW - EC Grant Agreement nr.: FP7/318490

KW - Synchronous Dataflow Graph

KW - Scheduling

KW - EWI-23670

KW - METIS-303965

KW - Multiprocessor

KW - Heterogeneous

KW - EC Grant Agreement nr.: FP7/2007-2013

M3 - Report

T3 - CTIT Technical Report Series

BT - Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Ahmad W, de Groote R, Holzenspies PKF, Stoelinga MIA, van de Pol JC. Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. Enschede: Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT Technical Report Series; TR-CTIT-13-17).