Scheduling shared memory multicore architectures in AutoFOCUS3 using Satisfiability Modulo Theories

abstract

This paper presents an approach to task and message scheduling for multicore architectures using a shared memory. A shared memory architecture is used in most of the current multicore systems. The presented approach is integrated in the AUTOFOCUS 3 toolchain that allows to automatically compute schedules for this architecture to fulfill certain system requirements. AUTOFOCUS 3 models are based on a formally defined system model using explicit data-flow and discrete-time semantics. Our approach relies on a symbolic encoding scheme, based on a scheduling model, that we generate out of AUTOFO-CUS 3 system architectures. This encoding scheme relies on the AUTOFOCUS 3 semantics of strong-and weak-causal com-ponents and enables to generate schedules, that fulfill certain system properties. In this paper we focus on finding optimized schedules with respect to the global discrete time base. This paper provides a formalization that describes the scheduling problem as a satisfiability problem using boolean formulas and linear arithmetical constraints. A state-of-the-art satisfiability modulo theories (SMT) solver is then used to compute these schedules. This paper demonstrates that state-of-the art satisfiability modulo theories solver can be used to to compute a schedule that fulfills certain system requirements and meet the challenges of providing both a convenient modeling language and the performance to solve industrialized-sized design problems.