Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

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

Also removes an unnecessary module in rt.util.epsilon.

Make it a statement about scheduled jobs, to match the neighboring
definitions.

Add a [job_ready] parameter to the job model, akin to [pending], that
defines whether a job can be scheduled at a given time in a given schedule.

Then use this new general notion of readiness to define [backlogged].

A pending job may not be ready, whereas (under any reasonable
definition) a ready job ought to be pending, so this definition is
more precise and captures effects such as jitter and self-suspensions.

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

When we were writing the paper on Abstract RTA, we noticed that the response-time recurrence for EDF does not match the known bound.

This merge request tightens the analysis in Prosa to match the known bound.

This patch adds the classic EDF optimality argument: by swapping
allocations, any schedule in which no job misses a deadline can be
transformed into an EDF schedule in which also no job misses a deadline.

Given an interval [a, b), a function f: nat -> T, a predicate P, and a
total, reflexive, transitive relation R, [search_arg f P R a b] will
find the x in [a, b) that is an extremum w.r.t. R among all elements x
in [a, b) for which (f x) satisfies P.

For example, this can be used to search in a schedule for a scheduled
job released before some reference time with the earliest deadline.

This patch adds functions for transforming a given schedule either by
replacing the allocation at a given point, or by swapping the allocations
at two points, together with a bunch of supporting lemmas and service
invariants.

Points before or after an interval are not in the interval...

n + a - b + b - a = n if n >= b

...to match leq_ltn_trans in ssrnat

To allow reasoning about an entire class of types of schedules /
processor modules, it's useful to have named definitions for various
invariants that processor models ensure. Let's collect these centrally
where we introduce processor models and schedules.

Maxime Lesourd authored 5 years ago and Björn Brandenburg committed 5 years ago

Add model definitions for work-conserving and priority-based preemptive schedules.

Maxime Lesourd authored 5 years ago and Björn Brandenburg committed 5 years ago

This is a port (+additions) of the definitions and semantics for arrival curves (model/arrival/curves.v). As a prerequisite, this includes definitions about activations of a task (model/task_arrivals.v).

Two additional definitions which were not found in the original library but will be useful to us in the future:

* in schedule.v : completes_at
* in task_arrivals.v : arrivals_come_from_taskset

simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model

- Consistently use JobType rather than eqType directly.
- Fix the comments style.

Coqdoc produces really nice output - let's automate this.

There's no need to run this for every compiler version; we only care
about the "main" version.

This avoids having to compile ssreflect from scratch each time we want
to compile Prosa.

Thanks to Pierre Roux (Pierre.Roux@onera.fr) for pointing out the
mathcomp Docker images!

From the mathcomp 1.9.0 release notes:

> removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
> improve robustness of by ...; scripts may need to invoke addn0,
> addnS, muln0 or mulnS explicitly where these hints were used
> accidentally.

=> This patch makes these required fixes in Prosa.

While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.