Oct 15, 2013: Waheed Ahmad: Optimal Scheduling of Synchronous Dataflow Graphs via Timed Automata

October 15, 2013Optimal Scheduling of Synchronous Dataflow Graphs via Timed Automata
Room: HalB 2FWaheed Ahmad

Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and a multiprocessing context. Efficient schedules are necessary to obtain maximal throughput with the optimum energy consumption in such a way that the number of resources used to run these applications is kept as low as possible. This paper presents an approach of scheduling SDF graphs using a proven formalism for timed systems called timed automata (TA). TA hold a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe an algorithm for the compositional translation of SDF graphs to TA and we provide an implementation of the translation to analyse and verify SDF graphs in the state-of-the-art tool Uppaal. 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 throughput. It also allows quantitative model checking and verification of user-defined properties like absence of deadlocks, safety, liveness and throughput analysis. The translation also forms the basis for future work of extending SDF graphs with the new features, e.g. stochastics, energy consumption and costs.