License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECRTS.2018.26
URN: urn:nbn:de:0030-drops-89773
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8977/
Cerqueira, Felipe ;
Nelissen, Geoffrey ;
Brandenburg, Björn B.
On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks
Abstract
Motivated by an apparent contradiction regarding whether certain scheduling policies are sustainable, we revisit the topic of sustainability in real-time scheduling and argue that the existing definitions of sustainability should be further clarified and generalized. After proposing a formal, generic sustainability theory, we relax the existing notion of (strongly) sustainable scheduling policy to provide a new classification called weak sustainability. Proving weak sustainability properties allows reducing the number of variables that must be considered in the search of a worst-case schedule, and hence enables more efficient schedulability analyses and testing regimes even for policies that are not (strongly) sustainable. As a proof of concept, and to better understand a model for which many mistakes were found in the literature, we study weak sustainability in the context of dynamic self-suspending tasks, where we formalize a generic suspension model using the Coq proof assistant and provide a machine-checked proof that any JLFP scheduling policy is weakly sustainable with respect to job costs and variable suspension times.
BibTeX - Entry
@InProceedings{cerqueira_et_al:LIPIcs:2018:8977,
author = {Felipe Cerqueira and Geoffrey Nelissen and Bj{\"o}rn B. Brandenburg},
title = {{On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks}},
booktitle = {30th Euromicro Conference on Real-Time Systems (ECRTS 2018)},
pages = {26:1--26:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-075-0},
ISSN = {1868-8969},
year = {2018},
volume = {106},
editor = {Sebastian Altmeyer},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8977},
URN = {urn:nbn:de:0030-drops-89773},
doi = {10.4230/LIPIcs.ECRTS.2018.26},
annote = {Keywords: real-time scheduling, sustainability, self-suspending tasks, machine-checked proofs}
}
Keywords: |
|
real-time scheduling, sustainability, self-suspending tasks, machine-checked proofs |
Collection: |
|
30th Euromicro Conference on Real-Time Systems (ECRTS 2018) |
Issue Date: |
|
2018 |
Date of publication: |
|
22.06.2018 |