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

From a spec readability PoV, it's unfortunate that the policy that is
being respected doesn't show up in the code. The subject of definitions
should show up as an explicit argument, even if it is implicit
everywhere else. This is however difficult to realize for the current
`respects_policy_at_preemption_time` predicate due to difficulties with
coercion technicalities (see further details below).

Therefore, instead of `respects_policy_at_preemption_time`, we now have:

* `respects_JLDP_policy_at_preemption_point`
* `respects_JLFP_policy_at_preemption_point`
* `respects_FP_policy_at_preemption_point`

Further details: RT-PROOFS/rt-proofs!188 (comment 78569)

Closes: #82

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

This ensures all hypotheses in behavior have corresponding trivial lemmas
in `analysis.facts.all` that enable to exploit them, which makes them 
easier to discover with `Search`.

This also makes the code more robust to potential changes in the precise way
these hypotheses are stated.

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

This commit renames scope [basic_facts] into [basic_rt_facts] to
highlight the that lemmas collected in the scope are real-time (rt)
theory lemmas.

These new tactics are just shorthand for [(e)auto with basic_rt_facts].

It was a parameter but that wasn't of any use,
it was just making everything more noisy.

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

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]

Martin Constantino–Bodin authored 4 years ago and Björn Brandenburg committed 3 years ago

... instead of `service_in`, to mirror the way
the primitive `scheduled_on` is used to realize
`scheduled_in`.

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

There are quite a few places where hypotheses about the task of a job are simply stated as equality (even though a proper predicate exists). This patch replaces the equalities with the predicate.

This way, an addition in external libraries
cannot shadow a definition in Prosa.

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

Provide an RTA for FIFO scheduling on ideal uniprocessors based on an
instantiation of abstract RTA. The provided RTA is works for tasks
described by arbitrary arrival curves and is independent of the
workload's preemption model (since FIFO schedules are necessarily
non-preemptive). 

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

I think that this experiment was not successful. These lemmas can be
easily replaced by ssreflect tactics. Also, they encourage to write
proofs that are harder to maintain.

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

...to match the description in the aRTA paper.

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

The lemma [instantiated_busy_interval_equivalent_edf_busy_interval] actually does not depend on EDF.

Currently, aRTA required [F] to be solution of equation
[A + F = task_rtct + IBF A (A + F)], this commit relaxes
this assumption to [A + F >= task_rtct + IBF A (A + F)]

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

Added helper lemmas relating `valid_schedule` to job execution hps with hint.
Removed useless hps in aRTA.

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

Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.

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