Kimaya Bedarkar authored 2 years ago and Björn Brandenburg committed 2 years ago

The current definitions of `respects_JLFP_policy_at_preemption_time`
and `respects_FP_policy_at_preemption_time` use the predicate
`hep_job_at`. This predicate does not make sense for `JLFP`
and `FP` policies. To avoid this, these definitions should
instead use the definition `respects_JLDP_policy_at_preemption_point`.
Doing this requires coercions from `JLFP` to `JLDP` and from
`FP` to `JLFP`. This patch also introduces these coercions.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

It is exactly big1_eq

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

It was subsumed by sum_nat_gt0

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

Too specific and one liner with existing MathComp lemmas.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

Subsumed by existing MathComp lemmas on division.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 3 years ago

leq_trans and leq_addr seem to be enough.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 3 years ago

Too specific.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

This commit also removes one spurious dependency on ideal uni-processor.
That is, previously file [model/service_of_jobs.v] imported
[processor.ideal], which is wrong, since [model/service_of_jobs.v]
assumes no specific model for processor.

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

As described in #92, the name `np_uni_schedule` is problematic. This
patch renames the scheduler to the more appropriate `pmc_uni_schedule`.

Closes: #92

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

To complement the existing interpretation, add one more instance of
numeric fixed priority that assigns higher priority to lower numeric
values.