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

The current definitions of `respects_JLFP_policy_at_preemption_time`
and `respects_FP_policy_at_preemption_time` use the predicate
`hep_job_at`. This predicate does not make sense for `JLFP`
and `FP` policies. To avoid this, these definitions should
instead use the definition `respects_JLDP_policy_at_preemption_point`.
Doing this requires coercions from `JLFP` to `JLDP` and from
`FP` to `JLFP`. This patch also introduces these coercions.

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

leq_trans and leq_addr seem to be enough.

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

To complement the existing interpretation, add one more instance of
numeric fixed priority that assigns higher priority to lower numeric
values.

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

Rename the type-class parameter to `job_preemptive_points` to avoid a
name clash with the the definition of the same name.

Keep `JobPreemptionPoints` to match `TaskPreemptionPoints`. This does
not  result in a name clash.

NB: This requires bumping up the "depth" parameter of `rt_auto` and `rt_eauto`.

As a benefit, it becomes possible to automatically use RBFs in the
context of periodic tasks, sporadic tasks, and tasks with arrival
curves. Full example:

```
Require Import prosa.model.task.arrival.periodic.
Require Import prosa.model.task.arrival.periodic_as_sporadic.
Require Import prosa.model.task.arrival.sporadic_as_curve.
Require Import prosa.model.task.arrival.curve_as_rbf.

Section AutoArrivalModelConversion.

  Context {Job : JobType} `{JobArrival Job}.
  Context {Task : TaskType} `{PeriodicModel Task} `{JobTask Job Task}.

  Variable ts : TaskSet Task.

  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.

  Hypothesis H_valid_periods : valid_periods ts.
  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.

  Context `{JobCost Job} `{TaskCost Task}.
  Hypothesis H_valid_costs : jobs_have_valid_job_costs.

  (** Interpret as an RBF. *)

  Goal valid_taskset_request_bound_function ts (task_max_rbf max_arrivals).
  Proof. by rt_auto. Qed.

  Goal taskset_respects_max_request_bound arr_seq ts.
  Proof. rt_eauto. Qed.

End AutoArrivalModelConversion.
```

This commit makes it possible to transparently interpret periodic
tasks as sporadic tasks, and sporadic tasks as tasks with an arrival
curve, such that all proof obligations can satisfied by `rt_auto` and
`rt_eauto`. Full example:

```
Require Import prosa.model.task.arrival.periodic.
Require Import prosa.model.task.arrival.periodic_as_sporadic.
Require Import prosa.model.task.arrival.sporadic_as_curve.

Section AutoArrivalModelConversion.

  Context {Job : JobType} `{JobArrival Job}.
  Context {Task : TaskType} `{PeriodicModel Task} `{JobTask Job Task}.

  Variable ts : TaskSet Task.

  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.

  Hypothesis H_valid_periods : valid_periods ts.

  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.

  (** 1. Interpret as sporadic: *)
  Goal valid_taskset_inter_arrival_times ts.
  Proof. by rt_auto. Qed.

  Goal taskset_respects_sporadic_task_model ts arr_seq.
  Proof. by rt_auto. Qed.

  (** 2. Interpret as an arrival curve. *)
  Goal valid_taskset_arrival_curve ts max_arrivals.
  Proof. by rt_auto. Qed.

  Goal taskset_respects_max_arrivals arr_seq ts.
  Proof. by rt_eauto. Qed.

End AutoArrivalModelConversion.

```

- move all to `prosa.model.task.arrival`
- unify names to `${FOO}_as_${BAR}.v`

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

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

...and many other proofs:

- Simplify proof of conversion_preserves_equivalence
- Simplify proofs in analysis/facts/behavior/service.v
- Simplify proofs in analysis/facts/behavior/deadlines.v
- Simplify proofs in analysis/facts/behavior/arrivals.v
- Fix order of arguments in identical_prefix_inclusion
- Simplify proofs in analysis/facts/behavior/completion.v

This change is semantically a no-op, but it has been argued that not
relying on the bool->nat coercion is more readable.

Closes: #55

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

file for gel

definition for gel

file for gel with basic facts

PriorityPoint and comment changes

PriorityPoint and comment changes

GEL rta with integer offset

Added set in proof

modified proof gel_is_total

spell check

spell check

moved defintion of offset and PriorityPoint, modified hep_job for GEL

spelling mistake

Added citation

spell check

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

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

The existing notion of priority policy compliance is silent on preemptions
that exchange jobs of equal priority. A real scheduler would not engage
in such superfluous preemptions. For some intuitively true properties, it
is natural and necessary to assume the absence of superfluous preemptions.
This patch introduces a definition for this purpose.

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

...and relate it to `nonpreemptive_schedule`, the existing notion of
non-preemptive schedules.

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

`Task` should obviously be of type `TaskType`.