Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
808 commits behind the upstream repository.
-
Felipe Cerqueira authored
1) Definition of a generic model for job suspensions based on received service (e.g., job j_1 should suspend for 4ms as soon as service reaches 5ms). 2) Definition of the dynamic suspension model (i.e., cumulative suspension of job j_1 <= X). 3) Analysis of suspension-aware scheduling by inflation of job costs (via schedule reduction). In the literature, this is called suspension-oblivious analysis. 4) Analysis of suspension-aware scheduling by adjusting job jitter (via schedule reduction). 5) Proof of (weak) sustainability of job costs under suspension-aware scheduling. We show that if we increase the costs of all jobs while reducing their suspension times in a certain way, the response times of all jobs do not decrease. This has an important implication regarding worst-case schedules: if some schedulability analysis already accounts for the fact that job suspension times can vary from 0 to the task suspension bound, then it's perfectly safe to assume that jobs execute for their WCET. 6) Proof of sustainability of the cost of a single job under suspension-aware scheduling. That is, we show that increasing the cost of a single job does not reduce its own response time. (Note that this is a very basic result that applies to many work-conserving, JLFP schedulers. We don't claim anything about the response time of other jobs.)
Felipe Cerqueira authored1) Definition of a generic model for job suspensions based on received service (e.g., job j_1 should suspend for 4ms as soon as service reaches 5ms). 2) Definition of the dynamic suspension model (i.e., cumulative suspension of job j_1 <= X). 3) Analysis of suspension-aware scheduling by inflation of job costs (via schedule reduction). In the literature, this is called suspension-oblivious analysis. 4) Analysis of suspension-aware scheduling by adjusting job jitter (via schedule reduction). 5) Proof of (weak) sustainability of job costs under suspension-aware scheduling. We show that if we increase the costs of all jobs while reducing their suspension times in a certain way, the response times of all jobs do not decrease. This has an important implication regarding worst-case schedules: if some schedulability analysis already accounts for the fact that job suspension times can vary from 0 to the task suspension bound, then it's perfectly safe to assume that jobs execute for their WCET. 6) Proof of sustainability of the cost of a single job under suspension-aware scheduling. That is, we show that increasing the cost of a single job does not reduce its own response time. (Note that this is a very basic result that applies to many work-conserving, JLFP schedulers. We don't claim anything about the response time of other jobs.)
reduction_properties.v 36.15 KiB