Kimaya Bedarkar authored 2 years ago and Björn Brandenburg committed 2 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: !188 (comment 78569)

Closes: #82

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

This ensures all hypotheses in behavior have corresponding trivial lemmas
in `analysis.facts.all` that enable to exploit them, which makes them 
easier to discover with `Search`.

This also makes the code more robust to potential changes in the precise way
these hypotheses are stated.

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

Deprecation only works for notations, it is a noop on definitions.
There is now a warning in Coq, https://github.com/coq/coq/pull/15760
to avoid this in future releases.

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

Martin Constantino–Bodin authored 3 years ago and Björn Brandenburg committed 3 years ago

- add mathcomp-zify to esy
- Make esy work by having all the mathcomp packages
  install in the same place.

Closes: #86

CI is failing as follows:

```
$ opam install coq-mathcomp-zify
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update
The following dependencies couldn't be met:
  - coq-mathcomp-zify -> coq-mathcomp-algebra < 1.14~
      not available because the package is pinned to version 1.14.0
No solution found, exiting
```

coq-mathcomp-algebra and coq-mathcomp-fingroup re-installed when
installing coq-mathcomp-zify, so don't remove them in the first place

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

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

The default works just fine (nowadays), so let's use that.

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.

As Pierre pointed out in [MR187](!187),
we don't want updates in any of our dependencies to accidentally
shadow Prosa symbols. Hence, always import Prosa modules last to make
sure Prosa symbols "win" any name clashes.

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

Provide an RTA for FIFO scheduling on ideal uniprocessors based on an
instantiation of abstract RTA. The provided RTA is works for tasks
described by arbitrary arrival curves and is independent of the
workload's preemption model (since FIFO schedules are necessarily
non-preemptive). 

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

* Added a lemma for proving `rbf` at `\varepsilon` is more than 0. This is a general fact which can be used in the FIFO RTA to simplify a proof. 
* Changed `1` to `\varepsilon` in one of the existing RBF lemmas for uniformity.