• Felipe Cerqueira's avatar
    Major commit: Suspension-Oblivious Analysis · 843c6ffc
    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
    843c6ffc
Name
Last commit
Last update
analysis Loading commit data...
doc Loading commit data...
implementation Loading commit data...
model Loading commit data...
util Loading commit data...
.gitignore Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
create_makefile.sh Loading commit data...