Pipelined Scheduling of Acyclic SDF Graphs using SMT Solvers

Abstract—We consider compile-time multi-core mapping and scheduling problem for synchronous dataflow (SDF) graphs, proved an important model of computation for streaming appli-cations, 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 periodic scheduling and acyclic graphs, giving up some efficiency for the sake of simplicity. We present an approach to encode the pipelined scheduling problem and demonstrate its practicality on Kalray MPPA-256 multi-core platform by executing various benchmarks according to the optimal schedules. I