See: https://github.com/cpitclaudel/alectryon

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

A standard mechanism for enforcing sequentiality of job execution is to use a readiness predicate that ensures that a job is not ready until all prior jobs of the same task are completed.

This patch introduces such predicates.

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

With help from Marco Maida <mmaida@mpi-sws.org>, Sergey Bozhko <sbozhko@mpi-sws.org>, Björn Brandenburg <bbb@mpi-sws.org>.

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.

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

...and some supporting theory. This will be needed to handle arrival curves extrapolated from a finite prefix.

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

Completion sequences are defined (as arrival sequences) from an arrival sequence and a schedule.

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].

The definition of busy interval can be generalized
to an arbitrary processor state model without
affecting other parts of the project.

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].

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

max arrival curve + WCET ➔ max RBF
min arrival curve + BCET ➔ min RBF

The vernacular commands Opaque / Transparent change coqtop's prompt
counter without generating a prompt (for whatever reason). The proof
state recorder needs to be aware of this to avoid a out-of-sync
assertion false positive.

For debugging purposes, slow down the interaction with coqtop to maybe
trigger some potential races more reliably.

If coqtop reports a different number of interactions in its prompt
than we provided, we're out of sync.

... to comments and closing braces on lines before bulleted
sub-proofs.

For better debugging support, add

	--parse-only
and

	--parse-only --verbose
modes.

So that we can link them to arrival curves of Network Calculus
in NCCoq.

Don't always "drill to the bottom" and unfold to sums; instead
explicitly make use of the fact that the EDF proof reasons about
finite identical prefixes, which allows staying at a semantically
higher level in the proof.

While at it, switch the file to using the preferred `now` tactical
when closing out proofs (rather than `by`) to avoid emacs indentation
issues.

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.

Can't rely on arg_maxnP just yet.

This change breaks compatibility with mathcomp < 1.10.

There's now also a `findP` in ssreflect's seq library.