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

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

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

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.

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.

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

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.

improve comments, fix names, move some stuff around

This is not yet the final organization, but already an improvement.

Move main high-level results to separate top-level `results` module.
Rationale: Let's make it very clear where to find the main, high-level
results in Prosa, and at the same time let's declutter the analysis
namespace.

Other notable change, apart from moving files around:

- move two key analysis definitions to analysis.definitions
- split RBF definition and facts into separate files
- move facts about ideal schedule to ideal_schedule.v

With proper re-exports everywhere, this is no longer necessary.

The Prosa notion of priority-driven scheduling depends on the
preemption model. That is ok; any theory that doesn't want to deal
with non-preemptive sections can simply Require Export the fully
preemptive model and be done with it.

By our newly adopted convention, the model/ module should not depend on analysis facts.

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions FP models