clean up RBF and related definitions and proofs
Co-authored-by:Kimaya Bedarkar <kbedarka@mpi-sws.org> Co-authored-by:
Björn Brandenburg <bbb@mpi-sws.org>
Showing
- analysis/abstract/IBF/task.v 15 additions, 16 deletionsanalysis/abstract/IBF/task.v
- analysis/abstract/ideal/abstract_seq_rta.v 1 addition, 2 deletionsanalysis/abstract/ideal/abstract_seq_rta.v
- analysis/abstract/restricted_supply/bounded_bi/aux.v 3 additions, 2 deletionsanalysis/abstract/restricted_supply/bounded_bi/aux.v
- analysis/abstract/restricted_supply/bounded_bi/edf.v 3 additions, 1 deletionanalysis/abstract/restricted_supply/bounded_bi/edf.v
- analysis/definitions/request_bound_function.v 43 additions, 77 deletionsanalysis/definitions/request_bound_function.v
- analysis/facts/busy_interval/carry_in.v 5 additions, 9 deletionsanalysis/facts/busy_interval/carry_in.v
- analysis/facts/busy_interval/existence.v 2 additions, 2 deletionsanalysis/facts/busy_interval/existence.v
- analysis/facts/model/dbf.v 12 additions, 40 deletionsanalysis/facts/model/dbf.v
- analysis/facts/model/rbf.v 218 additions, 236 deletionsanalysis/facts/model/rbf.v
- analysis/facts/model/workload.v 23 additions, 62 deletionsanalysis/facts/model/workload.v
- analysis/facts/priority/fifo_ahep_bound.v 3 additions, 3 deletionsanalysis/facts/priority/fifo_ahep_bound.v
- analysis/facts/priority/jlfp_with_fp.v 8 additions, 9 deletionsanalysis/facts/priority/jlfp_with_fp.v
- analysis/facts/workload/edf_athep_bound.v 5 additions, 7 deletionsanalysis/facts/workload/edf_athep_bound.v
- model/aggregate/workload.v 36 additions, 55 deletionsmodel/aggregate/workload.v
- results/elf/rta/bounded_pi.v 8 additions, 6 deletionsresults/elf/rta/bounded_pi.v
- results/fixed_priority/rta/bounded_pi.v 3 additions, 3 deletionsresults/fixed_priority/rta/bounded_pi.v
- results/gel/rta/bounded_pi.v 7 additions, 7 deletionsresults/gel/rta/bounded_pi.v
- results/rs/fifo/bounded_nps.v 0 additions, 3 deletionsresults/rs/fifo/bounded_nps.v
Loading
Please register or sign in to comment