2026-07-20T07:34:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8977 2024-03-06T10:43:07Z ddc:004 open_access

On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks Cerqueira, Felipe Nelissen, Geoffrey Brandenburg, Björn B. real-time scheduling sustainability self-suspending tasks machine-checked proofs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Felipe Cerqueira and Geoffrey Nelissen and Björn B. Brandenburg 2018 Is Part Of LIPIcs, Volume 106, 30th Euromicro Conference on Real-Time Systems (ECRTS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECRTS.2018.26 urn:nbn:de:0030-drops-89773 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2018.26 eng https://creativecommons.org/licenses/by/3.0/legalcode