Pranav Tendulkar, Peter Poplavko, Oded Maler
Strictly Periodic Scheduling of Acyclic Synchronous Dataflow Graphs using SMT Solvers (2014)
Strictly Periodic Scheduling of Acyclic Synchronous Dataflow Graphs using SMT Solvers (2014)
TR-2014-5.pdf
Keywords: synchronous dataflow graphs, multiprocessor scheduling, multi-rate data-flow graphs, pipelined scheduling, modulo scheduling, non-preemptive scheduling, constraint solving, SAT/SMT solving
Abstract: We consider compile-time multi-core mapping and scheduling problem for synchronous dataflow (SDF) graphs, proved an important model of computation for streaming applications, such as signal/image processing and video/image coding. In general the real-time constraints for these applications include both the task periods / throughput and the deadlines / latency. The deadlines are typically larger than the periods, which enables pipelined scheduling, allowing concurrent execution of different iterations of an application. A majority of algorithms for scheduling SDF graphs on a limited number of processors do not consider both latency and period real-time constraints at the same time. For this problem, we propose an efficient method based on SMT (satisfiability modulo theory) solvers. We restrict ourselves to strictly periodic scheduling and acyclic graphs, giving up some efficiency for the sake of simplicity. We also upgrade and integrate two alternative methods unfolding and modulo scheduling - into our scheduling framework. Experiments for different methods are performed for a set of application benchmarks and advantages of the proposed method is demonstrated empirically.
