... from `priority_inversion_occurs_only_till_preemption_point`

With contributions by Meenal Gupta <meenalg727@gmail.com>

Pierre Roux authored 1 year ago and Björn Brandenburg committed 1 year ago

This refactoring is the result of a joint effort by Pierre Roux, Sergey Bozhko, and Björn Brandenburg. 

Fixes: #111

Pierre Roux authored 1 year ago and Björn Brandenburg committed 1 year ago

Revise some definitions of interference with too much repetition.

Sergey Bozhko authored 1 year ago and Björn Brandenburg committed 1 year ago

In the lemma I'm working on now, I need a bool version of this
definition. As we discussed, we should avoid two identical versions
(Prop + bool) whenever possible

That coercion just cannot be uniform.

- avoid unfolding coercions all over the place
- reduce unfolding of priority policies
- provide `hep_job` and `hep_job_at` rewriting lemmas
- shorten some generality proofs

... by pulling out common reasoning steps.

Proofs should avoid destruct'ing the busy-window definitions all
over the place. This patch removes all instances of busy-window
`destruct`-ing from the `results` module.

Some old code sites in `analysis` remain. See also #97.

Future code additions should avoid adding new instances of
busy-window `destruct`-ing.

ssreflect doesn't care about these, so we don't want to see them when
importing `util.int`

Meenal Gupta authored 1 year ago and Björn Brandenburg committed 1 year ago

With contributions from Kimaya Bedarkar, Sergey Bozhko, Pierre Roux,
and Björn Brandenburg.