Arranging Partitures for Models and Theorems

In order to do reliable and efficient real-time scheduling of a software application or component, it is necessary to know as much as possible of the temporal behavior of a program up front. To make it possible to compose schedules it is necessary to know about the temporal behavior of the various applications and components involved. We describe the behavior using a Partiture, a description of the temporal phases of a program and their interdependencies. We then treat the partiture as a graph and model its semantics using abstract state machines. We then convert the state machine to a set of constraints and use the Z3 theorem prover to validate and solve the schedule. Finally the output is converted to a partially instantiated schedule, which can be executed on hardware, ranging from 8-bit microcontrollers to multicores and distributed systems. This work-in-progress paper shows how a number of common execution patterns map to a graph and model and how this interfaces with the theorem prover. It introduces an improved semantic description of partitures and for the first time shows how satisfiability modulo theory (SMT) could be used to perform scheduling analysis, with the practical side demonstrated by a simple case study. This sets the stage for planned future extensions to multiple resources and multicore.