sporadic arrival model (!203) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Merged Björn Brandenburg requested to merge bbb/prosa:wip-arrival-cleanup into master 3 years ago

Apr 07, 2022

CI: fix opam-triggered recompilation · 903e5476
Björn Brandenburg authored 2 years ago

903e5476
demonstrate arrival-model conversion with an example · c4b1ab2d
Björn Brandenburg authored 2 years ago

c4b1ab2d

enable periodic->RBF auto conversion · 5d5f9c72

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

5d5f9c72

enable automatic arrival-model conversion · 87001429

Björn Brandenburg authored 2 years ago

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.

```

87001429

reorganize arrival model conversions · fb114469
Björn Brandenburg authored 2 years ago
```
- move all to `prosa.model.task.arrival`
- unify names to `${FOO}_as_${BAR}.v`
```
fb114469
add sporadic task -> arrival curve interpretation · 26911c64
Björn Brandenburg authored 3 years ago

26911c64
establish an arrival bound for sporadic tasks · 83204784
Björn Brandenburg authored 3 years ago

83204784
add auxiliary lemmas on `{task_}arrivals_between` · 389fd50c
Björn Brandenburg authored 3 years ago

389fd50c
establish that `arrivals_between` is sorted · 485b88ca
Björn Brandenburg authored 3 years ago

485b88ca
add lemma on `div_ceil` on integer multiples · d6ce34a8
Björn Brandenburg authored 3 years ago

d6ce34a8
clean up facts.sporadic.arrival_times · 6eb2683e
Björn Brandenburg authored 3 years ago

6eb2683e
restructure sporadic task facts · c0e95f81
Björn Brandenburg authored 3 years ago

c0e95f81
sporadic task analysis: remove unneeded TaskMaxInterArrival · d96bdaad
Björn Brandenburg authored 3 years ago

d96bdaad
sporadic tasks analysis: remove unnecessary offset parameter · f7a31570
Björn Brandenburg authored 3 years ago
```
Arguments about sporadic tasks do not reason about offsets as future
arrival times are unknown.
```
f7a31570

sporadic arrival model

Merge request reports

Activity