LailaElbeheiry authored 4 years ago and Björn Brandenburg committed 4 years ago

This commit connects the two ways with which one can specify that a
schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
and the `respects_policy_at_preemption_point` with the EDF priority
policy predicate. We connect these two definitions by showing that
they're equivalent. We then restate the optimality proof of EDF
schedules using the proven equivalence.

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

The names for job's and task's run-to-completion
threshold functions are so long that it often gets
in the way of writing theorems and proofs. As
a compromise between verbosity and convenience it
was decided to rename [task_run_to_completion_threshold]
to [task_rtct] and [job_run_to_completion_threshold]
to [job_rtct].

Note that the prior definition of [sequential_tasks]
did not differentiate between a job coming from the
arrival sequence and any other job. However, all
computable properties (such as [job_respects_task_rtc,
valid_preemption_model, arrivals_have_valid_job_costs,
all_deadlines_of_arrivals_met]) are stated exclusively
for jobs from the arrival sequence. In order to make
the definition of [sequential_tasks] compatible with
computable properties, we add preconditions
[arrives_in arr_seq j1] and [arrives_in arr_seq j2].

Before mathcomp 1.11.0 (which requires Coq 8.12), case analysis
doesn't automatically rewrite destructed `minn` premises, so "try"
this manually until we drop support for mathcomp 1.11.0.

In anticipation of future reorganization efforts by Sophie, there's no
point in keeping the two kinds of definitions separate.

Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.

The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.