Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Source project has a limited visibility.
-
Felipe Cerqueira authored
- Add generic definition of job suspension based on the cumulative service - Define the dynamic suspension model (based on task suspension bounds) - Add suspension semantics for uniprocessor schedules - Formalize reduction from suspension-aware schedule to suspension-oblivious schedule by inflating costs (works with JLDP policies and non-unique priorities) - Formalize suspension-oblivious FP RTA using the reduction - Add implementation of a concrete suspension-aware scheduler - Test suspension-oblivious FP RTA with an actual task set - Add simpler definition for JLFP policies - Generalize busy interval lemmas from FP to JLFP scheduling
Felipe Cerqueira authored- Add generic definition of job suspension based on the cumulative service - Define the dynamic suspension model (based on task suspension bounds) - Add suspension semantics for uniprocessor schedules - Formalize reduction from suspension-aware schedule to suspension-oblivious schedule by inflating costs (works with JLDP policies and non-unique priorities) - Formalize suspension-oblivious FP RTA using the reduction - Add implementation of a concrete suspension-aware scheduler - Test suspension-oblivious FP RTA with an actual task set - Add simpler definition for JLFP policies - Generalize busy interval lemmas from FP to JLFP scheduling