Athul Raj Kollareth authored 2 months ago and Björn Brandenburg committed 1 month ago

Co-authored-by: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>

Generalize:

- `preemption_time`
- priority compliance
- priority facts
- task_schedule.v

... to work with any processor model (and not just ideal
uniprocessors).

Closes: #78

Changes:

* This commit generalises aRTA to "multi-stage" aRTA. The general idea
is explained in file [analysis/abstract/abstract_rta.v]. Short idea is
that the fixpoint equation can be extended to a sequence of fixpoint
equations. Solution to an equation can be used in later fixpoints. This
way one can support move expressive models of execution. The prior
version of aRTA (applicable to ideal uni-processors) is now an
instantiation of the new RTA theorem.

* Interference and Interfering workload are now type-classes. Note that
this changes files in directory [results], since [Variables] were
replaced with [Instance] declarations.

* IBF supports arbitrary parameters (not just relative arrival time).
IBF parametrised by the relative arrival time is not expressive enough
to support restricted-supply analysis. It was generalized to support a
larger class of parameters

* Rename [run to completion] file into [lower bound on service]. The
file was slightly generalized, now  it derives a lower bound on any
pre-defined amount of service.

* Generalize instantiations of interference and interfering workload.
Now, the definitions do not directly destruct the processor state.
Also, definitions for these functions have been made opaque.

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

Currently a lot of files use two hypotheses

```
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
```

instead of the combined `valid_arrival_sequence`.

This patch aims to fix this.

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

* The lemmas concerning the correctness of interference and interfering
  workload for JLFP policies are independent of specific scheduling
  policies. Therefore, these lemmas have been proved in the
  `ideal_jlfp_rta` for any general `JLFP` policies satisfying certain
  conditions.
* The precondition `job_of_task j tsk` in the work-conservation
  definition was unnecessary. This has been removed.
* Two new lemmas have been added to the global facts database. This led
  to the simplification of some proofs.
* Fixed one broken comment in `model.task.sequentiality`.
* Simplified one proof in `ideal_jlfp_rta` since it kept breaking due to
  use of auto-generated names. This required creating one new file -
  `analysis.facts.busy_interval.quiet_time`. Currently, this file
  contains just one lemma that is used in the `ideal_jlfp_rta` file.

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.

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.

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

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

With some misc. cleanups and reorganization thrown in.

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

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

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

No need to keep the two separate as they are tightly coupled anyway,
and the joint file doesn't become too long.

The property is a noun: a model of task sequentiality.