Skip to content

Prove existence of abstract busy interval

Sergey Bozhko requested to merge sbozhko/rt-proofs:abstract-bi-exists into master

Proofs of existence for busy intervals are usually quite long. They also depend on specific scheduling policy and preemption model. This leads to some unnecessary duplication. This commit introduces a proof of existence for abstract busy interval. The idea is to instantiate this proof for specific policies removing the duplication.

Merge request reports