General readiness, take two

A revised version of !36 (closed), rebased on top of current master and addressing the comments raised in the discussion of the first version.

NOTE: I have changed the definition of "completed jobs don't execute" to make it more uniform and to be able to prove that "only ready jobs execute" implies that "completed jobs don't execute".

I think the old definition is an artifact of history and does not generalize well. For instance, on non-uniform speed processors, what if a job receives more than remaining_cost units of service in the last time instant that it is scheduled? In such a case, service <= cost is not actually true. So let's not bake it into a fundamental part of the library.

The invariant service <= cost is true, however, if we know service_at <= 1 (i.e., a unit-speed model), and hence this is now proved as a lemma in facts/completion.v.

CC: @sophie @mlesourd @proux @sbozhko

added 1 commit

• e528641b - documentation fix

Compare with previous version

added 1 commit

• 1a6695de - fix typos

Compare with previous version

added 1 commit

• 0e8920d7 - clean up basic_readiness_compliance proof

Compare with previous version

added 1 commit

• 9cbf3a7f - fix comment

Compare with previous version

added 10 commits

• 91869441 - note that ideal processor model provides unit service
• 3fbb1eda - define [backlogged] in terms of job readiness
• 1aa2ea08 - prove jobs must arrive to be ready
• a63ca8f7 - make definition of completed_jobs_dont_execute uniform
• b59b3d3a - prove ready jobs are incomplete
• 0ceae791 - note equivalence of assumptions in case of basic readiness
• eb957144 - fix fallout from definition change in facts/completion.v
• 37e9bdac - relate ideal progress model with job completion
• 34c14244 - fix definition change fallout in EDF transformation analysis
• 0fbee8da - fix definition change fallout in swap analysis

Compare with previous version

resolved all threads

changed the description

unmarked as a Work In Progress

I have finished the missing proof and cleaned up the branch. This is now ready to go in.

Unless there are objections, I would like to merge this asap. @sophie? @mlesourd?

OK for me. From what I understand, it would be nice to have a discussion about what should be a type class and what not but this is not blocking here.

Thanks for the quick feedback.

it would be nice to have a discussion about what should be a type class and what not

Let's put that on the agenda for discussion at the fall meeting.

I'm fine with the merge request.

merged