We've had problems with spurious CI failures and unexpected recompilation of .vo files. Somehow the collection of .vo files in the build stage for reuse in the processing stage is not working properly. This MR simplifies the CI setup to compile, build the documentation, and validate all in one job.

It also disables builds with development versions of Coq and mathcomp (nobody was looking at this output anyway). 

Busy intervals by definition always include the job arrival time, so
stating `t1 <= job_arrival j < t2` explicitly is not required.

Closes: #93

- remove some needless `Let` bindings
- use coqdoc sectioning to expose structure in outline

Mariam Vardishvili authored 2 years ago and Björn Brandenburg committed 2 years ago

Modify the EDF blocking bound so that the arrival offset of the
job under analysis is taken into account when considering from
which task a lower-priority job that is causing arrival-blocking
may stem.

With contributions by Kimaya Bedarkar, Sergey Bozhko,
and Björn Brandenburg.

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

Currently, we have lemmas stating that `task_rbf` at `\vareosilon` is greater than equal to task cost, and `task_rbf` is monotone. I combined these two lemmas to state that `tsk_rbf` at any point greater than `0` is greater than task cost. I find that this fact is regularly required in proofs and, therefore, would be good to have in the facts folder.

Marco Maida authored 2 years ago and Björn Brandenburg committed 2 years ago

This commit defines and adds facts about a concrete arrival sequence in
which tasks release jobs "as quickly as possible" as allowed by their
respective arrival-curve constraints. This maximal arrival sequence is
used in POET to generate assumption-less certificates.

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 2 years ago

leq_trans and leq_addr seem to be enough.

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

Too specific.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 2 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 2 years ago and Björn Brandenburg committed 2 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 2 years ago and Björn Brandenburg committed 2 years ago

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

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

Rename the type-class parameter to `job_preemptive_points` to avoid a
name clash with the the definition of the same name.

Keep `JobPreemptionPoints` to match `TaskPreemptionPoints`. This does
not  result in a name clash.