FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Safe and Optimal Scheduling of Hard and Soft Tasks

Authors: Gilles Geeraerts, Shibashis Guha and Jean-Francois Raskin

Paper Information

Title:Safe and Optimal Scheduling of Hard and Soft Tasks
Authors:Gilles Geeraerts, Shibashis Guha and Jean-Francois Raskin
Proceedings:MoRe Papers
Editors: Mickael Randour and Jeremy Sproston
Keywords:Markov Decision Process, Scheduling, Strategy synthesis, Multi-objective synthesis
Abstract:

ABSTRACT. We consider a stochastic scheduling problem with both hard and soft tasks. Each task is described by a discrete probability distribution over possible execution times, a deadline and a distribution over inter-arrival times. Our scheduling problem is non-clairvoyant in the sense that the execution and inter-arrival times are subject to uncertainty modeled by stochastic distributions. Given an instance of our problem, we want to synthesize a schedule that is safe and efficient: safety imposes that deadline of hard tasks are never violated while efficient means that soft tasks should be completed as often as possible. To enforce that property, we impose a cost when a soft task deadline is violated and we are looking for a schedule that minimizes the expected value of the limit average of this cost.

First, we show that the dynamics of such a system can be modeled as a finite Markov Decision Process (MDP). Second, we show that the problem of deciding the existence of a safe and efficient scheduler is PP-hard and in EXPTIME. Third, we have implemented our synthesis algorithm that partly relies on the probabilistic model-checker Storm to analyze the underlying MDP. Given a set of both hard and soft tasks, we first compute the set of safe schedules, i.e., the ones in which the hard tasks always finish their execution, then we compute the scheduler that minimizes the limit average cost among the set of all safe schedules. Finally, we compare the optimal solutions obtained with our procedure against an adaptation of the earliest deadline first (EDF) algorithm to account for the soft task. We show that this EDF strategy can be arbitrarily worse in terms of the expected limit average cost for missing the deadlines of the soft tasks when compared to our optimal procedure.

Pages:4
Talk:Jul 13 16:30 (Session 88G: Markov decision processes 2)
Paper: