Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • RT-PROOFS/rt-proofs
  • sophie/rt-proofs
  • fstutz/rt-proofs
  • sbozhko/rt-proofs
  • fradet/rt-proofs
  • mlesourd/rt-proofs
  • xiaojie/rt-proofs
  • LailaElbeheiry/rt-proofs
  • ptorrx/rt-proofs
  • proux/rt-proofs
  • LasseBlaauwbroek/rt-proofs
  • krathul/rt-proofs
12 results
Show changes
Commits on Source (587)
487 additional commits have been omitted to prevent performance issues.
Hide whitespace changes
Inline Side-by-side
Showing
with 3810 additions and 108 deletions
.ackrc
View file @ a162d510
......@@ -2,5 +2,5 @@
# See https://beyondgrep.com/ for details.
# Ignore misc files generated by the build process
--ignore-file=ext:glob,aux
--ignore-dir=html
\ No newline at end of file
--ignore-file=ext:glob,aux,d,conf,orig
--ignore-dir=html
.gitignore
View file @ a162d510
*.d
*.glob
*.vo
*.vos
*.vok
*.html
/html
*.aux
Makefile*
Makefile.coq*
Makefile.conf
*.crashcoqide
*.v#
*.cache
*~
*.swp
*.orig
*/.#*
#*#
......@@ -16,3 +20,7 @@ Makefile*
*.DS_Store
/proof-state
/with-proof-state
/html-alectryon
_esy
esy.lock/
_CoqProject
.gitlab-ci.yml
View file @ a162d510
###################### Global Config ######################
workflow:
rules:
- if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
- if: '$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS'
when: never
- if: '$CI_COMMIT_BRANCH'
stages:
- build
- process
.build:
stage: build
image: mathcomp/mathcomp:${CI_JOB_NAME}
script:
- ./create_makefile.sh
- make -j ${NJOBS}
###################### Rules and Scripts ##################
1.9.0-coq-8.10:
extends: .build
# Keep track of all compiled output and the build infrastructure
artifacts:
name: prosa-build-files
paths:
- _CoqProject
- Makefile
- Makefile.conf
# Ugly hack around https://gitlab.com/gitlab-org/gitlab-runner/issues/2620
- "*/*.vo"
- "*/*/*.vo"
- "*/*/*/*.vo"
- "*/*/*/*/*.vo"
- "*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*/*.vo"
- "*/*.glob"
- "*/*/*.glob"
- "*/*/*/*.glob"
- "*/*/*/*/*.glob"
- "*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*/*.glob"
expire_in: 1 week
.not_in_wip_branches:
rules:
- if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
proof-length:
.only_in_wip_branches:
rules:
- if: ($CI_COMMIT_BRANCH =~ /^wip-.*$/) && ($CI_PIPELINE_SOURCE != "merge_request_event")
.build-common:
stage: build
image: python:3-alpine
script:
- scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
- opam pin add -n -y -k path coq-prosa .
- opam install -y -v -j ${NJOBS} coq-prosa
- opam pin add -n -y -k path coq-prosa-refinements .
- opam install -y -v -j ${NJOBS} coq-prosa-refinements
1.9.0-coq-8.9:
extends: .build
.preferred-stable-version:
image: registry.mpi-sws.org/mathcomp-for-prosa:2.3.0-coq-8.20
1.9.0-coq-dev:
extends: .build
# it's ok to fail with an unreleased version of Coq
allow_failure: true
.build:
image: registry.mpi-sws.org/mathcomp-for-prosa:${CI_JOB_NAME}
extends: .build-common
latest-coq-8.10:
.build-and-test-POET:
extends: .build
# it's ok to fail with an unreleased version of ssreflect
allow_failure: true
validate:
stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.10
needs: ["1.9.0-coq-8.10"]
dependencies:
- 1.9.0-coq-8.10
script: make validate
doc:
stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.10
needs: ["1.9.0-coq-8.10"]
dependencies:
- 1.9.0-coq-8.10
script:
- git clone https://gitlab.mpi-sws.org/RT-PROOFS/POET.git -b POET-for-Prosa-CI-next /tmp/POET
- !reference [.build-common, script]
- mv /tmp/POET .
- cd POET
- pip3 install --break-system-packages -r requirements.txt
- >-
for WORKLOAD in examples/*.yaml;
do
CERT=certs/cert-for-`basename $WORKLOAD`;
echo; echo; echo;
echo "==================";
echo "Testing $WORKLOAD:";
mkdir -p $CERT;
time ./poet -v -o $CERT -j ${NJOBS} -s $WORKLOAD;
done;
.make-html:
script:
- make html -j ${NJOBS}
- mv html with-proofs
......@@ -79,6 +63,33 @@ doc:
- mv html without-proofs
- make htmlpretty -j ${NJOBS}
- mv html pretty
###################### The Jobs ######################
2.2.0-coq-8.19:
extends:
- .build
- .not_in_wip_branches
2.3.0-coq-8.20:
extends:
- .build
- .not_in_wip_branches
POET:
extends:
- .build-and-test-POET
- .preferred-stable-version
- .not_in_wip_branches
compile-and-doc:
stage: build
extends:
- .only_in_wip_branches
- .preferred-stable-version
script:
- make -j ${NJOBS} all
- !reference [.make-html, script]
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
......@@ -87,24 +98,89 @@ doc:
- "pretty/"
expire_in: 1 week
proof-state:
stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.10
needs: ["1.9.0-coq-8.10"]
dependencies:
- 1.9.0-coq-8.10
compile-and-doc-and-validate:
stage: build
extends:
- .not_in_wip_branches
- .preferred-stable-version
script:
- make -j ${NJOBS} all 2>&1 | tee coqc-messages.txt
- if grep -q Warning coqc-messages.txt; then (echo "Please fix all Coq warnings:"; echo "--"; grep -B1 Warning coqc-messages.txt; exit 1); fi
- !reference [.make-html, script]
- scripts/check-axiom-free.sh results
##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
# - make validate 2>&1 | tee validation-results.txt
# - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
- "with-proofs/"
- "without-proofs/"
- "pretty/"
expire_in: 1 week
mangle-names:
stage: build
extends:
- .not_in_wip_branches
- .preferred-stable-version
script:
- make -j ${NJOBS} mangle-names
# Check that proof irrelevance shows up only due to refinements.
compile-and-validate:
stage: build
extends:
- .not_in_wip_branches
- .preferred-stable-version
script:
- find restructuring util -iname *.v | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
- scripts/intersperse-proof-state.py `find restructuring util -iname *.v`
- cd with-proof-state/
- ln -s ../scripts/
- ln -s ../_CoqProject
- ../create_makefile.sh
- make -j ${NJOBS}
- make html -j ${NJOBS} COQDOCEXTRAFLAGS=--plain-comments
- mv html ../with-proofs-and-proof-state
- scripts/check-axiom-free.sh results
##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
# - make validate 2>&1 | tee validation-results.txt
# - scripts/check-validation-output.sh validation-results.txt
proof-length:
stage: build
image: python:3
script:
- make proof-length
spell-check:
extends:
- .not_in_wip_branches
stage: build
image: registry.mpi-sws.org/aspell-ci:2023-03
script:
- make spell
# mathcomp-dev with stable Coq
#coq-8.17:
# extends:
# - .build-dev
# - .not_in_wip_branches
# # it's ok to fail with an unreleased version of ssreflect
# allow_failure: true
# mathcomp-dev with coq-dev
#coq-dev:
# extends:
# - .build-dev
# - .not_in_wip_branches
# # it's ok to fail with an unreleased version of ssreflect and Coq
# allow_failure: true
proof-state:
extends:
- .not_in_wip_branches
stage: build
image: registry.mpi-sws.org/alectryon-ci:2.3.0-coq-8.20
script:
- eval $(opam env)
- make -j ${NJOBS} all
- make -j ${NJOBS} alectryon
artifacts:
name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
paths:
- "with-proofs-and-proof-state/"
- "html-alectryon/"
expire_in: 1 week
.mailmap 0 → 100644
View file @ a162d510
Björn Brandenburg <bbb@mpi-sws.org> Björn Brandenburg <bbb@mpi-sws.org>
Sergey Bozhko <sbozhko@mpi-sws.org> Sergei Bozhko <sbozhko@mpi-sws.org>
Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <gkerfimf@gmail.com>
Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <sbozhko@sws-mpi.org>
Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <f20171026@goa.bits-pilani.ac.in>
Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Kimaya Bedarkar <kbedarka@mpi-sws.org> kbedarka <kbedarka@mpi-sws.org>
Kimaya Bedarkar <kbedarka@mpi-sws.org> kimaya <f20171026@goa.bits-pilani.ac.in>
Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <kbedarka@mpi-sws.org>
Marco Maida <mmaida@mpi-sws.org> Marco Maida <>
Marco Maida <mmaida@mpi-sws.org> mmaida <mmaida@mpi-sws.org>
Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mariamvardishvili@gmail.com>
Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mvardishvili@mpi-sws.org>
Mariam Vardishvili <mariamvardishvili@gmail.com> Mariam Vardishvili <mvardishvili@mpi-sws.org>
Maxime Lesourd <maxime.lesourd@inria.fr> Maxime Lesourd <maxime.lesourd@gmail.com>
Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@ens-lyon.org>
Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@inria.fr>
Pierre Roux <pierre.roux@onera.fr> Pierre Roux <pierre@roux01.fr>
Pierre Roux <pierre.roux@onera.fr> Pierre Roux <proux@mpi-sws.org>
Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <squinton@inrialpes.fr>
Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <sophie.quinton@inria.fr>
Xiaojie GUO <xiaojie.guo@inria.fr> Xiaojie GUO <gxj0303@loic.inrialpes.fr>
Meenal Gupta <meenalg727@gmail.com> Meenal-27 <80755301+Meenal-27@users.noreply.github.com>
LICENSE 0 → 100644
View file @ a162d510
BSD 2-Clause License
Copyright (c) 2014–2022, The Prosa Project & Contributors
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Makefile 0 → 100644
View file @ a162d510
# Makefile for Prosa
COQ_PROJ := _CoqProject
COQ_MAKEFILE := Makefile.coq
FIND_OPTS := . -name '*.v' ! -name '*\#*' ! -path './.git/*' ! -path './with-proof-state/*'
default: prosa
all: allCoqProject
$(MAKE) $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE)
prosa: prosaCoqProject
$(MAKE) $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE)
refinements: refinementsCoqProject
$(MAKE) $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE)
mangle-names: mangle-namesCoqProject
$(MAKE) $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE)
commonCoqProject:
@$(RM) -f $(COQ_PROJ)
@echo "# Automatically created by make, do not edit" > $(COQ_PROJ)
@echo "# (edit Makefile instead)" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@echo "-arg \"-w -notation-overriden,-parsing,-projection-no-head-constant,-ambiguous-paths\"" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
allCoqProject: commonCoqProject
@echo "-R . prosa" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@find $(FIND_OPTS) \
-print | scripts/module-toc-order.py >> $(COQ_PROJ)
prosaCoqProject: commonCoqProject
@echo "-R . prosa" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@find $(FIND_OPTS) \
! -path './implementation/refinements/*' \
-print | scripts/module-toc-order.py >> $(COQ_PROJ)
refinementsCoqProject: commonCoqProject
@echo "-R implementation/refinements prosa.implementation.refinements" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@find $(FIND_OPTS) \
-path './implementation/refinements/*' \
-print | scripts/module-toc-order.py >> $(COQ_PROJ)
mangle-namesCoqProject: commonCoqProject
@echo "-arg \"-mangle-names __\"" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@echo "-R . prosa" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ)
@find $(FIND_OPTS) \
-print | scripts/module-toc-order.py >> $(COQ_PROJ)
$(COQ_MAKEFILE): $(COQ_PROJ)
@coq_makefile -f $< -o $@ COQDOCEXTRAFLAGS = "--parse-comments --external https://math-comp.github.io/htmldoc/ mathcomp --external mathcomp https://math-comp.github.io/htmldoc/"
install htmlpretty clean cleanall validate alectryon: $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE) $@
html gallinahtml: $(COQ_MAKEFILE)
$(MAKE) -f $(COQ_MAKEFILE) $@
@# Prosa hack: let's tweak the style a bit
@sed -i.bak "s/#90bdff/#eeeeee/" html/coqdoc.css
@rm html/coqdoc.css.bak
%.vo: %.v
$(MAKE) -f $(COQ_MAKEFILE) $@
vacuum: allCoqProject cleanall
@echo 'VACUUMING *.vo *.glob .*.aux <empty directories>'
@find . -depth \( -iname '*.vo' -or -iname '*.glob' -or -iname '.*.aux' \) ! -path './.git/*' -delete
@find . -depth -type d -empty ! -path './.git/*' -delete
macos-clean:
@echo 'CLEAN .DS_Store'
@find . -depth -iname '.DS_Store' ! -path './.git/*' -delete
spell:
./scripts/flag-typos-in-comments.sh `find . -iname '*.v'`
./scripts/flag-typos-in-Markdown.sh `find . -iname '*.md'`
proof-length:
./scripts/proofloc.py --check `find . -iname '*.v'`
distclean: cleanall
$(RM) $(COQ_PROJ)
help:
@echo "You can run:"
@echo
@echo "'make' or 'make prosa' to build Prosa main development"
@echo "'make refinements' to build the refinement part only"
@echo " (requires the main development to be installed)"
@echo "'make all' to build everything"
@echo
@echo "'make install' to install previously compiled files"
@echo "'make validate' to check and verify all proofs"
@echo
@echo "'make htmlpretty' to build the documentation based on CoqdocJS"
@echo " (can hide/show proofs)"
@echo "'make gallinahtml' to build the documentation without proofs"
@echo "'make html' to build the documentation with all proofs"
@echo
@echo "'make clean' to remove generated files"
@echo "'make vacumm' to clean .vo .glob .aux files and empty dirs"
@echo "'make macos-clean' to clean macos' .DS_Store dirs"
@echo "'make distclean' to remove all generated files"
@echo
@echo "'make mangle-names' to compile with mangle-names option"
@echo "'make spell' to run a spell checker on comments and Markdown files"
@echo "'make proof-length' to flag too-long proofs"
@echo
.PHONY: all prosa refinements mangle-names mangle-namesCoqProject
.PHONY: commonCoqProject allCoqProject prosaCoqProject refinementsCoqProject
.PHONY: install html gallinahtml htmlpretty clean cleanall validate alectryon
.PHONY: vacuum macos-clean spell proof-length distclean help
Makefile.coq.local 0 → 100644
View file @ a162d510
# Prosa: include pretty documentation targets
include scripts/coqdocjs/Makefile.coqdocjs
include scripts/Makefile.alectryon
# Hack to enable esy support:
#
# In the esy container, $HOME is hidden, but this causes Coq to complain.
# We thus include a dummy $HOME value.
HOME ?= $(DESTDIR)
export HOME
README.md
View file @ a162d510
# Prosa: Formally Proven Schedulability Analysis
This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016. As of 2018, Prosa is primarily being developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (kindly funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016.
From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
## Documentation
Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
- <https://prosa.mpi-sws.org/branches>
## Publications
Please see the [list of publications](http://prosa.mpi-sws.org/documentation.html#publications) on the Prosa project's homepage.
Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
### Classic Prosa
All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
## Directory and Module Structure
The directory and module structure is currently undergoing a fundamental reorganization.
The directory and module structure is organized as follows. First, the main parts, of which there are currently six.
- [classic/](classic/): This module contains the "classic" version of Prosa as first presented at ECRTS'16.
All results published prior to 2020 build on this "classic" version of Prosa.
- [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
- [restructuring/](restructuring/): The new, refactored version of Prosa. Currently still under heavy development. This part of Prosa will soon move out of the `restructuring` namespace.
- [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
- [`model`](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate. These models are *axiomatic* in the sense that they are collections of hypotheses and not necessarily backed by concrete implementations (but see below).
- [`analysis`](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
- [`results`](results/): The `results` namespace contains all **high-level analysis results**.
- [`implementation`](implementation/): This module collects concrete implementations of some of the axiomatic models and scheduling policies to which the results apply. These are used to instantiate (i.e., apply) high-level results in an assumption-free environment for concrete job and task types, which establishes the absence of contradictions in the axiomatic models refined by the implementations.
- [`implementation.refinements`](implementation/refinements/): The refinements needed by [POET](https://drops.dagstuhl.de/opus/volltexte/2022/16336/) to compute with large numbers, based on [CoqEAL](https://github.com/coq-community/CoqEAL).
## Dependencies
Besides Coq itself, Prosa's only external dependency is the ssreflect library of the [Mathematical Components project](https://math-comp.github.io).
Furthermore, there are a couple of additional folders and modules.
Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
- [`util`](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
- [`scripts/`](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
## Compiling Prosa
Assuming ssreflect is available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
## Side-effects
First, create an appropriate `Makefile`.
Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basic lemmas about real-time systems.
```
./create_makefile.sh
Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
```
Prosa overwrites the default obligation tactic of Coq with `idtac`. Refer [`util.tactics`](util/tactics.v) for details.
Alternatively, to avoid compiling the older "classic" Prosa, specify the `--without-classic` option. This can speed up compilation considerably and is a good idea during development. (It's also possible to *only* compile the "classic" Prosa by specifying the `--only-classic` option, but this is rarely needed.)
## Installation
### With the OCaml Package Manager (`opam`)
Prosa can be installed using [`opam`](https://opam.ocaml.org/) (>= 2.0).
```bash
opam repo add coq-released https://coq.inria.fr/opam/released
# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
opam update
opam install coq-prosa
```
./create_makefile.sh --without-classic
### From Sources with `opam`
OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see `.gitlab-ci.yaml`).
```bash
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam pin add -n -y -k path coq-prosa .
opam install coq-prosa
```
### From Sources With `esy`
Prosa can be installed using the [`esy`](https://esy.sh/) package manager.
#### Installing `esy`
`esy` itself can typically be installed through `npm`.
It should look something like this on most `apt`-based systems:
```bash
sudo apt install npm
sudo npm install --global esy@latest
```
#### Installing Prosa
With `esy` in place, it is easy to compile Prosa in one go. To download and compile all of Prosa's dependencies (including Coq), and then to compile Prosa itself, simply issue the command:
```bash
esy
```
Second, compile the library.
Note that `esy` uses an internal compilation environment, which is not exported to the current shell.
To work within this environment, prefix any command with `esy`: for instance `esy coqide` to run your system’s CoqIDE within the right environment.
Alternatively, `esy shell` opens a shell within its environment.
### Manually From Sources
#### Dependencies
Besides on Coq itself, Prosa depends on
1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io),
2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`, and
3. the [The Coq Effective Algebra Library](https://github.com/coq-community/coqeal) (optional, needed only for POET-related refinements).
These dependencies can be easily installed with OPAM.
```bash
opam install -y coq-mathcomp-ssreflect coq-mathcomp-zify coq-coqeal
```
Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
#### Compiling Prosa
Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa can be done by just typing:
```bash
make -j
```
Depending on how powerful your machine is, this will take a few minutes.
The library can then be installed with:
```bash
make install
```
To compile the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), first install the main Prosa library with the two commands above, then type:
```bash
make refinements
```
The newly compiled files can then be installed with:
```bash
make install
```
## Generating HTML Documentation
The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with the provided `Makefile`:
Once the has been library compiled, the `coqdoc` documentation (as shown on the [web page](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with:
- `make htmlpretty -j` --- pretty documentation based on CoqdocJS (can hide/show proofs),
- `make gallinahtml -j` --- just the specification, without proofs,
- `make html -j` --- full specification with all proofs.
Since Coqdoc requires object files (`*.vo`) as input, please make sure that the code is compilable.
Since `coqdoc` requires object files (`*.vo`) as input, please make sure that the code compiles.
## Commit and Development Rules
......@@ -71,18 +166,18 @@ To make things as smooth as possible, here are a couple of rules and guidelines
1. Always follow the project [coding and writing guidelines](doc/guidelines.md).
2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
3. It's ok (and even recommended) to develop in a (private) dirty branch, but clean up and rebase (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
3. It's okay (and even recommended) to develop in a (private) dirty branch, but please clean up and re-base your branch (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.) as well.
5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:".
5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:".
6. We strive to have only "fast-forward merges" without merge commits, so always rebase your branch to linearize the history before merging. (WIP branches do not need to be linear.)
6. We strive to have only "fast-forward merges" without merge commits, so always re-base your branch to linearize the history before merging. (WIP branches do not need to be linear.)
7. Recommendation: Document the tactics that you use in the [list of tactics](doc/tactics.md), especially when introducing/using non-standard tactics.
8. If something seems confusing, please help with improving the documentation. :-)
9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discusion, please file a ticket.
9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket.
_CoqProject deleted 100644 → 0
View file @ 7b64c4b0
-R . rt -arg "-w -notation-overriden,-parsing"
analysis/README.md 0 → 100644
View file @ a162d510
# Prosa Analysis Library
This module provides virtually all **analysis concepts and definitions** and encapsulates the bulk of the **intermediate proofs** in Prosa.
More precisely, this module collects all definitions that are not needed to define the behavioral semantics (found in [`prosa.behavior`](../behavior)) and that also do not conceptually form part of the task and system model (found in [`prosa.model`](../model)). For example, precise notions of "schedulability," "busy window," or "response time" are clearly analysis concepts and consequently defined here.
The proofs found in this module are "intermediate proofs" in the sense that they are not an end in of themselves; rather, they are a means to enable the proofs of the high-level results provided in the [`prosa.results`](../results) module.
## Structure
The Prosa analysis library is currently organized as follows:
- [`abstract`](./abstract): This provides **abstract RTA** analysis framework, a general and extensible approach to response-time analysis (RTA).
- [`definitions`](./definitions): This folder currently collects all major and minor **analysis definitions** (such as schedulability, priority inversion, etc.).
- [`transform`](./transform): This folder contains procedures for transforming schedules, to be used in proofs that rely on modifying a given reference schedule in some way (e.g., the EDF "swapping argument").
- [`facts`](./facts): Currently the home of virtually all **intermediate proofs**. In particular, [facts.behavior](./facts/behavior) provides a library of basic facts that follow (mostly) directly from Prosa's trace semantics (as given in [`prosa.behavior`](../behavior)).
**NB**: It is expected that the analysis module will be further (re)organized and (re)structured in future versions of Prosa.
## Guidelines
- As a general rule, keep definitions and proofs separate, so that casual readers may read and understand the Prosa specification without encountering intermediate lemmas and proofs.
- Prefer folders with many short files over fewer, longer files.
- In each file that is specific to some system model, explicitly `Require` the specific modules that jointly constitute the assumed system model (e.g., `Require prosa.model.processor.ideal` to express that the results in a file depend on the ideal-uniprocessor assumption).
\ No newline at end of file
analysis/abstract/IBF/supply.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.abstract.abstract_rta.
(** In this module, we define _intra-supply interference_ as a kind of
conditional interference and use it to define an _intra-supply_
interference-bound function ([intra_IBF]). Recall that an
interference-bound function is a function that bounds the
interference experienced by a job of a task under analysis. This
way, the function [intra_IBF] bounds the cumulative interference
ignoring the interference due to a lack of supply.
Here, the term "intra-supply" is inspired by (but not limited to)
reservation-based schedulers, where a job only receives service
within a corresponding reservation. Similarly, intra-supply
interference refers to interference that occurs "inside" the time
instances where supply is present. *)
Section IntraInterferenceBound.
(** Consider any type of job associated with any type of tasks ... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(** ... with arrival times and costs. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Next, we introduce the notions of _intra-supply_ interference
and intra-supply IBF. Using these notions, one can separate the
interference due to the lack of supply from all the other
sources of interference. *)
(** We define intra-supply interference as interference conditioned
on the fact that there is supply. That is, a job [j] experiences
intra-supply interference at a time instant [t] if [j]
experiences interference at time [t] _and_ there is supply at
[t]. *)
Definition intra_interference (j : Job) (t : instant) :=
cond_interference (fun j t => has_supply sched t) j t.
(** We define the cumulative intra-supply interference. *)
Definition cumul_intra_interference j t1 t2 :=
cumul_cond_interference (fun j t => has_supply sched t) j t1 t2.
(** Consider an interference bound function [intra_IBF]. *)
Variable intra_IBF : duration -> duration -> work.
(** We say that intra-supply interference is bounded by [intra_IBF]
iff, for any job [j] of task [tsk], cumulative _intra-supply_
interference within the interval <<[t1, t1 + R)>> is bounded by
[intra_IBF(A, R)].*)
Definition intra_interference_is_bounded_by :=
cond_interference_is_bounded_by
arr_seq sched tsk intra_IBF
(relative_arrival_time_of_job_is_A sched) (fun j t => has_supply sched t).
End IntraInterferenceBound.
analysis/abstract/IBF/supply_task.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.IBF.task.
(** In this module, we define a _task-intra-supply_-interference-bound
function ([task_intra_IBF]). Function [task_intra_IBF] bounds
interference ignoring interference due to lack of supply _and_ due
to self-interference. *)
Section TaskIntraInterferenceBound.
(** Consider any type of job associated with any type of tasks ... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(** ... with arrival times and costs. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task.
(** Assume we are provided with abstract functions characterizing
interference and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Next, we introduce the notions of "task intra-supply
interference" and "task intra-supply IBF". Using these notions,
one can separate the interference due to the lack of supply or
due to self-interference from all the other sources of
interference. *)
(** Let us define a predicate stating that (1) there is supply at
time [t] and (2) the task of a job [j] is _not_ scheduled at a
time instant [t]. *)
Definition nonself_intra (j : Job) (t : instant) :=
(nonself arr_seq sched j t) && has_supply sched t.
(** We define _task intra-supply interference_ as interference
conditioned on the fact that there is supply and there is no
self-interference. *)
Definition task_intra_interference (j : Job) (t : instant) :=
cond_interference nonself_intra j t.
(** Consider an interference bound function [task_intra_IBF]. *)
Variable task_intra_IBF : duration -> duration -> work.
(** We say that task intra-supply interference is bounded by
[task_intra_IBF] iff, for any job [j] of task [tsk], the
cumulative task intra-supply interference within the interval
<<[t1, t1 + R)>> is bounded by [task_intra_IBF(A, R)]. *)
Definition task_intra_interference_is_bounded_by :=
cond_interference_is_bounded_by
arr_seq sched tsk task_intra_IBF
(relative_arrival_time_of_job_is_A sched) nonself_intra.
End TaskIntraInterferenceBound.
analysis/abstract/IBF/task.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.task_schedule.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.abstract.abstract_rta.
(** In this section, we define a notion of _task_ interference-bound
function [task_IBF]. Function [task_IBF] bounds interference that
excludes interference due to self-interference. *)
Section TaskInterferenceBound.
(** Consider any type of job associated with any type of tasks... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(** ... with arrival times and costs. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Next we introduce the notion of _task_ interference.
Intuitively, task [tsk] incurs interference when some of the
jobs of task [tsk] incur interference. As a result, [tsk] cannot
make any progress.
More formally, consider a job [j] of task [tsk]. The task
experiences interference at time [t] if job [j] experiences
interference ([interference j t = true]) and task [tsk] is not
scheduled at time [t]. *)
(** Let us define a predicate stating that the task of a job [j] is
_not_ scheduled at a time instant [t]. *)
Definition nonself (j : Job) (t : instant) :=
~~ task_served_at arr_seq sched (job_task j) t.
(** We define task interference as conditional interference where
[nonself] is used as the predicate. This way, [task_interference
j t] is [false] if the interference experienced by a job [j] is
caused by a job of the same task. *)
Definition task_interference (j : Job) (t : instant) :=
cond_interference nonself j t.
(** Next, we define the cumulative task interference. *)
Definition cumul_task_interference j t1 t2 :=
cumul_cond_interference nonself j t1 t2.
(** Consider an interference bound function [task_IBF]. *)
Variable task_IBF : duration -> duration -> work.
(** We say that task interference is bounded by [task_IBF] iff for
any job [j] of task [tsk] cumulative _task_ interference within
the interval <<[t1, t1 + R)>> is bounded by function [task_IBF(tsk, A, R)]. *)
Definition task_interference_is_bounded_by :=
cond_interference_is_bounded_by
arr_seq sched tsk task_IBF (relative_arrival_time_of_job_is_A sched) nonself.
End TaskInterferenceBound.
(** In the following section, we prove that, under certain assumptions
defined next, the fact that a function [task_IBF tsk A R]
satisfies hypothesis [task_interference_is_bounded_by] implies
that a function [(task_rbf (A + ε) - task_cost tsk) + task_IBF tsk
A R] satisfies [job_interference_is_bounded_by]. In other words,
the self-interference can be bounded by the term [(task_rbf (A +
ε) - task_cost tsk)], where [A] is the relative arrival time of a
job under analysis. *)
Section TaskIBFtoJobIBF.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context {jc : JobCost Job}.
(** Consider any kind of ideal uni-processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Consider any valid arrival sequence with consistent, non-duplicate arrivals...*)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any ideal schedule of this arrival sequence. *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set. *)
Variable ts : list Task.
(** Let [tsk] be any task in ts that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Let [max_arrivals] be a family of valid arrival curves, i.e.,
for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and (2) it is a monotonic function that equals
[0] for the empty interval [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Let us abbreviate task [tsk]'s RBF for clarity. *)
Let task_rbf := task_request_bound_function tsk.
(** When assuming sequential tasks, we need to introduce an
additional hypothesis to ensure that the values of interference
and workload remain consistent with the priority policy.
To understand why, let us consider a case where the sequential
task assumption does _not_ hold, and then work
backwards. Consider a fully preemptive policy that assigns the
highest priority to the job that was released _last_. Then, if
there is a pending job [j] of a task [tsk], it is not a part of
a busy interval of the next job [j'] of the same task. In this
case, both the interference and the interfering workload of job
[j'] will simply ignore job [j]. Thus, it is possible to have a
quiet time (for [j']) even though [j] is pending.
Now, assuming that our priority policy ensures that tasks are
sequential, the situation described above is impossible (job [j]
will always have a higher-or-equal priority than job [j']).
Hence, we need to rule our interference and interfering workload
instantiations that do not conform to the sequential tasks
assumption.
We ensure the consistency by assuming that, when a busy interval
of a job [j] of task [tsk] starts, both the cumulative task
workload and the task service must be equal within the interval
<<[0, t1)>>. This implies that a busy interval for job [j]
cannot start if there is another pending job of the same task
[tsk].*)
Definition interference_and_workload_consistent_with_sequential_tasks :=
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
job_of_task tsk j ->
job_cost j > 0 ->
busy_interval sched j t1 t2 ->
task_workload_between arr_seq tsk 0 t1
= task_service_of_jobs_in sched tsk (arrivals_between arr_seq 0 t1) 0 t1.
(** To prove the reduction from [task_IBF] to [job_IBF], we need to
ensure that the scheduling policy, interference, and interfering
workload all respect the sequential tasks hypothesis. For this,
we assume that (1) tasks are sequential and (2) functions
interference and interfering_workload are consistent with the
hypothesis of sequential tasks. *)
Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks.
(** Next, we assume that [task_IBF] is a bound on interference
incurred by the task. *)
Variable task_IBF : duration -> duration -> duration.
Hypothesis H_task_interference_is_bounded :
task_interference_is_bounded_by arr_seq sched tsk task_IBF.
(** Before proceed to the main proof, we first show a few simple
lemmas about the completion of jobs from the task considering
the busy interval of the job under consideration. *)
Section CompletionOfJobsFromSameTask.
(** Consider any two jobs [j1] [j2] of [tsk]. *)
Variable j1 j2 : Job.
Hypothesis H_j1_arrives : arrives_in arr_seq j1.
Hypothesis H_j2_arrives : arrives_in arr_seq j2.
Hypothesis H_j1_from_tsk : job_of_task tsk j1.
Hypothesis H_j2_from_tsk : job_of_task tsk j2.
Hypothesis H_j1_cost_positive : job_cost_positive j1.
(** Consider the busy interval <<[t1, t2)>> of job j1. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j1 t1 t2.
(** We prove that if a job from task [tsk] arrived before the
beginning of the busy interval, then it must be completed
before the beginning of the busy interval *)
Lemma completed_before_beginning_of_busy_interval :
job_arrival j2 < t1 ->
completed_by sched j2 t1.
Proof.
move => JA; have /eqP TSK2eq := H_j2_from_tsk.
have [ZERO|POS] := posnP (@job_cost _ jc j2).
{ by rewrite /completed_by /service.completed_by ZERO. }
{ by eapply all_jobs_have_completed_equiv_workload_eq_service => //. }
Qed.
(** Next we prove that if a job is pending after the beginning of
the busy interval <<[t1, t2)>> then it arrives after [t1]. *)
Lemma arrives_after_beginning_of_busy_interval :
forall t,
t1 <= t ->
pending sched j2 t ->
arrived_between j2 t1 t.+1.
Proof.
move => t GE PEND.
apply/andP; split; last first.
{ by move: PEND => /andP [ARR _]; rewrite ltnS. }
rewrite leqNgt; apply/negP => LT.
have L12 := completed_before_beginning_of_busy_interval LT.
apply completion_monotonic with (t' := t) in L12 => //.
by move: PEND => /andP [_ /negP T2].
Qed.
End CompletionOfJobsFromSameTask.
(** In this section we show that there exists a bound for cumulative
interference for any job of task [tsk]. *)
Section BoundOfCumulativeJobInterference.
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider the busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j t1 t2.
(** Let's define [A] as a relative arrival time of job [j] (with
respect to time [t1]). *)
Let A : duration := job_arrival j - t1.
(** Consider an arbitrary time [x] ... *)
Variable x : duration.
(** ... such that [t1 + x] is inside the busy interval ... *)
Hypothesis H_inside_busy_interval : t1 + x < t2.
(** ... and job [j] is not completed by time [t1 + x]. *)
Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + x).
(** In this section, we show that the cumulative interference of
job [j] in the interval <<[t1, t1 + x)>> is bounded by the sum
of the task workload in the interval <<[t1, t1 + A + ε)>> and
the cumulative interference of [j]'s task in the interval
<<[t1, t1 + x)>>. Note that the task workload is computed only
on the interval <<[t1, t1 + A + ε)>>. Thanks to the hypothesis
about sequential tasks, jobs of task [tsk] that arrive after
[t1 + A + ε] cannot interfere with [j]. *)
Section TaskInterferenceBoundsInterference.
(** We start by proving a simpler analog of the lemma that
states that at any time instant <<t ∈ [t1, t1 + x)>> the sum
of [interference j t] and [scheduled_at j t] is no larger
than the sum of [the service received by jobs of task tsk at
time t] and [task_iterference tsk t]. *)
(** Next we consider 4 cases. *)
Section CaseAnalysis.
(** Consider an arbitrary time instant [t] ∈ <<[t1, t1 + x)>>. *)
Variable t : instant.
Hypothesis H_t_in_interval : t1 <= t < t1 + x.
Section Case1.
(** Assume the processor is idle at time [t]. *)
Hypothesis H_idle : is_idle arr_seq sched t.
(** In case when the processor is idle, one can show that
[interference j t = 1, service_at j t = 0]. But since
interference doesn't come from a job of task [tsk]
[task_interference tsk = 1]. Which reduces to [1 ≤
1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_idle :
interference j t + service_at sched j t
<= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
+ task_interference arr_seq sched j t.
Proof.
replace (service_of_jobs_at _ _ _ _) with 0; last first.
{ symmetry; rewrite /service_of_jobs_at /=.
eapply big1; move => j' _.
apply not_scheduled_implies_no_service.
exact: not_scheduled_when_idle. }
have ->: service_at sched j t = 0.
{ apply: not_scheduled_implies_no_service.
exact: not_scheduled_when_idle. }
rewrite addn0 add0n /task_interference /cond_interference.
case INT: (interference j t) => [|//].
rewrite //= lt0b // andbT.
exact: no_task_served_when_idle.
Qed.
End Case1.
Section Case2.
(** Assume a job [j'] from another task is scheduled at time [t]. *)
Variable j' : Job.
Hypothesis H_sched : scheduled_at sched j' t.
Hypothesis H_not_job_of_tsk : ~~ job_of_task tsk j'.
(** If a job [j'] from another task is scheduled at time
[t], then [interference j t = 1, served_at j t = 0]. But
since interference doesn't come from a job of task [tsk]
[task_interference tsk = 1]. Which reduces to [1 ≤
1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_task:
interference j t + service_at sched j t
<= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
+ task_interference arr_seq sched j t.
Proof.
have ARRs : arrives_in arr_seq j'.
{ by apply H_jobs_come_from_arrival_sequence with t. }
rewrite /task_interference /cond_interference.
have ->: service_at sched j t = 0.
{ apply: not_scheduled_implies_no_service; apply/negP => SCHED.
have EQ : j' = j by eapply H_uniprocessor_proc_model.
by subst; move: H_not_job_of_tsk; rewrite H_job_of_tsk. }
case INT: (interference j t) => [|//].
rewrite andbT.
have ->: nonself arr_seq sched j t.
{ eapply job_of_other_task_scheduled' => //.
by move: (H_job_of_tsk) => /eqP ->; apply: H_not_job_of_tsk. }
by clear; lia.
Qed.
End Case2.
Section Case3.
(** Assume a job [j'] of task [tsk] is scheduled at time [t]
but receives no service. *)
Variable j' : Job.
Hypothesis H_sched : scheduled_at sched j' t.
Hypothesis H_not_job_of_tsk : job_of_task tsk j'.
Hypothesis H_serv : service_at sched j' t = 0.
(** If a job [j'] of task [tsk] is scheduled at time [t],
then [interference j t = 1, service_at j t =
0]. Moreover, since interference comes from a job of the
same task [task_interference tsk = 0]. However, in this
case [service_of_jobs of tsk = 1]. Which reduces to [1 ≤
1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_job :
interference j t + service_at sched j t
<= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
+ task_interference arr_seq sched j t.
Proof.
rewrite /task_interference /cond_interference.
have SERVj: service_at sched j t = 0; last rewrite SERVj.
{ have [] := service_is_zero_or_one _ sched j t => // => SERVj.
apply: not_scheduled_implies_no_service; apply/negP => SCHED.
have EQ : j' = j by eapply H_uniprocessor_proc_model.
by subst j'; move: H_serv SERVj => ->.
}
have ->: interference j t = true.
{ have NEQT: t1 <= t < t2
by move: H_t_in_interval => /andP [NEQ1 NEQ2]; apply/andP; split; last apply ltn_trans with (t1 + x).
move: (H_work_conserving j t1 t2 t H_j_arrives H_job_cost_positive (fst H_busy_interval) NEQT) => [Hn _].
apply/negPn/negP; move => CONTR; move: CONTR => /negP CONTR.
by apply Hn in CONTR; move: CONTR; rewrite /receives_service_at SERVj.
}
have /eqP-> : nonself arr_seq sched j t == true.
{ rewrite eqb_id.
apply: job_of_task_not_served => //.
by move: H_job_of_tsk => /eqP ->.
}
by rewrite addnC leq_add => //.
Qed.
End Case3.
Section Case4.
(** Before proceeding to the last case, let us note that the
sum of interference and the service of [j] at [t] always
equals to [1]. *)
Fact interference_and_service_eq_1 :
interference j t + service_at sched j t = 1.
Proof.
have NEQT: t1 <= t < t2
by move: H_t_in_interval => /andP [NEQ1 NEQ2]; apply/andP; split; last apply ltn_trans with (t1 + x).
have [] := service_is_zero_or_one _ sched j t => // => SERVj.
{ rewrite SERVj.
have ->: interference j t = true; last by done.
{ move: (H_work_conserving j t1 t2 t H_j_arrives H_job_cost_positive (fst H_busy_interval) NEQT) => [Hn _].
apply/negPn/negP; move => CONTR; move: CONTR => /negP CONTR.
by apply Hn in CONTR; move: CONTR; rewrite /receives_service_at SERVj.
}
}
{ rewrite SERVj.
have ->: interference j t = false; last by done.
{ move: (H_work_conserving j t1 t2 t H_j_arrives H_job_cost_positive (fst H_busy_interval) NEQT) => [_ Hs].
apply/negP; apply: Hs.
by rewrite /receives_service_at SERVj.
}
}
Qed.
(** Assume that a job [j'] is scheduled at time [t] and receives service. *)
Variable j' : Job.
Hypothesis H_sched : scheduled_at sched j' t.
Hypothesis H_not_job_of_tsk : job_of_task tsk j'.
Hypothesis H_serv : service_at sched j' t = 1.
(** If job [j'] is served at time [t], then [service_of_jobs
of tsk = 1]. With the fact that [interference +
service_at = 1], we get the inequality to [1 ≤ 1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_j :
interference j t + service_at sched j t
<= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
+ task_interference arr_seq sched j t.
Proof.
rewrite interference_and_service_eq_1 -addn1 addnC leq_add //.
rewrite /service_of_jobs_at big_mkcond sum_nat_gt0 filter_predT; apply/hasP.
exists j'; last by rewrite H_not_job_of_tsk.
eapply arrived_between_implies_in_arrivals => //.
apply/andP; split.
- move_neq_up CONTR.
eapply completed_before_beginning_of_busy_interval in CONTR => //.
apply scheduled_implies_not_completed in H_sched => //.
move: H_sched => /negP T; apply: T.
by apply (completion_monotonic _ _ t1) => //; move: (H_t_in_interval); clear; lia.
- rewrite -addn1 leq_add2r /A subnKC //.
have NCOMPL : ~~ completed_by sched j t.
{ by apply: (incompletion_monotonic _ _ _ (t1 + x)) => //; move: (H_t_in_interval); clear; lia. }
clear H_job_j_is_not_completed; apply: scheduler_executes_job_with_earliest_arrival => //.
by rewrite /same_task; move: (H_job_of_tsk) (H_not_job_of_tsk) => /eqP -> /eqP ->.
Qed.
End Case4.
(** We use the above case analysis to prove that any time
instant <<t ∈ [t1, t1 + x)>> the sum of [interference j t]
and [scheduled_at j t] is no larger than the sum of [the
service received by jobs of task tsk at time t] and
[task_iterference tsk t]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference:
interference j t + service_at sched j t
<= service_of_jobs_at sched (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + A + ε)) t
+ task_interference arr_seq sched j t.
Proof.
rewrite /task_interference /cond_interference.
have [IDLE|SCHED] := boolP (is_idle arr_seq sched t).
{ by apply interference_plus_sched_le_serv_of_task_plus_task_interference_idle. }
{ apply is_nonidle_iff in SCHED; move: SCHED => // => [[s SCHEDs]].
have ARRs: arrives_in arr_seq s by done.
have [TSKEQ|TSKNEQ] := boolP (job_of_task tsk s); last first.
{ exact: interference_plus_sched_le_serv_of_task_plus_task_interference_task. }
{ have [] := service_is_zero_or_one _ sched s t => // => SERVj.
{ exact: interference_plus_sched_le_serv_of_task_plus_task_interference_job. }
{ exact: interference_plus_sched_le_serv_of_task_plus_task_interference_j. }
}
}
Qed.
End CaseAnalysis.
(** Next we prove cumulative version of the lemma above. *)
Lemma cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference:
cumulative_interference j t1 (t1 + x)
<= (task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x)) + cumul_task_interference arr_seq sched j t1 (t1 + x).
Proof.
have j_is_in_arrivals_between: j \in arrivals_between arr_seq t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals => //.
by apply/andP; split; last rewrite /A subnKC // addn1.
}
rewrite /task_service_of_jobs_in /service_of_jobs.task_service_of_jobs_in /service_of_jobs exchange_big //=.
rewrite -(leq_add2r (\sum_(t1 <= t < (t1 + x)) service_at sched j t)).
rewrite [X in _ <= X]addnC addnA subnKC; last first.
{ rewrite (exchange_big _ _ (arrivals_between _ _ _)) /= (big_rem j) //=.
by rewrite H_job_of_tsk leq_addr. }
rewrite -big_split -big_split //=.
rewrite big_nat_cond [X in _ <= X]big_nat_cond leq_sum //; move => t /andP [NEQ _].
rewrite -(leqRW (interference_plus_sched_le_serv_of_task_plus_task_interference _ _ )) => //.
Qed.
(** As the next step, the service terms in the inequality above
can be upper-bound by the workload terms. *)
Lemma serv_of_task_le_workload_of_task_plus:
task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x) + cumul_task_interference arr_seq sched j t1 (t1 + x)
<= (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference arr_seq sched j t1 (t1 + x).
Proof.
have j_is_in_arrivals_between: j \in arrivals_between arr_seq t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals => //.
by apply/andP; split; last rewrite /A subnKC // addn1. }
rewrite leq_add2r.
rewrite /task_workload_between/task_service_of_jobs_in/task_service_of_jobs_in/service_of_jobs.
rewrite (big_rem j) ?[X in _ <= X - _](big_rem j) //=; auto using j_is_in_arrivals_between.
rewrite H_job_of_tsk addnC -addnBA// [X in _ <= X - _]addnC -addnBA//.
rewrite !subnn !addn0.
exact: service_of_jobs_le_workload.
Qed.
(** Finally, we show that the cumulative interference of job [j]
in the interval <<[t1, t1 + x)>> is bounded by the sum of
the task workload in the interval [t1, t1 + A + ε) and the
cumulative interference of [j]'s task in the interval <<[t1,
t1 + x)>>. *)
Lemma cumulative_job_interference_le_task_interference_bound:
cumulative_interference j t1 (t1 + x)
<= (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference arr_seq sched j t1 (t1 + x).
Proof.
by apply leq_trans with
(task_service_of_jobs_in sched tsk (arrivals_between arr_seq t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x)
+ cumul_task_interference arr_seq sched j t1 (t1 + x));
[ apply cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference
| apply serv_of_task_le_workload_of_task_plus].
Qed.
End TaskInterferenceBoundsInterference.
(** We use the lemmas above to obtain the bound on [interference]
in terms of [task_rbf] and [task_interference]. *)
Lemma cumulative_job_interference_bound :
cumulative_interference j t1 (t1 + x)
<= (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference arr_seq sched j t1 (t1 + x).
Proof.
set (y := t1 + x) in *.
have IN: j \in arrivals_between arr_seq t1 (t1 + A + ε).
{ apply: arrived_between_implies_in_arrivals => //.
by apply/andP; split; last rewrite /A subnKC // addn1. }
apply leq_trans with (
task_workload_between arr_seq tsk t1 (t1+A+ε) - job_cost j + cumul_task_interference arr_seq sched j t1 y
).
- by apply cumulative_job_interference_le_task_interference_bound.
- rewrite leq_add2r /A.
have -> : (t1 + (job_arrival j - t1) + ε) = (t1 + (job_arrival j - t1 + ε)) by lia.
apply: task_rbf_without_job_under_analysis => //=.
by move: IN => /[!job_arrival_in_bounds] // -[]; lia.
Qed.
End BoundOfCumulativeJobInterference.
(** Finally, we show that one can construct a job IBF from the given task IBF. *)
Lemma task_IBF_implies_job_IBF :
job_interference_is_bounded_by
arr_seq sched tsk
(fun A R => (task_rbf (A + ε) - task_cost tsk) + task_IBF A R)
(relative_arrival_time_of_job_is_A sched).
Proof.
move => t1 t2 R j ARR TSK BUSY NEQ COMPL.
have [ZERO|POS] := posnP (@job_cost _ jc j).
{ exfalso; move: COMPL => /negP COMPL; apply: COMPL.
by rewrite /service.completed_by ZERO. }
move => A LE; specialize (LE _ _ BUSY).
apply leq_trans with (task_rbf (A + ε) - task_cost tsk + cumul_task_interference arr_seq sched j t1 (t1 + R)).
- rewrite -/cumulative_interference.
eapply leq_trans; first by eapply cumulative_job_interference_bound; eauto 2.
by rewrite LE; replace (t1 + A - t1) with A by lia.
- rewrite leq_add2l; eapply leq_trans; last exact:leqnn.
rewrite /cumul_task_interference.
apply (H_task_interference_is_bounded t1 t2 R) => //.
have EQ : job_arrival j - t1 = A by lia.
subst A.
rewrite /relative_arrival_time_of_job_is_A => t1' t2' BUSY'.
have [EQ1 E2] := busy_interval_is_unique _ _ _ _ _ _ BUSY BUSY'.
by subst.
Qed.
End TaskIBFtoJobIBF.
analysis/abstract/abstract_rta.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.lower_bound_on_service.
(** * Abstract Response-Time Analysis *)
(** In this module, we propose the general framework for response-time
analysis (RTA) of uni-processor scheduling of real-time tasks with
arbitrary arrival models. *)
(** We prove that the maximum (with respect to the set of offsets)
among the solutions of the response-time bound recurrence is a
response-time bound for the task under analysis. *)
Section Abstract_RTA.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context {jc : JobCost Job}.
(** Consider _any_ kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival and any schedule of this arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Variable sched : schedule PState.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Consider a task set [ts]... *)
Variable ts : list Task.
(** ... and a task [tsk] of [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the scheduler is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Let [L] be a constant that bounds the length of any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_bounded_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Note that response-time analyses are static analyses and by
definition have no access to dynamic information of an
individual execution of a system. However, oftentimes some
dynamic information can improve the tightness of a response-time
bound. For example, in case of a model with sequential tasks,
information about relative arrival time of a job can be used to
bound the maximum self-interference. *)
(** To gain access to some dynamic information for a response-time
recurrence, one can _assume_ that an execution of a system
satisfies a statically defined predicate. Then a response-time
bound can be calculated by considering a family of inputs to the
predicate that covers all the relevant dynamic scenarios.
To give a concrete example, one can (1) assume that any job [j]
of a task [tsk] arrives exactly [A] time units after the
beginning of [j]'s busy interval, (2) calculate the
response-time bound of [tsk] as if the assumption of step (1)
was satisfied, and (3) try all the possible [A]s. That results
in a "relative-arrival"-aware analysis. *)
(** The idea we will employ in this file is that one can use more
sophisticated dynamic information in a response-time recurrence.
In the following, we consider a case when information about (1)
relative arrival time of a job and (2) relative time when any
job of task [tsk] receives at least [task_rtc tsk] units of
service is used in the response-time recurrence. *)
(** Next, the response-time analysis will proceed in a sequence of
stages. A stage defines the set of sources of interference that
can postpone the execution of a job. Note that this separation
is mostly a design question. And for different models there might be
a varying number of stages with different meanings. *)
(** For our purposes, we consider two stages. *)
(** First stage: A job [j] can be (1) preempted because of the
presence of higher-or-equal priority workload and (2) make no
progress due to some other reason (spinning, lack of supply, and
so on). To bound all this interference we introduce an
interference bound function [IBF_P]. Note that [IBF_P] (1)
counts any job with higher-or-equal priority as interference and
(2) depends on the relative arrival time of a job. To bound time
that [j] spends in the first stage, we need to find a fixpoint
of equation [F : task_rtc tsk + IBF_P tsk A F ≤ F]. *)
(** To formalize the dependency of [IBF_P] on the relative arrival
time in Coq, we introduce a predicate that tests whether a job
[j] arrives exactly [A] time units after the beginning of its
busy interval, which is unique (if it exists). *)
Definition relative_arrival_time_of_job_is_A (j : Job) (A : duration) :=
forall (t1 t2 : instant),
busy_interval sched j t1 t2 ->
A = job_arrival j - t1.
(** Next, consider a valid interference bound function [IBF_P] that
can use information about relative time arrival of a job of task
[tsk]. Recall that an interference bound function gives a bound on
the cumulative interference incurred by jobs of task [tsk]. *)
Variable IBF_P : (* A *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded_IBFP :
job_interference_is_bounded_by
arr_seq sched tsk IBF_P relative_arrival_time_of_job_is_A.
(** Second stage: Job [j] reaches its run-to-completion
threshold. After this point the job cannot be preempted by a
high-or-equal priority job (so we can forget about any
task-generated workload). At this stage, the only reason why the
job cannot make progress is due to lack of supply or similar. To
bound time that [j] spends in the second stage we use
[IBF_NP]. Note that the amount of interference may depend on the
relative time when job [j] receives [task_rtc tsk] units of
service; hence, [IBF_NP] depends on this parameter. Also, notice
that [IBF_NP] still bounds interference starting from the
beginning of the busy window, even though it can use the
solution of the first fixpoint equation. *)
(** To formalize the dependency of [IBF_NP] on the relative time
when job [j] receives [task_rtc tsk] units of service in Coq, we
introduce a predicate that tests whether a job [j] has more than
[task_rtc tsk] units of service at a time instant [t1 + F],
where [t1] is the beginning of [j]'s busy interval. The first
conjunct of the proposition is needed to derive a fact that by
time [t1 + F] job [j] does not receive any interference from
higher-or-equal priority jobs. *)
Definition relative_time_to_reach_rtct (j : Job) (F : duration) :=
forall (t1 t2 : instant),
busy_interval sched j t1 t2 ->
task_rtct tsk + IBF_P (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F).
(** Next, consider a valid interference bound function [IBF_NP] that
can use information about the relative time when any given job of task
[tsk] receives at least [task_rtc tsk] units of service. *)
Variable IBF_NP : (* F *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded_IBFNP:
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP relative_time_to_reach_rtct.
(** In addition, we assume that [IBF_NP] indeed takes into account
information received in the first stage. Specifically, we assume
that the sum of [tsk]'s cost and [IBF_NP F Δ] is never smaller
than [F]. This intuitively means that the second stage cannot
have a solution that is smaller than the solution to the first
stage. *)
Hypothesis H_IBF_NP_ge_param : forall F Δ, F <= task_cost tsk + IBF_NP F Δ.
(** Given [IBF_P] and [IBF_NP] we construct a response-time recurrence. *)
(** For clarity, let's define a local name for the search space. *)
Let is_in_search_space A := is_in_search_space L IBF_P A.
(** We use the following equation to bound the response-time of a
job of task [tsk]. Consider any value [R] that upper-bounds the
solution of each response-time recurrence, i.e., for any
relative arrival time [A] in the search space, there exists a
corresponding solution [F] such that [task_rtc tsk + IBF_P tsk A
F ≤ F] and [task_cost tsk + IBF_NP tsk F (A + R) ≤ A + R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum :
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
task_rtct tsk + IBF_P A F <= F /\
task_cost tsk + IBF_NP F (A + R) <= A + R.
(** * Proof of the Theorem *)
(** In the next section we show a detailed proof of the main theorem
that establishes that [R] is indeed a response-time bound of
task [tsk]. *)
Section ProofOfTheorem.
(** Consider any job [j] of [tsk] with a positive cost. Note that
the assumption about positive job cost is needed to apply
hypothesis [H_bounded_busy_interval_exists]. Later, we
consider the case when [job_cost j = 0] as well. This way, we
ensure that this assumption does not propagate further. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Assume we have a busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j t1 t2.
(** Let's define [A] as a relative arrival time of job
[j] (with respect to time [t1]). *)
Let A := job_arrival j - t1.
(** First, note that [job_arrival j] is equal to [t1 + A]. *)
Fact job_arrival_eq_t1_plus_A : job_arrival j = t1 + A.
Proof. by move: H_busy_interval => [[/andP [GT LT] _] _]; rewrite /A subnKC. Qed.
(** Since the length of the busy interval is bounded by [L], the
relative arrival time [A] of job [j] is less than [L]. *)
Fact relative_arrival_is_bounded : A < L.
Proof.
move: (H_job_of_tsk) => /eqP TSK.
edestruct H_bounded_busy_interval_exists as [t1' [t2' [_ [BOUND BUSY]]]] => //.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t1' t2'; clear BUSY.
apply leq_trans with (t2 - t1); last by rewrite leq_subLR.
move: (H_busy_interval)=> [[/andP [T1 T3] [_ _]] _].
by apply ltn_sub2r; first apply leq_ltn_trans with (job_arrival j).
Qed.
(** In order to prove that [R] is a response-time bound of job
[j], we use hypothesis [H_R_is_maximum]. Note that the
relative arrival time [A] does not necessarily belong to the
search space. However, earlier (see file
[abstract.search_space]) we have proven that for any [A] there
exists another [A_sp] from the search space that shares the
same [IBF_P] value.
Moreover, since the function [IBF_P(A, ⋅)] is equivalent to
the function [IBF_P(A_sp, ⋅)], a solution [F] for [task_rtc
tsk + IBF_P tsk A_sp F ≤ F] also is a solution for [task_rtc
tsk + IBF_P tsk A F ≤ F]. Thus, despite the fact that the
relative arrival time may not lie in the search space, we can
still use the assumption [H_R_is_maximum]. *)
(** More formally, consider any [A_sp] such that: *)
Variable A_sp : duration.
(** (a) [A_sp] is less than or equal to [A]. *)
Hypothesis H_Asp_le_A : A_sp <= A.
(** (b) [IBF_P A x] is equal to [IBF_P A_sp x] for all [x] less than [L]. *)
Hypothesis H_equivalent :
are_equivalent_at_values_less_than (IBF_P A) (IBF_P A_sp) L.
(** (c) [A_sp] is in the search space. *)
Hypothesis H_Asp_is_in_search_space : is_in_search_space A_sp.
(** (d) [F] such that ... *)
Variable F : duration.
(** ... [F] is a solution of the response-time recurrence. *)
Hypothesis H_F_fixpoint : task_rtct tsk + IBF_P A_sp F <= F.
(** And finally, (e) [task_cost tsk + IBF_NP F (A_sp + R)] is
no greater than [A_sp + R]. *)
Hypothesis H_Asp_R_fixpoint :
task_cost tsk + IBF_NP F (A_sp + R) <= A_sp + R.
(** ** Case 1 *)
(** First, we consider the case where the solution [F] is so large
that the value of [t1 + F] goes beyond the busy
interval. Depending on the pessimism of [IBF_P] and [IBP_NP]
this might be either possible or impossible. Regardless, the
response-time bound can be easily proven, since any job that
completes by the end of the busy interval remains
completed. *)
Section FixpointOutsideBusyInterval1.
(** By assumption, suppose that [t2] is less than or equal to [t1 + F]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + F.
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
Lemma t2_le_arrival_plus_R_1 :
t2 <= job_arrival j + R.
Proof.
move: H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].
apply leq_trans with (t1 + F) => [//|].
rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l.
rewrite -(leqRW H_Asp_le_A) -(leqRW H_Asp_R_fixpoint).
by apply H_IBF_NP_ge_param.
Qed.
(** But since we know that the job is completed by the end of
its busy interval, we can show that job [j] is completed by
[job arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_1 :
completed_by sched j (job_arrival j + R).
Proof.
move: H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].
apply completion_monotonic with t2 => //.
exact: t2_le_arrival_plus_R_1.
Qed.
End FixpointOutsideBusyInterval1.
(** ** Case 2 *)
(** Next, we consider the case where the solution of the first
recurrence is small ([t1 + F < t2]), but the solution of the
second fixpoint goes beyond the busy interval. Although this
case may be (also) impossible, the response-time bound can be
easily proven, since any job that completes by the end of the
busy interval remains completed. *)
Section FixpointOutsideBusyInterval2.
(** Assume that [t1 + F] is less than [t2], ... *)
Hypothesis H_small_fixpoint_solution : t1 + F < t2.
(** ... but [t1 + (A_sp + R)] is at least [t2]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + (A_sp + R).
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
Lemma t2_le_arrival_plus_R_2 :
t2 <= job_arrival j + R.
Proof.
move: H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].
apply leq_trans with (t1 + (A_sp + R)) => [//|].
by rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l leq_add2r.
Qed.
(** But since we know that the job is completed by the end of
its busy interval, we can show that job [j] is completed by
[job arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_2 :
completed_by sched j (job_arrival j + R).
Proof.
move: H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].
apply completion_monotonic with t2.
- exact: t2_le_arrival_plus_R_2.
- exact: job_completes_within_busy_interval.
Qed.
End FixpointOutsideBusyInterval2.
(** ** Case 3 *)
(** Next, we consider the case when both solutions are smaller
than the length of the busy interval. *)
Section FixpointsInsideBusyInterval.
(** So, assume that [t1 + F] and [t1 + (A_sp + R)] are both
smaller than [t2]. *)
Hypothesis H_small_fixpoint_solution1 : t1 + F < t2.
Hypothesis H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2.
(** First note that [F] is indeed less than [L]. *)
Lemma relative_rtc_time_is_bounded : F < L.
Proof.
edestruct H_bounded_busy_interval_exists as [t1' [t2' [_ [BOUND BUSY]]]]; eauto 2.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t1' t2'; clear BUSY.
apply leq_trans with (t2 - t1); last by rewrite leq_subLR.
by rewrite ltn_subRL.
Qed.
(** Next we consider two sub-cases. *)
(** *** Case 3.1 *)
(** The cost of job [j] is smaller than or equal to the
run-to-completion threshold of task [tsk]. *)
Section JobCostIsSmall.
(** We assume that [job_cost j <= task_rtc tsk]. *)
Hypothesis H_job_cost_is_small : job_cost j <= task_rtct tsk.
(** Then we apply lemma [j_receives_enough_service] with
parameters [progress_of_job := job_cost j] and [delta :=
F] to obtain the fact that the service of [j] by time [t1
+ F] is no less than [job_cost j] (that is, the job is
completed). *)
Lemma job_receives_enough_service_1 :
job_cost j <= service sched j (t1 + F).
Proof.
move_neq_up T; move: (T) => NC; move_neq_down T.
eapply j_receives_enough_service; eauto 2;
rewrite /definitions.cumulative_interference.
rewrite -{2}(leqRW H_F_fixpoint).
rewrite leq_add //.
rewrite -H_equivalent; [ | apply relative_rtc_time_is_bounded].
eapply H_job_interference_is_bounded_IBFP with t2 => //.
+ by rewrite -ltnNge.
+ move => t1' t2' BUSY.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
by subst t1' t2'; rewrite job_arrival_eq_t1_plus_A; lia.
Qed.
End JobCostIsSmall.
(** *** Case 3.2 *)
(** The cost of job [j] is greater than or equal to
the run-to-completion threshold of task [tsk ]. *)
Section JobCostIsBig.
(** We assume that [task_rtc tsk <= job_cost j]. *)
Hypothesis H_job_cost_is_big : task_rtct tsk <= job_cost j.
(** We apply lemma [j_receives_enough_service] with parameters
[progress_of_job := task_rtc tsk] and [delta := F] to
obtain the fact that the service of [j] by time [t1 + F]
is no less than [task_rtc tsk]. *)
Lemma job_receives_enough_service_2 :
task_rtct tsk <= service sched j (t1 + F).
Proof.
move_neq_up T; move: (T) (H_job_of_tsk) => NC /eqP TSK; move_neq_down T.
eapply j_receives_enough_service => //.
rewrite /definitions.cumulative_interference.
erewrite leq_trans; last apply H_F_fixpoint; auto.
rewrite leq_add //.
rewrite -H_equivalent; [ | apply relative_rtc_time_is_bounded].
eapply H_job_interference_is_bounded_IBFP with t2 => //.
+ by rewrite -ltnNge (leqRW NC).
+ intros t0 t3 BUSY.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t0 t3; clear BUSY.
by rewrite job_arrival_eq_t1_plus_A; lia.
Qed.
(** Next, we again apply lemma [j_receives_enough_service]
with parameters [progress_of_job := job_cost j] and [delta
:= A_sp + R] to obtain the fact that the service of [j] by
time [t1 + (A_sp + R)] is no less than [job_cost j]. *)
Lemma job_receives_enough_service_3 :
job_cost j <= service sched j (t1 + (A_sp + R)).
Proof.
move: (H_job_of_tsk) => /eqP TSK.
apply/negPn/negP; intros NC; move: NC => /negP NC; apply NC; move: NC => /negP NC.
apply: j_receives_enough_service => //.
erewrite leq_trans; [ | | apply H_Asp_R_fixpoint]; auto.
apply leq_add; [by rewrite -TSK; apply H_valid_job_cost | ].
eapply H_job_interference_is_bounded_IBFNP with (t2 := t2); eauto 2.
intros t0 t3 BUSY.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t0 t3; clear BUSY; split.
- by rewrite H_equivalent //; apply relative_rtc_time_is_bounded.
- by rewrite -(leqRW job_receives_enough_service_2).
Qed.
End JobCostIsBig.
(** Either way, job [j] is completed by time [job_arrival j + R]. *)
Lemma job_is_completed_by_arrival_plus_R :
completed_by sched j (job_arrival j + R).
Proof.
edestruct (leqP (job_cost j) (task_rtct tsk)) as [LE|LE].
- eapply completion_monotonic; [ | eapply job_receives_enough_service_1; auto].
apply leq_trans with (t1 + (A_sp + R));
[ rewrite leq_add2l; eapply leq_trans; [ | apply H_Asp_R_fixpoint]; eauto
| by rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l leq_add2r].
- eapply completion_monotonic; [ | eapply job_receives_enough_service_3; auto].
by rewrite addnA leq_add2r job_arrival_eq_t1_plus_A leq_add2l.
Qed.
End FixpointsInsideBusyInterval.
End ProofOfTheorem.
(** * Response-Time Bound *)
(** Using the lemmas above, we prove that [R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound:
task_response_time_bound arr_seq sched tsk R.
Proof.
move => j ARR JOBtsk; unfold job_response_time_bound.
move: (posnP (@job_cost _ jc j)) => [ZERO|POS].
{ by rewrite /completed_by ZERO. }
move: (H_bounded_busy_interval_exists _ ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].
move: (relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY) => AltL.
move: (representative_exists _ IBF_P _ AltL) => [A__sp [ALEA2 [EQΦ INSP]]].
set (A := job_arrival j - t1) in *.
move: (H_R_is_maximum _ INSP) => [F [FIX1 FIX2]].
edestruct (leqP t2 (t1 + F)) as [LE1|LE1];
[ | edestruct (leqP t2 (t1 + (A__sp + R))) as [LE2|LE2]].
- by eapply job_completed_by_arrival_plus_R_1; eauto.
- by eapply job_completed_by_arrival_plus_R_2; eauto.
- by eapply job_is_completed_by_arrival_plus_R with (A_sp := A__sp); eauto 2.
Qed.
End Abstract_RTA.
analysis/abstract/busy_interval.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.abstract.definitions.
(** * Lemmas About Abstract Busy Intervals *)
(** In this file we prove a few basic lemmas about the notion of
an abstract busy interval. *)
Section LemmasAboutAbstractBusyInterval.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
(** Next, consider any work-conserving schedule of this arrival sequence
... *)
Variable sched : schedule PState.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... where jobs do not execute before their arrival. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** Consider an arbitrary job [j] with positive cost. Notice that a
positive-cost assumption is required to ensure that one cannot
construct a busy interval without any workload inside of it. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** We first prove that any interval <<[t1, t2)>> is either a busy
interval of job [j] or not. *)
Lemma busy_interval_prefix_case :
forall t1 t2,
busy_interval_prefix sched j t1 t2 \/ ~ busy_interval_prefix sched j t1 t2.
Proof.
move=> t1 t2.
have [JA|NAT] := boolP (t1 <= job_arrival j < t2); last first.
{ by right; move => PREF; move: NAT => /negP NQT; apply: NQT; apply PREF. }
have [QT1|NQT] := boolP (quiet_time sched j t1); last first.
{ by right; move => PREF; move: NQT => /negP NQT; apply: NQT; apply PREF. }
have [AQT|NQT] := boolP (all (fun t => ~~ quiet_time sched j t) (index_iota t1.+1 t2)); last first.
{ right; move=> PREF; move: NQT => /negP NQT; apply: NQT.
apply/allP => t IO; apply/negP.
by apply PREF; move: IO; rewrite mem_index_iota.
}
left; split; [by done | split] => //.
move => t NEQ; apply/negP; move: AQT => /allP AQT; apply: AQT.
by rewrite mem_index_iota.
Qed.
(** Consider two intervals <<[t1, t2)>> ⊆ <<[t1, t2')>>, where
<<[t1, t2)>> is a busy-interval prefix and <<[t1, t2')>> is not
a busy-interval prefix. Then there exists [t2''] such that
<<[t1, t2'')>> is a busy interval. *)
Lemma terminating_busy_prefix_is_busy_interval :
forall t1 t2 t2',
t2 <= t2' ->
busy_interval_prefix sched j t1 t2 ->
~ busy_interval_prefix sched j t1 t2' ->
exists t2'', busy_interval sched j t1 t2''.
Proof.
move=> t1 t2 t2' LE BUSY NBUSY.
interval_to_duration t2 t2' δ.
induction δ as [ | δ IHδ].
{ by exfalso; apply: NBUSY; rewrite addn0. }
have [BUSY'|NBUSY'] := busy_interval_prefix_case t1 (t2 + δ); last by apply IHδ in NBUSY'.
clear IHδ.
exists (t2 + δ); split => //.
apply negbNE; apply/negP => FF.
apply:NBUSY; split; first by move: BUSY => []; lia.
split; first by move: BUSY => []; lia.
move => t; rewrite addnS ltnS [_ <= t2 + δ]leq_eqVlt.
move => /andP [LT1 /orP [/eqP WDFW | VB]].
- by subst; apply/negP.
- by apply BUSY'; lia.
Qed.
(** Next, consider a busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j t1 t2.
(** First, we prove that job [j] completes by the end of the busy
interval. Note that the busy interval contains the execution of
job [j]; in addition, time instant [t2] is a quiet time. Thus by
the definition of a quiet time the job must be completed
before time [t2]. *)
Lemma job_completes_within_busy_interval :
completed_by sched j t2.
Proof.
move: (H_busy_interval) => [[/andP [_ LT] _] /andP [_ QT2]].
unfold quiet_time, pending_earlier_and_at, pending, has_arrived in QT2.
move: QT2; rewrite negb_and => /orP [QT2|QT2].
{ by move: QT2 => /negP QT2; exfalso; apply QT2, ltnW. }
by rewrite Bool.negb_involutive in QT2.
Qed.
(** We show that, similarly to the classical notion of busy
interval, the job does not receive service before the busy
interval starts. *)
Lemma no_service_before_busy_interval :
forall t, service sched j t = service_during sched j t1 t.
Proof.
move => t; move : (H_busy_interval) => [[/andP [LE1 LE2] [QT1 AQT]] QT2].
destruct (leqP t1 t) as [NEQ1|NEQ1]; first destruct (leqP t2 t) as [NEQ2|NEQ2].
- apply/eqP; rewrite eqn_leq; apply/andP; split.
+ rewrite /service -(service_during_cat _ _ _ t1);
[ | by apply/andP; split; lia].
by rewrite cumulative_service_before_job_arrival_zero; eauto 2.
+ rewrite /service -[in X in _ <= X](service_during_cat _ _ _ t1);
[ | by apply/andP; split; lia].
by (erewrite cumulative_service_before_job_arrival_zero with (t1 := 0)
|| erewrite cumulative_service_before_job_arrival_zero with (t3 := 0)).
- rewrite /service -(service_during_cat _ _ _ t1);
[ | by apply/andP; split; lia].
by rewrite cumulative_service_before_job_arrival_zero; eauto 2.
- rewrite service_during_geq; last by lia.
by rewrite /service cumulative_service_before_job_arrival_zero//; lia.
Qed.
(** Since the job cannot arrive before the busy interval starts and
completes by the end of the busy interval, it receives at least
[job_cost j] units of service within the interval. *)
Lemma service_within_busy_interval_ge_job_cost :
job_cost j <= service_during sched j t1 t2.
Proof.
move : (H_busy_interval) => [[/andP [LE1 LE2] [QT1 AQT]] QT2].
rewrite -[service_during _ _ _ _]add0n.
rewrite -(cumulative_service_before_job_arrival_zero sched j _ 0 _ LE1)//.
rewrite service_during_cat; last by apply/andP; split; lia.
rewrite -/(completed_by sched j t2).
exact: job_completes_within_busy_interval.
Qed.
(** Trivially, job [j] arrives before the end of the busy window (if arrival
times are consistent), which is a useful fact to observe for proof
automation. *)
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
Fact abstract_busy_interval_arrivals_before :
j \in arrivals_before arr_seq t2.
Proof.
move: (H_busy_interval) => [[/andP [_ LT] _] _].
by apply: arrived_between_implies_in_arrivals.
Qed.
(** For the same reason, we note the trivial fact that by definition [j]
arrives no earlier than at time [t1]. For automation, we note this both as
a fact on busy-interval prefixes ... *)
Fact abstract_busy_interval_prefix_job_arrival :
forall t t', busy_interval_prefix sched j t t' -> t <= job_arrival j.
Proof.
by move=> ? ? [/andP [GEQ _] _].
Qed.
(** ... and complete busy-intervals. *)
Fact abstract_busy_interval_job_arrival :
t1 <= job_arrival j.
Proof.
move: H_busy_interval => [PREFIX _].
exact: abstract_busy_interval_prefix_job_arrival.
Qed.
(** Next, let us assume that the introduced processor model is
unit-supply. *)
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Under this assumption, the sum of the total service during the
time interval <<[t1, t1 + Δ)>> and the cumulative interference
during the same interval is bounded by the length of the time
interval. *)
Lemma service_and_interference_bound :
forall Δ,
t1 + Δ <= t2 ->
service_during sched j t1 (t1 + Δ) + cumulative_interference j t1 (t1 + Δ) <= Δ.
Proof.
move=> Δ LE; rewrite -big_split //= -{2}(sum_of_ones t1 Δ).
rewrite big_nat [in X in _ <= X]big_nat; apply leq_sum => t /andP[Lo Hi].
move: (H_work_conserving j t1 t2 t) => Workj.
feed_n 4 Workj => //.
{ by move: H_busy_interval => [PREF QT]. }
{ by apply/andP; split; lia. }
rewrite /cond_interference //=; move: Workj; case: interference => Workj.
- by rewrite addn1 ltnS; move_neq_up NE; apply Workj.
- by rewrite addn0; apply: H_unit_service_proc_model.
Qed.
End LemmasAboutAbstractBusyInterval.
(** In the following section, we derive a sufficient condition for the
existence of abstract busy intervals for unit-service
processors. *)
Section AbstractBusyIntervalExists.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of of unit-service processor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Assume we are provided with abstract functions for interference
and interfering workload ... *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** ... that do not allow speculative execution. *)
Hypothesis H_no_speculative_exec : no_speculative_execution.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.
(** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
(** Next, consider any work-conserving (in the abstract sense)
schedule of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Consider an arbitrary job [j] from task [tsk] with positive cost. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_task : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** In this section, we prove a fact that allows one to extend an
inequality between cumulative interference and interfering
workload from a busy-interval prefix <<[t1, t)>> to the whole
timeline <<[0, t)>>. *)
Section CumulativeIntIntWorkExtension.
(** Consider any busy-interval prefix of job [j]. *)
Variable t1 t_busy : instant.
Hypothesis H_is_busy_prefix : busy_interval_prefix sched j t1 t_busy.+1.
(** We assume that, for some positive [δ], the cumulative
interfering workload within interval <<[t1, t1 + δ)>> is
bounded by cumulative interference in the same interval. *)
Variable δ : duration.
Hypothesis H_iw_bounded :
cumulative_interfering_workload j t1 (t1 + δ) <= cumulative_interference j t1 (t1 + δ).
(** Then the cumulative interfering workload within interval <<[0,
t1 + δ)>> is bounded by the cumulative interference in the
same interval. *)
Local Lemma cumul_iw_bounded_by_cumul_i :
cumulative_interfering_workload j 0 (t1 + δ) <= cumulative_interference j 0 (t1 + δ).
Proof.
move: (H_iw_bounded) => LE.
rewrite /definitions.cumulative_interference
/definitions.cumulative_interfering_workload
/cumul_cond_interference.
rewrite (@big_cat_nat _ _ _ t1) //=; last by lia.
rewrite [in X in _ <= X](@big_cat_nat _ _ _ t1) //=; last by lia.
move: H_is_busy_prefix => [_ [/andP [/eqP DD KK ] ADD]].
rewrite /cumulative_interfering_workload in LE; rewrite (leqRW LE); clear LE.
rewrite leq_add2r.
rewrite /cumulative_interfering_workload in DD.
by rewrite -DD; clear DD.
Qed.
End CumulativeIntIntWorkExtension.
(** In the following section, we show that the busy interval is
bounded. More specifically, we show that the length of any
abstract busy interval is bounded, as long as there is enough
supply to accommodate the interfering workload. *)
Section BoundingBusyInterval.
(** For simplicity, let us define some local names. *)
Let quiet_time t := quiet_time sched j t.
Let busy_interval_prefix := busy_interval_prefix sched j.
Let busy_interval := busy_interval sched j.
(** Suppose that job [j] is pending at time [t_busy]. *)
Variable t_busy : instant.
Hypothesis H_j_is_pending : pending sched j t_busy.
(** First, we show that there must exist a busy interval prefix. *)
Section LowerBound.
(** Since job [j] is pending at time [t_busy], there is a
(potentially unbounded) busy interval that starts no later
than with the arrival of [j]. *)
Lemma exists_busy_interval_prefix :
exists t1,
busy_interval_prefix t1 t_busy.+1 /\
t1 <= job_arrival j <= t_busy.
Proof.
rename H_j_is_pending into PEND.
destruct ([exists t:'I_t_busy.+1, quiet_time t]) eqn:EX.
{ set (last0 := \max_(t < t_busy.+1 | quiet_time t) t).
move: EX => /existsP [t EX].
have PRED: quiet_time last0 by apply (bigmax_pred t_busy.+1 (quiet_time) t).
move: PRED => QUIET.
exists last0.
have JARRIN: last0 <= job_arrival j <= t_busy.
{ move: PEND => /andP [ARR NCOM].
apply/andP; split => //. move: QUIET => /andP [_ PE].
move: PE; rewrite negb_and -leqNgt => /orP [ | /negPn COMPL] => //; exfalso.
apply completion_monotonic with (t' := t_busy) in COMPL.
- by move: NCOM => /negP.
- by rewrite -ltnS; eapply bigmax_ltn_ord.
}
repeat split; auto 2; try apply QUIET => //=.
move => t0 /andP [GTlast LTbusy] QUIET0.
move_neq_down GTlast.
by eapply (@leq_bigmax_cond
_ (fun (x: 'I_t_busy.+1) => quiet_time x)
(fun x => x) (Ordinal LTbusy)).
}
{ apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
exists 0; split; last by apply/andP; split; last by move: PEND => /andP [ARR _].
repeat split.
- apply/andP; split => //; rewrite ltnS.
by move: PEND => /andP PEND; apply PEND.
- apply/andP; split;
first by rewrite /cumulative_interference /cumul_cond_interference /cumulative_interfering_workload !big_geq.
by apply not_pending_earlier_and_at_0.
- move => t /andP [GE LT] QUIET.
move: (ALL (Ordinal LT)) => /negP ALL'.
by apply ALL'.
}
Qed.
End LowerBound.
(** Next we prove that, if there is a point where the requested
workload is upper-bounded by the supply, then the busy
interval eventually ends. *)
Section UpperBound.
(** Consider any busy interval prefix of job [j]. *)
Variable t1 : instant.
Hypothesis H_is_busy_prefix : busy_interval_prefix t1 t_busy.+1.
(** We assume that for some positive [δ], the cumulative
interfering workload within interval <<[t1, t1 + δ)>> is
bounded by [δ]. *)
Variable δ : duration.
Hypothesis H_δ_positive : δ > 0.
Hypothesis H_workload_is_bounded :
workload_of_job arr_seq j t1 (t1 + δ)
+ cumulative_interfering_workload j t1 (t1 + δ) <= δ.
(** If there is a quiet time by time [t1 + δ], it trivially
follows that the busy interval is bounded. Thus, let's
consider first the harder case where there is no quiet time,
which turns out to be impossible. *)
Section CannotBeBusyForSoLong.
(** Assume that there is no quiet time in the interval <<(t1, t1 + δ]>>. *)
Hypothesis H_no_quiet_time : forall t, t1 < t <= t1 + δ -> ~ quiet_time t.
(** We prove that the sum of cumulative service and cumulative
interference in the interval <<[t, t + δ)>> is equal to
[δ]. *)
(** Since the interval is always non-quiet, the processor is
always busy processing job [j] and the job's interference
and, hence, the sum of service of [j] and its cumulative
interference within the interval <<[t1, t1 + δ)>> is
greater than or equal to [δ]. *)
Lemma busy_interval_has_uninterrupted_service :
δ <= service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).
Proof.
clear H_δ_positive H_workload_is_bounded H_j_is_pending.
rewrite /service_during /cumulative_interference /cumul_cond_interference /cond_interference /service_at.
rewrite -big_split //= -{1}(sum_of_ones t1 δ).
rewrite big_nat [in X in _ <= X]big_nat.
apply leq_sum => x /andP[Lo Hi].
destruct (leqP (t1 + δ) (t_busy.+1)) as [LE|LT].
{ move: (H_work_conserving j t1 t_busy.+1 x) => Workj.
feed_n 4 Workj; try done.
{ by apply/andP; split; eapply leq_trans; eauto. }
destruct interference.
- by lia.
- by rewrite //= addn0; apply Workj.
}
{ move: (H_work_conserving j t1 (t1 + δ) x) => Workj.
feed_n 4 Workj; try done.
- move: H_is_busy_prefix => [/andP [A1 A2] [QT NQT]]; split; [ | split].
+ by apply/andP; split => //; rewrite (leqRW A2) -(leqRW LT).
+ by apply QT.
+ move => t /andP [A3 A4]; apply H_no_quiet_time.
by apply/andP; split; lia.
- by apply/andP; split; eapply leq_trans; eauto 2.
- destruct interference.
+ by lia.
+ by rewrite //= addn0; apply Workj.
}
Qed.
(** However, since the total workload is bounded (see
[H_workload_is_bounded]), the sum of [j]'s cost and its
interfering workload within the interval <<[t1, t1 + δ)>>
is bounded by [j]'s service and its interference within
the same time interval. *)
Lemma busy_interval_too_much_workload :
job_cost j + cumulative_interfering_workload j t1 (t1 + δ) <=
service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).
Proof.
replace (job_cost j) with (workload_of_job arr_seq j t1 (t1 + δ));
first by rewrite (leqRW H_workload_is_bounded)
-(leqRW busy_interval_has_uninterrupted_service).
move: (H_is_busy_prefix) => [/andP [NEQ1 _] _].
erewrite workload_of_job_eq_job_arrival => //=.
rewrite NEQ1 Bool.andb_true_l.
have -> : job_arrival j < t1 + δ; last by done.
move_neq_up GE.
apply (H_no_quiet_time (t1 + δ)).
{ by apply/andP; split; [rewrite -addn1 leq_add2l | done]. }
apply/andP; split.
- move: (H_workload_is_bounded); rewrite workload_of_job_eq_job_arrival //=.
rewrite NEQ1 Bool.andb_true_l [_ < _ + _]leqNgt ltnS GE //= add0n => LE.
rewrite eqn_leq; apply/andP; split.
+ by apply H_no_speculative_exec.
+ apply (cumul_iw_bounded_by_cumul_i _ t_busy) => //=; rewrite (leqRW LE).
eapply leq_trans; first apply busy_interval_has_uninterrupted_service.
by have -> : service_during sched j t1 (t1 + δ) = 0
by rewrite cumulative_service_before_job_arrival_zero.
- by rewrite /pending_earlier_and_at negb_and;
apply/orP; left; rewrite -ltnNge ltnS.
Qed.
(** The latter two lemmas imply that [t1 + δ] is a quiet time ... *)
Lemma t1δ_is_quiet : quiet_time (t1 + δ).
Proof.
have LW := busy_interval_too_much_workload.
have NEQ: forall a b c d, a >= c -> b >= d -> a + b <= c + d -> a = c /\ b = d by lia.
apply NEQ in LW; first destruct LW as [EQ1 EQ2].
- apply/andP; split.
+ rewrite eqn_leq; apply/andP; split.
* by apply H_no_speculative_exec.
* by apply (cumul_iw_bounded_by_cumul_i _ t_busy) => //=; rewrite EQ2.
+ rewrite negb_and Bool.negb_involutive; apply/orP; right.
rewrite /completed_by EQ1.
by erewrite <-(service_cat); [apply leq_addl | ]; lia.
- eapply leq_trans; last by apply service_at_most_cost => //=.
by erewrite <-(service_cat); [apply leq_addl | ]; lia.
- move: H_is_busy_prefix => [_ [/andP [/eqP D _] _]].
rewrite -(leq_add2l (definitions.cumulative_interference j 0 t1)) {2}D.
rewrite -(big_cat_nat) //=; last by lia.
by rewrite -(big_cat_nat) //=; last by lia.
Qed.
(** ... which is a contradiction with the initial
assumption. *)
Lemma t1δ_is_quiet_contra : False.
Proof.
eapply H_no_quiet_time; last by apply t1δ_is_quiet.
apply/andP; split; last by done.
by rewrite -addn1 leq_add2l.
Qed.
End CannotBeBusyForSoLong.
(** Since the interval cannot remain busy for so long, we prove
that the busy interval finishes at some point [t2 <= t1 +
δ]. *)
Lemma busy_interval_is_bounded :
exists t2,
t_busy < t2
/\ t2 <= t1 + δ
/\ busy_interval t1 t2.
Proof.
move: H_is_busy_prefix => [NEQ [QT NQT]].
destruct ([exists t2:'I_(t1 + δ).+1, (t2 > t1) && quiet_time t2]) eqn:EX.
{ have EX': exists (t2 : instant), ((t1 < t2 <= t1 + δ) && quiet_time t2).
{ move: EX => /existsP [t2 /andP [LE QUIET]].
exists t2; apply/andP; split => //;
by apply/andP; split; last (rewrite -ltnS; apply ltn_ord). }
move: (ex_minnP EX') => [t2 /andP [/andP [GT LE] QUIET] MIN]; clear EX EX'.
exists t2; split; [ | split; [ |split; [split; [ | split] | ] ]]; try done.
{ move_neq_up NEQ2.
move: (H_is_busy_prefix) => [_ [_ NQ]]; apply:(NQ t2) => //.
by apply/andP; split => //.
}
{ move: NEQ => /andP [IN1 IN2].
apply/andP; split => //.
apply leq_ltn_trans with t_busy; eauto 2.
rewrite ltnNge; apply/negP; intros CONTR.
apply NQT with t2 => //.
by apply/andP; split; last rewrite ltnS.
}
{ move => t /andP [GT1 LT2] BUG.
feed (MIN t); first (apply/andP; split) => //.
{ by apply/andP; split; last apply leq_trans with (n := t2); eauto using ltnW. }
{ by lia. }
}
}
{ apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL'.
have ALL: forall t, t1 < t <= t1 + δ -> ~ quiet_time t.
{ move => t /andP [GTt LEt] QUIET; rewrite -ltnS in LEt.
specialize (ALL' (Ordinal LEt)); rewrite negb_and /= GTt orFb in ALL'.
by move: ALL' => /negP ALL'; apply ALL'; clear ALL'.
}
by clear ALL'; exfalso; eapply t1δ_is_quiet_contra.
}
Qed.
End UpperBound.
End BoundingBusyInterval.
End AbstractBusyIntervalExists.
(** We add some facts into the "Hint Database" basic_rt_facts, so Coq will be
able to apply them automatically where needed. *)
Global Hint Resolve
abstract_busy_interval_arrivals_before
job_completes_within_busy_interval
abstract_busy_interval_prefix_job_arrival
abstract_busy_interval_job_arrival
: basic_rt_facts.
analysis/abstract/definitions.v 0 → 100644
View file @ a162d510
Require Export prosa.model.task.concept.
(** * Definitions for Abstract Response-Time Analysis *)
(** In the following, we propose a set of definitions for the general
framework for response-time analysis (RTA) of uni-processor
scheduling of real-time tasks with arbitrary arrival models. *)
(** We are going to introduce two main variables of the analysis:
(a) interference, and (b) interfering workload. *)
(** ** a) Interference *)
(** Execution of a job may be postponed by the environment and/or the
system due to different factors (preemption by higher-priority
jobs, jitter, black-out periods in hierarchical scheduling, lack
of budget, etc.), which we call interference.
Besides, note that even the subsequent activation of a task can
suffer from interference at the beginning of its busy interval
(despite the fact that this job hasn’t even arrived at that
moment!). Thus, it makes more sense (at least for the current
busy-interval analysis) to think about interference of a job as
any interference within the corresponding busy interval, and not
just after the release of the job.
Based on that rationale, assume a predicate that expresses whether a job [j]
under consideration incurs interference at a given time [t] (in
the context of the schedule under consideration). This will be
used later to upper-bound job [j]'s response time. Note that a
concrete realization of the function may depend on the schedule,
but here we do not require this for the sake of simplicity and
generality. *)
Class Interference (Job : JobType) :=
interference : Job -> instant -> bool.
(** ** b) Interfering Workload *)
(** In addition to interference, the analysis assumes that at any time
[t], we know an upper bound on the potential cumulative
interference that can be incurred in the future by any job (i.e.,
the total remaining potential delays). Based on that, assume a
function [interfering_workload] that indicates for any job [j], at
any time [t], the amount of potential interference for job [j]
that is introduced into the system at time [t]. This function will
be later used to upper-bound the length of the busy window of a
job. One example of workload function is the "total cost of jobs
that arrive at time [t] and have higher-or-equal priority than job
[j]". In some task models, this function expresses the amount of the
potential interference on job [j] that "arrives" in the system at
time [t]. *)
Class InterferingWorkload (Job : JobType) :=
interfering_workload : Job -> instant -> duration.
(** Next we introduce all the abstract notions required by the analysis. *)
Section AbstractRTADefinitions.
(** Consider any type of job associated with any type of tasks... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(** ... with arrival times and costs. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Let [tsk] be any task that is to be analyzed *)
Variable tsk : Task.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** In order to perform subsequent abstract Response Time Analyses
(RTAs), it is essential that we have the capability to bound
interference of a certain type (for example, interference that
comes from other tasks' jobs). To achieve this, we define
"conditional" interference as a conjunction of a predicate [P :
Job -> instant -> bool] encoding the property of interest and
[interference]. *)
Definition cond_interference P j t :=
(P j t) && (interference j t).
(** In order to bound the response time of a job, we must consider
(1) the cumulative conditional interference, ... *)
Definition cumul_cond_interference P j t1 t2 :=
\sum_(t1 <= t < t2) cond_interference P j t.
(** ... (2) cumulative interference, ... *)
Definition cumulative_interference j t1 t2 :=
cumul_cond_interference (fun _ _ => true) j t1 t2.
(** ... and (3) cumulative interfering workload. *)
Definition cumulative_interfering_workload j t1 t2 :=
\sum_(t1 <= t < t2) interfering_workload j t.
(** Next, we introduce a notion of absence of speculative
execution. This notion is _not_ directly related to Abstract
RTA, but it is useful when proving the existence of bounded busy
intervals.
We say that the functions [Interference] and
[InterferingWorkload] do not allow speculative execution if the
cumulative interference never exceeds the cumulative interfering
workload. Intuitively, one can interpret this definition as
stating that it is not allowed to perform work before it is
known whether it is actually needed (i.e., before the work
appears as actual workload). *)
Definition no_speculative_execution :=
forall j t,
cumulative_interference j 0 t <= cumulative_interfering_workload j 0 t.
(** Definition of Busy Interval *)
(** Further analysis will be based on the notion of a busy
interval. The overall idea of the busy interval is to take into
account the workload that cause a job under consideration to
incur interference. In this section, we provide a definition of
an abstract busy interval. *)
Section BusyInterval.
(** We say that time instant [t] is a quiet time for job [j] iff
two conditions hold. First, the cumulative interference at
time [t] must be equal to the cumulative interfering
workload. Intuitively, this condition indicates that the
potential interference seen so far has been fully "consumed"
(i.e., there is no more higher-priority work or other kinds of
delay pending). Second, job [j] cannot be pending at any time
earlier than [t] _and_ at time instant [t] (i.e., either it
was pending earlier but is no longer pending now, or it was
previously not pending and may or may not be released
now). The second condition ensures that the busy window
captures the execution of job [j]. *)
Definition quiet_time (j : Job) (t : instant) :=
(cumulative_interference j 0 t == cumulative_interfering_workload j 0 t)
&& ~~ pending_earlier_and_at sched j t.
(** Based on the definition of quiet time, we say that an interval
<<[t1, t2)>> is a (potentially unbounded) busy-interval prefix
w.r.t. job [j] iff the interval (a) contains the arrival of
job j, (b) starts with a quiet time and (c) remains
non-quiet. *)
Definition busy_interval_prefix (j : Job) (t1 t2 : instant) :=
t1 <= job_arrival j < t2 /\
quiet_time j t1 /\
(forall t, t1 < t < t2 -> ~ quiet_time j t).
(** Next, we say that an interval <<[t1, t2)>> is a busy interval
iff <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet
time. *)
Definition busy_interval (j : Job) (t1 t2 : instant) :=
busy_interval_prefix j t1 t2 /\
quiet_time j t2.
(** Note that the busy interval, if it exists, is unique. *)
Fact busy_interval_is_unique :
forall j t1 t2 t1' t2',
busy_interval j t1 t2 ->
busy_interval j t1' t2' ->
t1 = t1' /\ t2 = t2'.
Proof.
move=> j t1 t2 t1' t2' BUSY BUSY'.
have EQ: t1 = t1'.
{ apply/eqP.
apply/negPn/negP; intros CONTR.
move: BUSY => [[IN [QT1 NQ]] _].
move: BUSY' => [[IN' [QT1' NQ']] _].
move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
{ apply NQ with t1' => //; clear NQ.
apply/andP; split=> [//|].
move: IN IN' => /andP [_ T1] /andP [T2 _].
by apply leq_ltn_trans with (job_arrival j).
}
{ apply NQ' with t1 => [|//]; clear NQ'.
apply/andP; split=> [//|].
move: IN IN' => /andP [T1 _] /andP [_ T2].
by apply leq_ltn_trans with (job_arrival j).
}
}
subst t1'.
have EQ: t2 = t2'.
{ apply/eqP.
apply/negPn/negP; intros CONTR.
move: BUSY => [[IN [_ NQ]] QT2].
move: BUSY' => [[IN' [_ NQ']] QT2'].
move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
{ apply NQ' with t2 => //; clear NQ'.
apply/andP; split=> [|//].
move: IN IN' => /andP [_ T1] /andP [T2 _].
by apply leq_ltn_trans with (job_arrival j).
}
{ apply NQ with t2' => //; clear NQ.
apply/andP; split=> [|//].
move: IN IN' => /andP [T1 _] /andP [_ T2].
by apply leq_ltn_trans with (job_arrival j).
}
}
by subst t2'.
Qed.
End BusyInterval.
(** In this section, we introduce some assumptions about the busy
interval that are fundamental to the analysis. *)
Section BusyIntervalProperties.
(** We say that a schedule is "work-conserving" (in the abstract
sense) iff, for any job [j] from task [tsk] and at any time [t]
within a busy interval, there are only two options: either (a)
[interference(j, t)] holds or (b) job [j] is scheduled at time
[t]. *)
Definition work_conserving :=
forall j t1 t2 t,
arrives_in arr_seq j ->
job_cost j > 0 ->
busy_interval_prefix j t1 t2 ->
t1 <= t < t2 ->
~ interference j t <-> receives_service_at sched j t.
(** Next, we say that busy intervals of task [tsk] are bounded by
[L] iff, for any job [j] of task [tsk], there exists a busy
interval with length at most [L]. Note that the existence of
such a bounded busy interval is not guaranteed if the schedule
is overloaded with work. Therefore, in the later concrete
analyses, we will have to introduce an additional condition
that prevents overload. *)
Definition busy_intervals_are_bounded_by L :=
forall j,
arrives_in arr_seq j ->
job_of_task tsk j ->
job_cost j > 0 ->
exists t1 t2,
t1 <= job_arrival j < t2 /\
t2 <= t1 + L /\
busy_interval j t1 t2.
(** Although we have defined the notion of cumulative
(conditional) interference of a job, it cannot be used in a
(static) response-time analysis because of the dynamic
variability of job parameters. To address this issue, we
define the notion of an interference bound. *)
(** As a first step, we introduce a notion of an "interference
bound function" [IBF]. An interference bound function is any
function with a type [duration -> duration -> work] that bounds
cumulative conditional interference of a job of task [tsk] (a
precise definition will be presented below).
Note that the function has two parameters. The second
parameter is the length of an interval in which the
interference is supposed to be bounded. It is quite intuitive;
so, we will not explain it in more detail. However, the first
parameter deserves more thoughtful explanation, which we
provide next. *)
Variable IBF : duration -> duration -> work.
(** The first parameter of [IBF] allows one to organize a case
analysis over a set of values that are known only during the
computation. For example, the most common parameter is the
relative arrival time [A] of a job (of a task under
analysis). Strictly speaking, [A] is not known when computing
a fixpoint; however, one can consider a set of [A] that covers
all the relevant cases. There can be other valid properties
such as "a time instant when a job under analysis has received
enough service to become non-preemptive."
To make the first parameter customizable, we introduce a
predicate [ParamSem : Job -> instant -> Prop] that is used to
assign meaning to the second parameter. More precisely,
consider an expression [IBF(X, delta)], and assume that we
instantiated [ParamSem] as some predicate [P]. Then, it is
assumed that [IBF(X, delta)] bounds (conditional) interference
of a job under analysis [j ∈ tsk] if [P j X] holds. *)
Variable ParamSem : Job -> nat -> Prop.
(** As mentioned, [IBF] must upper-bound the cumulative
_conditional_ interference. This is done to make further
extensions of the base aRTA easier. The most general aRTA
assumes that an IBF bounds _all_ interference of a given job
[j]. However, as we refine the model under analysis, we split
the IBF into more and more parts. For example, assuming that
tasks are sequential, it is possible to split IBF into two
parts: (1) the part that upper-bounds the cumulative
interference due to self-interference and (2) the part that
upper-bounds the cumulative interference due to all other
reasons. To avoid duplication, we parameterize the definition
of an IBF by a predicate that encodes the type of interference
that must be upper-bounded. *)
Variable Cond : Job -> instant -> bool.
(** Next, let us define this reasoning formally. We say that the
conditional interference is bounded by an "interference bound
function" [IBF] iff for any job [j] of task [tsk] and its busy
interval <<[t1, t2)>> the cumulative conditional interference
incurred by [j] w.r.t. predicate [Cond] in the sub-interval
<<[t1, t1 + Δ)>> does not exceed [IBF(X, Δ)], where [X] is a
constant that satisfies a predefined predicate [ParamSem].
In other words, for a job [j ∈ tsk], the term [IBF(X, Δ)]
provides an upper-bound on the cumulative conditional
interference (w.r.t. the predicate [Cond]) that [j] might
experience in an interval of length [Δ] _assuming_ that
[ParamSem j X] holds. *)
Definition cond_interference_is_bounded_by :=
(** Consider a job [j] of task [tsk], a busy interval <<[t1,
t2)>> of [j], and an arbitrary interval <<[t1, t1 + Δ) ⊆
[t1, t2)>>. *)
forall t1 t2 Δ j,
arrives_in arr_seq j ->
job_of_task tsk j ->
busy_interval j t1 t2 ->
(** We require the IBF to bound the interference only within
the interval [t1, t1 + Δ). *)
t1 + Δ < t2 ->
(** Next, we require the [IBF] to bound the interference only
until the job is completed, after which the function can
behave arbitrarily. *)
~~ completed_by sched j (t1 + Δ) ->
(** And finally, the IBF function might depend not only on the
length of the interval, but also on a constant [X]
satisfying predicate [Param]. *)
forall X,
ParamSem j X ->
cumul_cond_interference Cond j t1 (t1 + Δ) <= IBF X Δ.
End BusyIntervalProperties.
(** As an important special case, we say that a job's interference
is (unconditionally) bounded by [IBF] if it is conditionally
bounded with [Cond := fun j t => true]. *)
Definition job_interference_is_bounded_by IBF Param :=
cond_interference_is_bounded_by IBF Param (fun _ _ => true).
End AbstractRTADefinitions.
analysis/abstract/ideal/abstract_rta.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.facts.model.ideal.schedule.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.
(** * Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model *)
(** In this module, we present an instantiation of the general
response-time analysis framework for models that satisfy the ideal
uni-service progress assumptions. *)
(** We prove that the maximum (with respect to the set of offsets)
among the solutions of the response-time bound recurrence is a
response-time bound for [tsk]. Note that in this section we add
additional restrictions on the processor state. These assumptions
allow us to eliminate the second equation from [aRTA+]'s
recurrence since jobs experience no delays while executing
non-preemptively. *)
Section AbstractRTAIdeal.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
(** Consider any kind of uni-service ideal processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Next, consider any schedule of this arrival sequence... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Consider a task set [ts]... *)
Variable ts : list Task.
(** ... and a task [tsk] of [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Consider a valid preemption model... *)
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
(** ...and a valid task run-to-completion threshold function. That
is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
for any job [j] of task [tsk] [job_rtct j] is bounded by
[task_rtct tsk]. *)
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
(** Assume we are provided with abstract functions for Interference
and Interfering Workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the scheduler is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Next, assume that [interference_bound_function] is a bound on
the interference incurred by jobs of task [tsk] parametrized by
the relative arrival time [A]. *)
Variable interference_bound_function : (* A *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded :
job_interference_is_bounded_by
arr_seq sched tsk interference_bound_function (relative_arrival_time_of_job_is_A sched).
(** To apply the generalized aRTA, we have to instantiate [IBF_P]
and [IBF_NP]. In this file, we assume we are given a generic function
[interference_bound_function] that bounds interference of jobs
of tasks in [ts] and which have to be instantiated in subsequent
files. We use this function to instantiate [IBF_P]. *)
(** However, we still have to instantiate function [IBF_NP], which
is a function that bounds interference in a non-preemptive stage
of execution. We prove that this function can be instantiated
with a constant function [λ F Δ ⟹ F - task_rtct tsk]. *)
Let IBF_NP (F : duration) (Δ : duration) := F - task_rtct tsk.
(** Let us re-iterate on the intuitive interpretation of this
function. Since [F] is a solution to the first equation
[task_rtct tsk + IBF_P tsk A F <= F], we know that by time
instant [t1 + F] a job receives [task_rtct tsk] units of service
and, hence, it becomes non-preemptive. Given this information,
how can we bound the job's interference in an interval <<[t1, t1
+ R)>>? Note that this interval starts with the beginning of the
busy interval. We know that the job receives [F - task_rtct tsk]
units of interference, and there will no more
interference. Hence, [IBF_NP tsk F Δ := F - task_rtct tsk]. *)
Lemma nonpreemptive_interference_is_bounded :
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk interference_bound_function).
Proof.
move => t1 t2 Δ j ARR TSK BUSY LT NCOM F RTC; specialize (RTC _ _ BUSY).
have POS : 0 < job_cost j.
{ move_neq_up ZE; move: ZE; rewrite leqn0; move => /eqP ZE.
move: NCOM => /negP NCOM; apply: NCOM.
by rewrite /completed_by ZE.
}
move: (BUSY) => [PREF _].
move : (TSK) (BUSY) RTC => /eqP TSKeq [[/andP [LE1 LE2] [QT1 AQT]] QT2] [LEQ RTC].
rewrite leq_subRL_impl // addnC -/cumulative_interference.
destruct (leqP t2 (t1 + F)) as [NEQ1|NEQ1]; last destruct (leqP F Δ) as [NEQ2|NEQ2].
{ rewrite -leq_subLR in NEQ1.
rewrite -(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) //
(leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) //.
rewrite (leqRW (cumulative_interference_sub _ _ t1 _ t1 t2 _ _)) //.
have LLL : (t1 < t2) = true by apply leq_ltn_trans with (t1 + Δ); lia.
interval_to_duration t1 t2 k.
eapply leq_trans.
- by rewrite addnC; (eapply service_and_interference_bounded with (t := t1) (t3 := t1+k)
|| eapply service_and_interference_bounded with (t := t1) (t2 := t1+k)).
- lia.
}
{ have NoInterference: cumulative_interference j (t1 + F) (t1 + Δ) = 0.
{ rewrite /cumulative_interference /cumul_cond_interference big_nat.
apply big1; move => t /andP [GE__t LT__t].
apply/eqP; rewrite eqb0; apply/negP; eapply H_work_conserving => //.
{ by apply/andP; split; lia. }
apply: H_ideal_progress_proc_model.
apply: job_nonpreemptive_after_run_to_completion_threshold GE__t _ _ => //.
- by rewrite -(leqRW RTC); apply H_valid_run_to_completion_threshold.
- by move: NCOM; apply contra; apply completion_monotonic; lia.
}
rewrite (leqRW RTC); erewrite cumulative_interference_cat with (t := t1 + F); last by lia.
rewrite /cumulative_interference in NoInterference.
rewrite NoInterference addn0; erewrite no_service_before_busy_interval => //.
by rewrite addnC; apply: service_and_interference_bounded.
}
{ rewrite (leqRW RTC) (leqRW (cumulative_interference_sub _ _ t1 _ t1 (t1 + F) _ _ )); try lia.
erewrite no_service_before_busy_interval => //.
by rewrite addnC; eapply service_and_interference_bounded. }
Qed.
(** For simplicity, let's define a local name for the search space. *)
Let is_in_search_space A := is_in_search_space L interference_bound_function A.
(** Consider any value [R] that upper-bounds the solution of each
response-time recurrence, i.e., for any relative arrival time A
in the search space, there exists a corresponding solution [F]
such that [F + (task_cost tsk - task_rtc tsk) <= R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum_ideal :
forall A,
is_in_search_space A ->
exists F,
task_rtct tsk + interference_bound_function A (A + F) <= A + F /\
F + (task_cost tsk - task_rtct tsk) <= R.
(** Using the lemma about [IBF_NP], we instantiate the general RTA
theorem's result to the ideal uniprocessor's case to prove that
[R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound_ideal :
task_response_time_bound arr_seq sched tsk R.
Proof.
eapply uniprocessor_response_time_bound with (IBF_NP := fun F Δ => F - task_rtct tsk) => //.
{ by apply nonpreemptive_interference_is_bounded. }
{ move => F _.
destruct (leqP F (task_rtct tsk)) as [NEQ|NEQ].
- eapply leq_trans; [apply NEQ | ].
by eapply leq_trans; [apply H_valid_run_to_completion_threshold | lia].
- by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
}
{ move => A SP; specialize (H_R_is_maximum_ideal A SP).
destruct H_R_is_maximum_ideal as [F [EQ1 EQ2]].
exists (A + F); split=> [//|].
eapply leq_trans; [ | by erewrite leq_add2l; apply EQ2].
by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
}
Qed.
End AbstractRTAIdeal.
analysis/abstract/ideal/abstract_seq_rta.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.analysis.facts.model.task_schedule.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Require Export prosa.analysis.abstract.IBF.task.
(** * Abstract Response-Time Analysis with sequential tasks *)
(** In this section we propose the general framework for response-time
analysis (RTA) of uni-processor scheduling of real-time tasks with
arbitrary arrival models and sequential tasks. *)
(** We prove that the maximum among the solutions of the response-time
bound recurrence for some set of parameters is a response-time
bound for [tsk]. Note that in this section we _do_ rely on the
hypothesis about task sequentiality. This allows us to provide a
more precise response-time bound function, since jobs of the same
task will be executed strictly in the order they arrive. *)
Section Sequential_Abstract_RTA.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
(** Consider any kind of ideal uni-processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
(** Consider any valid arrival sequence with consistent, non-duplicate arrivals...*)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any ideal schedule of this arrival sequence. *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Consider an arbitrary task set. *)
Variable ts : list Task.
(** Let [tsk] be any task in ts that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Consider a valid preemption model ... *)
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** ...and a valid task run-to-completion threshold function. That
is, [task_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for
any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
(** Let [max_arrivals] be a family of valid arrival curves, i.e.,
for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and (2) it is a monotonic function that equals
[0] for the empty interval [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Unlike the previous theorem
[uniprocessor_response_time_bound_ideal], we assume that (1)
tasks are sequential, moreover (2) functions interference and
interfering_workload are consistent with the hypothesis of
sequential tasks. *)
Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
(** Assume we have a constant [L] that bounds the busy interval of
any of [tsk]'s jobs. *)
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Next, we assume that [task_IBF] is a bound on interference
incurred by the task. *)
Variable task_IBF : duration -> duration -> duration.
Hypothesis H_task_interference_is_bounded :
task_interference_is_bounded_by arr_seq sched tsk task_IBF.
(** Let us abbreviate task [tsk]'s RBF for clarity. *)
Let task_rbf := task_request_bound_function tsk.
(** Given any job [j] of task [tsk] that arrives exactly [A] units
after the beginning of the busy interval, the bound on the total
interference incurred by [j] within an interval of length [Δ] is
no greater than [task_rbf (A + ε) - task_cost tsk + task's IBF
Δ]. Note that in case of sequential tasks the bound consists of
two parts: (1) the part that bounds the interference received
from other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost
tsk] and (2) any other interference that is bounded by
[task_IBF(tsk, A, Δ)]. *)
Let total_interference_bound (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + task_IBF A Δ.
(** Note that since we consider the modified interference bound
function, the search space has also changed. One can see that
the new search space is guaranteed to include any A for which
[task_rbf (A) ≠ task_rbf (A + ε)], since this implies the fact
that [total_interference_bound (A, Δ) ≠ total_interference_bound
(A + ε, Δ)]. *)
Let is_in_search_space_seq := is_in_search_space L total_interference_bound.
(** Consider any value [R], and assume that for any relative arrival
time [A] from the search space there is a solution [F] of the
response-time recurrence that is bounded by [R]. In contrast to
the formula in "non-sequential" Abstract RTA, assuming that
tasks are sequential leads to a more precise response-time
bound. Now we can explicitly express the interference caused by
other jobs of the task under consideration.
To understand the right part of the fix-point in the equation,
it is helpful to note that the bound on the total interference
([bound_of_total_interference]) is equal to [task_rbf (A + ε) -
task_cost tsk + task_IBF tsk A Δ]. Besides, a job must receive
enough service to become non-preemptive [task_lock_in_service
tsk]. The sum of these two quantities is exactly the right-hand
side of the equation. *)
Variable R : duration.
Hypothesis H_R_is_maximum_seq :
forall (A : duration),
is_in_search_space_seq A ->
exists (F : duration),
A + F >= (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_IBF A (A + F)
/\ R >= F + (task_cost tsk - task_rtct tsk).
(** Since we are going to use the
[uniprocessor_response_time_bound_ideal] theorem to prove the
theorem of this section, we have to show that all the hypotheses
are satisfied. Namely, we need to show that [H_R_is_maximum_seq]
implies [H_R_is_maximum]. Note that the fact that hypotheses
[H_sequential_tasks, H_i_w_are_task_consistent and
H_task_interference_is_bounded_by] imply
[H_job_interference_is_bounded] is proven in the file
[analysis/abstract/IBF/task]. *)
(** In this section, we prove that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
(** To rule out pathological cases with the [H_R_is_maximum_seq]
equation (such as [task_cost tsk] being greater than [task_rbf
(A + ε)]), we assume that the arrival curve is
non-pathological. *)
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
(** For simplicity, let's define a local name for the search space. *)
Let is_in_search_space A :=
is_in_search_space L total_interference_bound A.
(** We prove that [H_R_is_maximum] holds. *)
Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
A + F >= task_rtct tsk +
(task_rbf (A + ε) - task_cost tsk + task_IBF A (A + F))
/\ R >= F + (task_cost tsk - task_rtct tsk).
Proof.
move: H_valid_run_to_completion_threshold => [PRT1 PRT2]; move => A INSP.
clear H_sequential_tasks H_interference_and_workload_consistent_with_sequential_tasks.
move: (H_R_is_maximum_seq _ INSP) => [F [FIX LE]].
exists F; split=> [|//].
rewrite -{2}(leqRW FIX).
rewrite addnA leq_add2r.
rewrite addnBA; last first.
{ apply leq_trans with (task_rbf 1).
- exact: task_rbf_1_ge_task_cost.
- by apply: task_rbf_monotone => //; rewrite addn1.
}
by rewrite subnBA; auto; rewrite addnC.
Qed.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
(** We apply the [uniprocessor_response_time_bound_ideal] theorem,
and using the lemmas proven earlier, we prove that all the
requirements are satisfied. So, [R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound_seq :
task_response_time_bound arr_seq sched tsk R.
Proof.
move => j ARR TSK.
eapply uniprocessor_response_time_bound_ideal => //.
{ exact: task_IBF_implies_job_IBF => //. }
{ exact: max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis => //. }
Qed.
End Sequential_Abstract_RTA.
analysis/abstract/ideal/cumulative_bounds.v 0 → 100644
View file @ a162d510
Require Export analysis.abstract.ideal.iw_instantiation.
(** In this file, we prove some inequalities that always
hold inside the busy interval of a job. Throughout this file we
assume the ideal uniprocessor model. *)
Section BusyIntervalInequalities.
(** Consider any kind of tasks and their jobs, each characterized by
an arrival time, a cost, and an arbitrary notion of readiness. *)
Context {Task : TaskType} {Job : JobType} `{JobTask Job Task}.
Context `{JobArrival Job} `{JobCost Job} {JR :JobReady Job (ideal.processor_state Job)}.
(** Consider a JLFP policy that is reflexive and respects sequential tasks. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_policy_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_policy_respecsts_sequential_tasks : policy_respects_sequential_tasks JLFP.
(** Consider a consistent arrival sequence that does not contain duplicates. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Consider any valid ideal uniprocessor schedule defined over this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
(** Consider a set of tasks [ts] that contains all the jobs in the
arrival sequence. *)
Variable ts : list Task.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Consider a task [tsk]. *)
Variable tsk : Task.
(** Consider a job [j] of the task [tsk] that has a positive job cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive: job_cost_positive j.
(** Consider the ideal JLFP definitions of interference and
interfering workload. *)
#[local] Instance ideal_jlfp_interference : Interference Job :=
ideal_jlfp_interference arr_seq sched.
#[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
ideal_jlfp_interfering_workload arr_seq sched.
(** Consider the busy interval for j is given by <<[t1,t2)>>. *)
Variable t1 t2 : duration.
Hypothesis H_busy_interval : definitions.busy_interval sched j t1 t2.
(** Let us denote the relative arrival time by [A]. *)
Let A := job_arrival j - t1.
(** Consider any arbitrary time [Δ] inside the busy interval. *)
Variable Δ : duration.
Hypothesis H_Δ_in_busy : t1 + Δ <= t2.
(** First, we prove that if the priority inversion is bounded then,
the cumulative priority inversion is also bounded. *)
Section PIBound.
(** Consider the priority inversion in any given interval
is bounded by a constant. *)
Variable priority_inversion_bound : duration -> duration.
Hypothesis H_priority_inversion_is_bounded :
priority_inversion_is_bounded_by arr_seq sched tsk priority_inversion_bound.
(** Then, the cumulative priority inversion in any interval
is also bounded. *)
Lemma cumulative_priority_inversion_is_bounded:
cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ)
<= priority_inversion_bound (job_arrival j - t1).
Proof.
apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t2).
- rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //=; try by lia.
by rewrite /priority_inversion leq_addr.
- apply: H_priority_inversion_is_bounded => //.
by move: H_busy_interval; rewrite -instantiated_busy_interval_equivalent_busy_interval // => -[PREF _].
Qed.
End PIBound.
(** Let [jobs] denote the arrivals in the interval [Δ]. *)
Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
(** Next, we prove that the cumulative interference from higher priority
jobs of other tasks in an interval is bounded by the total service
received by the higher priority jobs of those tasks. *)
Lemma cumulative_interference_is_bounded_by_total_service:
cumulative_another_task_hep_job_interference arr_seq sched j t1 (t1 + Δ)
<= service_of_jobs sched (fun jo => another_task_hep_job jo j) jobs t1 (t1 + Δ).
Proof.
move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
rewrite cumulative_i_thep_eq_service_of_othep => //.
have /eqP TSK := H_job_of_tsk.
by rewrite instantiated_quiet_time_equivalent_quiet_time.
Qed.
End BusyIntervalInequalities.
analysis/abstract/ideal/iw_instantiation.v 0 → 100644
View file @ a162d510
Require Export prosa.analysis.facts.busy_interval.carry_in.
Require Export prosa.analysis.abstract.IBF.task.
Require Export prosa.analysis.facts.interference.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
Require Export prosa.analysis.facts.model.ideal.priority_inversion.
(** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
(** In this module we instantiate functions Interference and
Interfering Workload for ideal uni-processor schedulers with an
arbitrary JLFP-policy that satisfies the sequential-tasks
hypothesis. We also prove equivalence of Interference and
Interfering Workload to the more conventional notions of service
or workload. *)
Section JLFPInstantiation.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any valid arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any ideal uni-processor schedule of this arrival
sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after
completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Consider a JLFP-policy that indicates a higher-or-equal priority
relation, and assume that this relation is reflexive and
transitive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
(** We also assume that the policy respects sequential tasks,
meaning that later-arrived jobs of a task don't have higher
priority than earlier-arrived jobs of the same task. *)
Hypothesis H_JLFP_respects_sequential_tasks :
policy_respects_sequential_tasks JLFP.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** * Interference and Interfering Workload *)
(** In the following, we introduce definitions of interference,
interfering workload and a function that bounds cumulative
interference. *)
(** ** Instantiation of Interference *)
(** Before we define the notion of interference, we need to recall
the definition of priority inversion. We say that job [j] is
incurring a priority inversion at time [t] if there exists a job
with lower priority that executes at time [t]. In order to
simplify things, we ignore the fact that according to this
definition a job can incur priority inversion even before its
release (or after completion). All such (potentially bad) cases
do not cause problems, as each job is analyzed only within the
corresponding busy interval where the priority inversion behaves
in the expected way. *)
(** We say that job [j] incurs interference at time [t] iff it
cannot execute due to a higher-or-equal-priority job being
scheduled, or if it incurs a priority inversion. *)
#[local,program] Instance ideal_jlfp_interference : Interference Job :=
{
interference (j : Job) (t : instant) :=
priority_inversion arr_seq sched j t
|| another_hep_job_interference arr_seq sched j t
}.
(** ** Instantiation of Interfering Workload *)
(** The interfering workload, in turn, is defined as the sum of the
priority inversion predicate and interfering workload of jobs
with higher or equal priority. *)
#[local,program] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
{
interfering_workload (j : Job) (t : instant) :=
priority_inversion arr_seq sched j t
+ other_hep_jobs_interfering_workload arr_seq j t
}.
(** ** Equivalences *)
(** In this section we prove useful equivalences between the
definitions obtained by instantiation of definitions from the
Abstract RTA module (interference and interfering workload) and
definitions corresponding to the conventional concepts.
Instantiated functions of interference and interfering workload
usually do not have any useful lemmas about them. However, it is
possible to prove their equivalence to the more conventional
notions like service or workload. Next, we prove the equivalence
between the instantiations and conventional notions as well as a
few useful rewrite rules. *)
Section Equivalences.
(** In the following subsection, we prove properties of the
introduced functions under the assumption that the schedule is
idle. *)
Section IdleSchedule.
(** Consider a time instant [t] ... *)
Variable t : instant.
(** ... and assume that the schedule is idle at [t]. *)
Hypothesis H_idle : ideal_is_idle sched t.
(** We prove that in this case: ... *)
(** ... there is no interference, ... *)
Lemma no_interference_when_idle :
forall j, ~~ interference j t.
Proof.
move => j; apply/negP.
rewrite /interference /ideal_jlfp_interference => /orP [PI | HEPI].
- have [j' schj'] : exists j' : Job, scheduled_at sched j' t
by exact/priority_inversion_scheduled_at.
exact: ideal_sched_implies_not_idle schj' H_idle.
- by move: HEPI => /negPn; rewrite no_hep_job_interference_when_idle // is_idle_def //.
Qed.
(** ... as well as no interference for [tsk]. *)
Lemma no_task_interference_when_idle :
forall j, ~~ task_interference arr_seq sched j t.
Proof.
move=> j; rewrite /task_interference /cond_interference.
by rewrite negb_and; apply/orP; right; apply no_interference_when_idle.
Qed.
End IdleSchedule.
(** Next, we prove properties of the introduced functions under
the assumption that the scheduler is not idle. *)
Section ScheduledJob.
(** Consider a job [j] of task [tsk]. In this subsection, job
[j] is deemed to be the main job with respect to which the
functions are computed. *)
Variable j : Job.
Hypothesis H_j_tsk : job_of_task tsk j.
(** Consider a time instant [t]. *)
Variable t : instant.
(** In the next subsection, we consider a case when a job [j']
from the same task (as job [j]) is scheduled. *)
Section FromSameTask.
(** Consider a job [j'] that comes from task [tsk] and is
scheduled at time instant [t]. *)
Variable j' : Job.
Hypothesis H_j'_tsk : job_of_task tsk j'.
Hypothesis H_j'_sched : scheduled_at sched j' t.
(** Similarly, there is no task interference, since in order
to incur the task interference, a job from a distinct task
must be scheduled. *)
Lemma task_interference_eq_false :
~~ task_interference arr_seq sched j t.
Proof.
apply/negP; move => /andP [+ _]; rewrite /nonself /task_scheduled_at.
rewrite task_served_eq_task_scheduled //=; erewrite job_of_scheduled_task => //.
move: H_j_tsk H_j'_tsk; rewrite /job_of_task => /eqP -> /eqP ->.
by rewrite eq_refl.
Qed.
End FromSameTask.
(** In the next subsection, we consider a case when a job [j']
from a task other than [j]'s task is scheduled. *)
Section FromDifferentTask.
(** Consider a job [j'] that _does_ _not_ comes from task
[tsk] and is scheduled at time instant [t]. *)
Variable j' : Job.
Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.
Hypothesis H_j'_sched : scheduled_at sched j' t.
(** Hence, if we assume that [j'] has higher-or-equal priority, ... *)
Hypothesis H_j'_hep : hep_job j' j.
(** Moreover, in this case, task [tsk] also incurs interference. *)
Lemma sched_athep_implies_task_interference :
task_interference arr_seq sched j t.
Proof.
apply/andP; split.
- rewrite /nonself task_served_eq_task_scheduled => //.
apply: job_of_other_task_scheduled => //.
by move: H_j_tsk => /eqP -> .
- apply/orP; right.
apply/hasP; exists j'.
+ by apply scheduled_at_implies_in_served_at => //.
+ rewrite another_hep_job_diff_task // same_task_sym.
exact: (diff_task tsk).
Qed.
End FromDifferentTask.
End ScheduledJob.
(** We prove that we can split cumulative interference into two
parts: (1) cumulative priority inversion and (2) cumulative
interference from jobs with higher or equal priority. *)
Lemma cumulative_interference_split :
forall j t1 t2,
cumulative_interference j t1 t2
= cumulative_priority_inversion arr_seq sched j t1 t2
+ cumulative_another_hep_job_interference arr_seq sched j t1 t2.
Proof.
rewrite /cumulative_interference /cumul_cond_interference /cond_interference /interference.
move=> j t1 t2; rewrite -big_split //=.
apply/eqP; rewrite eqn_leq; apply/andP; split; rewrite leq_sum//.
{ move => t _; unfold ideal_jlfp_interference.
by destruct (priority_inversion _ _ _ _), (another_hep_job_interference arr_seq sched j t).
}
{ move => t _; rewrite /ideal_jlfp_interference.
destruct (ideal_proc_model_sched_case_analysis sched t) as [IDLE | [s SCHED]].
- have -> : priority_inversion arr_seq sched j t = false
by exact/negbTE/idle_implies_no_priority_inversion.
by rewrite add0n.
- destruct (hep_job s j) eqn:PRIO.
+ by erewrite sched_hep_implies_no_priority_inversion => //; rewrite add0n.
+ erewrite !sched_lp_implies_priority_inversion => //; last by rewrite PRIO.
rewrite orTb.
by rewrite add1n ltnS //= leqn0 eqb0; erewrite no_ahep_interference_when_scheduled_lp; last by erewrite PRIO.
}
Qed.
(** Similarly, we prove that we can split cumulative interfering
workload into two parts: (1) cumulative priority inversion and
(2) cumulative interfering workload from jobs with higher or
equal priority. *)
Lemma cumulative_interfering_workload_split :
forall j t1 t2,
cumulative_interfering_workload j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t2
+ cumulative_other_hep_jobs_interfering_workload arr_seq j t1 t2.
Proof.
rewrite /cumulative_interfering_workload
/cumulative_priority_inversion
/cumulative_other_hep_jobs_interfering_workload.
by move => j t1 t2; rewrite -big_split //=.
Qed.
(** Let [j] be any job of task [tsk]. Then the cumulative task
interference received by job [j] is bounded to the sum of the
cumulative priority inversion of job [j] and the cumulative
interference incurred by job [j] due to higher-or-equal
priority jobs from other tasks. *)
Lemma cumulative_task_interference_split :
forall j t1 t2,
arrives_in arr_seq j ->
job_of_task tsk j ->
~~ completed_by sched j t2 ->
cumul_task_interference arr_seq sched j t1 t2
<= cumulative_priority_inversion arr_seq sched j t1 t2
+ cumulative_another_task_hep_job_interference arr_seq sched j t1 t2.
Proof.
move=> j t1 R ARR TSK NCOMPL.
rewrite /cumul_task_interference /cumul_cond_interference.
rewrite -big_split //= big_seq_cond [leqRHS]big_seq_cond.
apply leq_sum; move => t /andP [IN _].
rewrite /cond_interference /nonself /interference /ideal_jlfp_interference.
have [IDLE|[s SCHEDs]] := ideal_proc_model_sched_case_analysis sched t.
{ move: (IDLE) => IIDLE; erewrite <-is_idle_def in IDLE => //.
have ->: priority_inversion arr_seq sched j t = false
by apply/eqP; rewrite eqbF_neg; apply: no_priority_inversion_when_idle => //.
have ->: another_hep_job_interference arr_seq sched j t = false
by apply/eqP; rewrite eqbF_neg; apply no_hep_job_interference_when_idle.
have ->: another_task_hep_job_interference arr_seq sched j t = false
by apply/eqP; rewrite eqbF_neg; apply/negP; rewrite_neg @no_hep_task_interference_when_idle.
by rewrite andbF.
}
{ rewrite (interference_ahep_def _ _ _ _ _ _ _ _ _ _ _ SCHEDs) //.
rewrite (interference_athep_def _ _ _ _ _ _ _ _ _ _ _ SCHEDs) => //.
rewrite (priority_inversion_equiv_sched_lower_priority _ _ _ _ _ _ _ _ _ SCHEDs) => //.
rewrite task_served_eq_task_scheduled // (job_of_scheduled_task _ _ _ _ _ _ _ _ _ SCHEDs) => //.
rewrite /another_hep_job /another_task_hep_job.
have [EQj|NEQj] := eqVneq s j.
{ by subst; rewrite /job_of_task eq_refl H_priority_is_reflexive. }
have [/eqP EQt|NEQt] := eqVneq (job_task s) (job_task j).
{ apply/eqP; move: (EQt) => /eqP <-.
by rewrite /job_of_task eq_refl //= andbF addn0 eq_sym eqb0; apply/negP => LPs. }
{ by rewrite /job_of_task NEQt //= andbT; case: hep_job. }
}
Qed.
(** In this section, we prove that the (abstract) cumulative
interfering workload is equivalent to the conventional workload,
i.e., the one defined with concrete schedule parameters. *)
Section InstantiatedWorkloadEquivalence.
(** Let <<[t1,t2)>> be any time interval. *)
Variables t1 t2 : instant.
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Then for any job [j], the cumulative interfering workload is
equal to the conventional workload. *)
Lemma cumulative_iw_hep_eq_workload_of_ohep :
cumulative_other_hep_jobs_interfering_workload arr_seq j t1 t2
= workload_of_other_hep_jobs arr_seq j t1 t2.
Proof.
rewrite /cumulative_other_hep_jobs_interfering_workload /workload_of_other_hep_jobs.
case NEQ: (t1 < t2); last first.
{ move: NEQ => /negP /negP; rewrite -leqNgt; move => NEQ.
rewrite big_geq//.
rewrite /arrivals_between /arrival_sequence.arrivals_between big_geq//.
by rewrite /workload_of_jobs big_nil.
}
{ unfold other_hep_jobs_interfering_workload, workload_of_jobs.
interval_to_duration t1 t2 k.
elim: k => [|k IHk].
- rewrite !addn0.
rewrite big_geq//.
rewrite /arrivals_between /arrival_sequence.arrivals_between big_geq//.
by rewrite /workload_of_jobs big_nil.
- rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
rewrite IHk.
rewrite /arrivals_between /arrival_sequence.arrivals_between big_nat_recr //=.
+ by rewrite big_cat.
+ by rewrite leq_addr.
}
Qed.
End InstantiatedWorkloadEquivalence.
(** In this section we prove that the abstract definition of busy
interval is equivalent to the conventional, concrete
definition of busy interval for JLFP scheduling. *)
Section BusyIntervalEquivalence.
(** In order to avoid confusion, we denote the notion of a quiet
time in the _classical_ sense as [quiet_time_cl], and the
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
Let quiet_time_cl := classical.quiet_time arr_seq sched.
Let quiet_time_ab := abstract.definitions.quiet_time sched.
(** Same for the two notions of a busy interval prefix ... *)
Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
(** ... and the two notions of a busy interval. *)
Let busy_interval_cl := classical.busy_interval arr_seq sched.
Let busy_interval_ab := abstract.definitions.busy_interval sched.
(** Consider any job j of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** To show the equivalence of the notions of busy intervals, we
first show that the notions of quiet time are also
equivalent. *)
(** First, we show that the classical notion of quiet time
implies the abstract notion of quiet time. *)
Lemma quiet_time_cl_implies_quiet_time_ab :
forall t, quiet_time_cl j t -> quiet_time_ab j t.
Proof.
clear H_JLFP_respects_sequential_tasks.
have zero_is_quiet_time: forall j, quiet_time_cl j 0.
{ by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
move=> t QT; apply/andP; split; last first.
{ rewrite negb_and negbK; apply/orP.
by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
{ erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
rewrite cumulative_i_ohep_eq_service_of_ohep//.
rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
apply all_jobs_have_completed_equiv_workload_eq_service => //.
move => j0 IN HEP; apply QT.
- by apply in_arrivals_implies_arrived in IN.
- by move: HEP => /andP [H6 H7].
- by apply in_arrivals_implies_arrived_between in IN.
}
Qed.
(** And vice versa, the abstract notion of quiet time implies
the classical notion of quiet time. *)
Lemma quiet_time_ab_implies_quiet_time_cl :
forall t, quiet_time_ab j t -> quiet_time_cl j t.
Proof.
clear H_JLFP_respects_sequential_tasks.
have zero_is_quiet_time: forall j, quiet_time_cl j 0.
{ by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
move => t /andP [T0 T1] jhp ARR HP ARB.
eapply all_jobs_have_completed_equiv_workload_eq_service with
(P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t) => //.
erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
rewrite -/(service_of_other_hep_jobs arr_seq _ j 0 t) -cumulative_i_ohep_eq_service_of_ohep => //.
rewrite -/(workload_of_other_hep_jobs _ j 0 t) -cumulative_iw_hep_eq_workload_of_ohep; eauto.
move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
{ have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
{ move => j__copy IN; apply negbTE.
rewrite negb_and; apply/orP; right; apply/negPn/eqP => EQ; subst j__copy.
move: NA => /negP CONTR; apply: CONTR.
by apply in_arrivals_implies_arrived_between in IN. }
erewrite service_of_jobs_equiv_pred with (P2 := pred0) => [|//].
erewrite workload_of_jobs_equiv_pred with (P' := pred0) => [|//].
move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
by erewrite workload_of_jobs_pred0, service_of_jobs_pred0.
}
{ have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j0 : Job => hep_job j0 j && ~~ (j0 != j)) =1 eq_op j}.
{ move => j__copy IN.
replace (~~ (j__copy != j)) with (j__copy == j); last by case: (j__copy == j).
rewrite eq_sym; destruct (j == j__copy) eqn:EQ; last by rewrite Bool.andb_false_r.
by move: EQ => /eqP EQ; rewrite Bool.andb_true_r; apply/eqP; rewrite eqb_id; subst. }
erewrite service_of_jobs_equiv_pred with (P2 := eq_op j) => [|//].
erewrite workload_of_jobs_equiv_pred with (P' := eq_op j) => [|//].
move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
apply/eqP; eapply all_jobs_have_completed_equiv_workload_eq_service with
(P := eq_op j) (t1 := 0) (t2 := t) => //.
by move => j__copy _ /eqP EQ; subst j__copy.
}
Qed.
(** The equivalence trivially follows from the lemmas above. *)
Corollary instantiated_quiet_time_equivalent_quiet_time :
forall t,
quiet_time_cl j t <-> quiet_time_ab j t.
Proof.
clear H_JLFP_respects_sequential_tasks.
move => ?; split.
- by apply quiet_time_cl_implies_quiet_time_ab.
- by apply quiet_time_ab_implies_quiet_time_cl.
Qed.
(** Based on that, we prove that the concept of busy interval
prefix obtained by instantiating the abstract definition of
busy interval prefix coincides with the conventional
definition of busy interval prefix. *)
Lemma instantiated_busy_interval_prefix_equivalent_busy_interval_prefix :
forall t1 t2, busy_interval_prefix_cl j t1 t2 <-> busy_interval_prefix_ab j t1 t2.
Proof.
move => t1 t2; split.
{ move => [NEQ [QTt1 [NQT REL]]].
split=> [//|]; split.
- by apply instantiated_quiet_time_equivalent_quiet_time in QTt1.
- by move => t NE QT; eapply NQT; eauto 2; apply instantiated_quiet_time_equivalent_quiet_time.
}
{ move => [/andP [NEQ1 NEQ2] [QTt1 NQT]].
split; [ | split; [ |split] ].
- by apply leq_ltn_trans with (job_arrival j).
- by eapply instantiated_quiet_time_equivalent_quiet_time.
- by move => t NEQ QT; eapply NQT; eauto 2; eapply instantiated_quiet_time_equivalent_quiet_time in QT.
- by apply/andP.
}
Qed.
(** Similarly, we prove that the concept of busy interval
obtained by instantiating the abstract definition of busy
interval coincides with the conventional definition of busy
interval. *)
Lemma instantiated_busy_interval_equivalent_busy_interval :
forall t1 t2, busy_interval_cl j t1 t2 <-> busy_interval_ab j t1 t2.
Proof.
move => t1 t2; split.
{ move => [PREF QTt2]; split.
- by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- by eapply instantiated_quiet_time_equivalent_quiet_time in QTt2.
}
{ move => [PREF QTt2]; split.
- by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- by eapply instantiated_quiet_time_equivalent_quiet_time.
}
Qed.
(** For the sake of proof automation, we note the frequently needed
special case of an abstract busy window implying the existence of a
classic quiet time. *)
Fact abstract_busy_interval_classic_quiet_time :
forall t1 t2,
busy_interval_ab j t1 t2 -> quiet_time_cl j t1.
Proof.
by move=> ? ? /instantiated_busy_interval_equivalent_busy_interval [[_ [? _]] _].
Qed.
(** Also for automation, we note a similar fact about classic busy-window prefixes. *)
Fact abstract_busy_interval_classic_busy_interval_prefix :
forall t1 t2,
busy_interval_ab j t1 t2 -> busy_interval_prefix_cl j t1 t2.
Proof. by move=> ? ? /instantiated_busy_interval_equivalent_busy_interval [+ _]. Qed.
End BusyIntervalEquivalence.
End Equivalences.
(** In this section we prove some properties about the interference
and interfering workload as defined in this file. *)
Section I_IW_correctness.
(** Consider work-bearing readiness. *)
Context `{!JobReady Job (ideal.processor_state Job)}.
Hypothesis H_work_bearing_readiness : work_bearing_readiness arr_seq sched.
(** Assume that the schedule is valid and work-conserving. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Note that we differentiate between abstract and classical
notions of work-conserving schedule. *)
Let work_conserving_ab := definitions.work_conserving arr_seq sched.
Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.
Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
(** We assume that the schedule is a work-conserving schedule in
the _classical_ sense, and later prove that the hypothesis
about abstract work-conservation also holds. *)
Hypothesis H_work_conserving : work_conserving_cl.
(** Assume the scheduling policy under consideration is reflexive. *)
Hypothesis H_policy_reflexive : reflexive_job_priorities JLFP.
(** In this section, we prove the correctness of interference
inside the busy interval, i.e., we prove that if interference
for a job is [false] then the job is scheduled and vice versa.
This property is referred to as abstract work conservation. *)
Section Abstract_Work_Conservation.
(** Consider a job [j] that is in the arrival sequence
and has a positive job cost. *)
Variable j : Job.
Hypothesis H_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : 0 < job_cost j.
(** Let the busy interval of the job be <<[t1,t2)>>. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix_ab j t1 t2.
(** Consider a time [t] inside the busy interval of the job. *)
Variable t : instant.
Hypothesis H_t_in_busy_interval : t1 <= t < t2.
(** First, we prove that if interference is [false] at a time
[t] then the job is scheduled. *)
Lemma not_interference_implies_scheduled :
~ interference j t -> receives_service_at sched j t.
Proof.
move => /negP HYP; move : HYP.
rewrite negb_or /another_hep_job_interference.
move => /andP [HYP1 HYP2].
have [Idle|[jo Sched_jo]] := ideal_proc_model_sched_case_analysis sched t.
{ exfalso; clear HYP1 HYP2.
eapply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in H_busy_interval_prefix => //.
apply: not_quiet_implies_not_idle => //.
by rewrite is_idle_def.
}
{ have PINV := negP HYP1.
have: ~~ another_hep_job jo j by apply: contraNN HYP2; erewrite <-interference_ahep_def => //.
rewrite negb_and => /orP [NHEP | EQ].
- rewrite/receives_service_at; move_neq_up ZS; move: ZS; rewrite leqn0 => /eqP ZS.
apply no_service_not_scheduled in ZS => //; apply: PINV.
exact/uni_priority_inversion_P.
- apply negbNE in EQ; move: EQ => /eqP EQ; subst jo.
by rewrite /receives_service_at service_at_is_scheduled_at Sched_jo.
}
Qed.
(** Conversely, if the job is scheduled at [t] then interference is [false]. *)
Lemma scheduled_implies_no_interference :
receives_service_at sched j t -> ~ interference j t.
Proof.
move=> RSERV /orP[PINV | INT].
- rewrite (sched_hep_implies_no_priority_inversion _ _ _ _ _ _ _ _ j) in PINV => //.
by rewrite /receives_service_at service_at_is_scheduled_at lt0b in RSERV.
- rewrite /receives_service_at service_at_is_scheduled_at lt0b in RSERV.
by move: INT; rewrite_neg @no_ahep_interference_when_scheduled.
Qed.
End Abstract_Work_Conservation.
(** Using the above two lemmas, we can prove that abstract work
conservation always holds for these instantiations of [I] and
[IW]. *)
Corollary instantiated_i_and_w_are_coherent_with_schedule :
work_conserving_ab.
Proof.
move => j t1 t2 t ARR POS BUSY NEQ; split.
- exact: (not_interference_implies_scheduled j ARR POS).
- exact: scheduled_implies_no_interference.
Qed.
(** Next, in order to prove that these definitions of [I] and [IW]
are consistent with sequential tasks, we need to assume that
the policy under consideration respects sequential tasks. *)
Hypothesis H_policy_respects_sequential_tasks : policy_respects_sequential_tasks JLFP.
(** We prove that these definitions of [I] and [IW] are consistent
with sequential tasks. *)
Lemma instantiated_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
Proof.
move => j t1 t2 ARR /eqP TSK POS BUSY.
eapply instantiated_busy_interval_equivalent_busy_interval in BUSY => //.
eapply all_jobs_have_completed_equiv_workload_eq_service => //.
move => s INs /eqP TSKs.
move: (INs) => NEQ.
eapply in_arrivals_implies_arrived_between in NEQ => //.
move: NEQ => /andP [_ JAs].
move: (BUSY) => [[ _ [QT [_ /andP [JAj _]]] _]].
apply QT => //; first exact: in_arrivals_implies_arrived.
apply H_policy_respects_sequential_tasks; first by rewrite TSK TSKs.
by apply leq_trans with t1; [lia |].
Qed.
(** Since interfering and interfering workload are sufficient to define the busy window,
next, we reason about the bound on the length of the busy window. *)
Section BusyWindowBound.
(** Consider an arrival curve. *)
Context `{MaxArrivals Task}.
(** Consider a set of tasks that respects the arrival curve. *)
Variable ts : list Task.
Hypothesis H_taskset_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.
(** Assume that all jobs come from this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Consider a constant [L] such that... *)
Variable L : duration.
(** ... [L] is greater than [0], and... *)
Hypothesis H_L_positive : L > 0.
(** [L] is the fixed point of the following equation. *)
Hypothesis H_fixed_point : L = total_request_bound_function ts L.
(** Assume all jobs have a valid job cost. *)
Hypothesis H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq.
(** Then, we prove that [L] is a bound on the length of the busy window. *)
Lemma instantiated_busy_intervals_are_bounded:
busy_intervals_are_bounded_by arr_seq sched tsk L.
Proof.
move => j ARR TSK POS.
edestruct busy_interval_from_total_workload_bound
with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]] => //.
{ move => t _; rewrite {3}H_fixed_point.
have ->: blackout_during sched t (t + L) = 0.
{ apply/eqP; rewrite /blackout_during big1 // => l _.
by rewrite /is_blackout ideal_proc_has_supply. }
by rewrite add0n; apply total_workload_le_total_rbf. }
exists t1, t2; split=> [//|]; split=> [//|].
by apply instantiated_busy_interval_equivalent_busy_interval.
Qed.
End BusyWindowBound.
End I_IW_correctness.
End JLFPInstantiation.
(** To preserve modularity and hide the implementation details of a
technical definition presented in this file, we make the
definition opaque. This way, we ensure that the system will treat
each of these definitions as a single entity. *)
Global Opaque another_hep_job_interference
another_task_hep_job_interference
ideal_jlfp_interference
ideal_jlfp_interfering_workload
cumulative_another_hep_job_interference
cumulative_another_task_hep_job_interference
cumulative_other_hep_jobs_interfering_workload
other_hep_jobs_interfering_workload.
(** We add some facts into the "Hint Database" basic_rt_facts, so Coq will be
able to apply them automatically where needed. *)
Global Hint Resolve
abstract_busy_interval_classic_quiet_time
abstract_busy_interval_classic_busy_interval_prefix
: basic_rt_facts.