Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version)

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

    Research output: Book/ReportReportOther research output

    29 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, the Netherlands
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages32
    Publication statusPublished - 21 Jan 2014

    Publication series

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

    Keywords

    • Timed Automata
    • IR-89306
    • Multiprocessor
    • Heterogeneous
    • Scheduling
    • Synchronous Dataflow Graph
    • Throughput

    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 SDF graphs via timed automata (extended version). (CTIT technical reports; No. TR-CTIT-13-17). Enschede, the Netherlands: 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 SDF graphs via timed automata (extended version). Enschede, the Netherlands : Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT technical reports; TR-CTIT-13-17).
    @book{6f198824517e4008828d1195e1a330fd,
    title = "Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version)",
    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 = "Timed Automata, IR-89306, Multiprocessor, Heterogeneous, Scheduling, Synchronous Dataflow Graph, Throughput",
    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 ACSD 2014 submission",
    year = "2014",
    month = "1",
    day = "21",
    language = "Undefined",
    series = "CTIT technical reports",
    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 SDF graphs via timed automata (extended version). CTIT technical reports, no. TR-CTIT-13-17, Centre for Telematics and Information Technology (CTIT), Enschede, the Netherlands.

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

    Enschede, the Netherlands : Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT technical reports; No. TR-CTIT-13-17).

    Research output: Book/ReportReportOther research output

    TY - BOOK

    T1 - Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version)

    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 ACSD 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 - Timed Automata

    KW - IR-89306

    KW - Multiprocessor

    KW - Heterogeneous

    KW - Scheduling

    KW - Synchronous Dataflow Graph

    KW - Throughput

    M3 - Report

    T3 - CTIT technical reports

    BT - Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version)

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede, the Netherlands

    ER -

    Ahmad W, de Groote R, Holzenspies PKF, Stoelinga MIA, van de Pol JC. Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version). Enschede, the Netherlands: Centre for Telematics and Information Technology (CTIT), 2014. 32 p. (CTIT technical reports; TR-CTIT-13-17).