make the policy explicit in policy-compliance predicates
From a spec readability PoV, it's unfortunate that the policy that is being respected doesn't show up in the code. The subject of definitions should show up as an explicit argument, even if it is implicit everywhere else. This is however difficult to realize for the current `respects_policy_at_preemption_time` predicate due to difficulties with coercion technicalities (see further details below). Therefore, instead of `respects_policy_at_preemption_time`, we now have: * `respects_JLDP_policy_at_preemption_point` * `respects_JLFP_policy_at_preemption_point` * `respects_FP_policy_at_preemption_point` Further details: RT-PROOFS/rt-proofs!188 (comment 78569) Closes: #82
Showing
- analysis/facts/busy_interval/priority_inversion.v 2 additions, 2 deletionsanalysis/facts/busy_interval/priority_inversion.v
- analysis/facts/edf_definitions.v 3 additions, 3 deletionsanalysis/facts/edf_definitions.v
- analysis/facts/priority/edf.v 1 addition, 1 deletionanalysis/facts/priority/edf.v
- analysis/facts/priority/fifo.v 1 addition, 1 deletionanalysis/facts/priority/fifo.v
- analysis/facts/priority/sequential.v 2 additions, 2 deletionsanalysis/facts/priority/sequential.v
- implementation/facts/ideal_uni/prio_aware.v 2 additions, 2 deletionsimplementation/facts/ideal_uni/prio_aware.v
- model/schedule/priority_driven.v 22 additions, 7 deletionsmodel/schedule/priority_driven.v
- results/edf/optimality.v 1 addition, 1 deletionresults/edf/optimality.v
- results/edf/rta/bounded_nps.v 1 addition, 1 deletionresults/edf/rta/bounded_nps.v
- results/edf/rta/floating_nonpreemptive.v 1 addition, 1 deletionresults/edf/rta/floating_nonpreemptive.v
- results/edf/rta/fully_nonpreemptive.v 1 addition, 1 deletionresults/edf/rta/fully_nonpreemptive.v
- results/edf/rta/fully_preemptive.v 1 addition, 1 deletionresults/edf/rta/fully_preemptive.v
- results/edf/rta/limited_preemptive.v 1 addition, 1 deletionresults/edf/rta/limited_preemptive.v
- results/fifo/rta.v 1 addition, 1 deletionresults/fifo/rta.v
- results/fixed_priority/rta/bounded_nps.v 2 additions, 2 deletionsresults/fixed_priority/rta/bounded_nps.v
- results/fixed_priority/rta/floating_nonpreemptive.v 2 additions, 2 deletionsresults/fixed_priority/rta/floating_nonpreemptive.v
- results/fixed_priority/rta/fully_nonpreemptive.v 2 additions, 2 deletionsresults/fixed_priority/rta/fully_nonpreemptive.v
- results/fixed_priority/rta/fully_preemptive.v 2 additions, 2 deletionsresults/fixed_priority/rta/fully_preemptive.v
- results/fixed_priority/rta/limited_preemptive.v 2 additions, 2 deletionsresults/fixed_priority/rta/limited_preemptive.v
Loading
Please register or sign in to comment