Commit b40399b2 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Move interference bounds to analysis/

parent 95379048
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
# #
# This Makefile was generated by the command line : # This Makefile was generated by the command line :
# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./model/basic/schedulability.v ./model/basic/interference_bound_edf.v ./model/basic/task.v ./model/basic/interference_bound_fp.v ./model/basic/task_arrival.v ./model/basic/interference_bound.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/basic/workload_bound.v ./model/jitter/schedulability.v ./model/jitter/interference_bound_edf.v ./model/jitter/task.v ./model/jitter/interference_bound_fp.v ./model/jitter/task_arrival.v ./model/jitter/interference_bound.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v ./model/jitter/workload_bound.v -o Makefile # coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
# #
.DEFAULT_GOAL := all .DEFAULT_GOAL := all
...@@ -95,19 +95,24 @@ VFILES:=util/ssromega.v\ ...@@ -95,19 +95,24 @@ VFILES:=util/ssromega.v\
implementation/jitter/job.v\ implementation/jitter/job.v\
implementation/jitter/arrival_sequence.v\ implementation/jitter/arrival_sequence.v\
analysis/basic/bertogna_fp_theory.v\ analysis/basic/bertogna_fp_theory.v\
analysis/basic/interference_bound_edf.v\
analysis/basic/interference_bound_fp.v\
analysis/basic/interference_bound.v\
analysis/basic/bertogna_edf_comp.v\ analysis/basic/bertogna_edf_comp.v\
analysis/basic/bertogna_fp_comp.v\ analysis/basic/bertogna_fp_comp.v\
analysis/basic/bertogna_edf_theory.v\ analysis/basic/bertogna_edf_theory.v\
analysis/basic/workload_bound.v\
analysis/jitter/bertogna_fp_theory.v\ analysis/jitter/bertogna_fp_theory.v\
analysis/jitter/interference_bound_edf.v\
analysis/jitter/interference_bound_fp.v\
analysis/jitter/interference_bound.v\
analysis/jitter/bertogna_edf_comp.v\ analysis/jitter/bertogna_edf_comp.v\
analysis/jitter/bertogna_fp_comp.v\ analysis/jitter/bertogna_fp_comp.v\
analysis/jitter/bertogna_edf_theory.v\ analysis/jitter/bertogna_edf_theory.v\
analysis/jitter/workload_bound.v\
model/basic/schedulability.v\ model/basic/schedulability.v\
model/basic/interference_bound_edf.v\
model/basic/task.v\ model/basic/task.v\
model/basic/interference_bound_fp.v\
model/basic/task_arrival.v\ model/basic/task_arrival.v\
model/basic/interference_bound.v\
model/basic/platform.v\ model/basic/platform.v\
model/basic/schedule.v\ model/basic/schedule.v\
model/basic/priority.v\ model/basic/priority.v\
...@@ -118,13 +123,9 @@ VFILES:=util/ssromega.v\ ...@@ -118,13 +123,9 @@ VFILES:=util/ssromega.v\
model/basic/arrival_sequence.v\ model/basic/arrival_sequence.v\
model/basic/response_time.v\ model/basic/response_time.v\
model/basic/platform_fp.v\ model/basic/platform_fp.v\
model/basic/workload_bound.v\
model/jitter/schedulability.v\ model/jitter/schedulability.v\
model/jitter/interference_bound_edf.v\
model/jitter/task.v\ model/jitter/task.v\
model/jitter/interference_bound_fp.v\
model/jitter/task_arrival.v\ model/jitter/task_arrival.v\
model/jitter/interference_bound.v\
model/jitter/platform.v\ model/jitter/platform.v\
model/jitter/schedule.v\ model/jitter/schedule.v\
model/jitter/priority.v\ model/jitter/priority.v\
...@@ -134,8 +135,7 @@ VFILES:=util/ssromega.v\ ...@@ -134,8 +135,7 @@ VFILES:=util/ssromega.v\
model/jitter/job.v\ model/jitter/job.v\
model/jitter/arrival_sequence.v\ model/jitter/arrival_sequence.v\
model/jitter/response_time.v\ model/jitter/response_time.v\
model/jitter/platform_fp.v\ model/jitter/platform_fp.v
model/jitter/workload_bound.v
-include $(addsuffix .d,$(VFILES)) -include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES)) .SECONDARY: $(addsuffix .d,$(VFILES))
......
...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.workload_bound rt.model.basic.schedulability rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.priority rt.model.basic.platform rt.model.basic.response_time rt.model.basic.platform rt.model.basic.response_time.
rt.model.basic.interference_bound_edf. Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF. Module ResponseTimeAnalysisEDF.
......
...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.workload_bound rt.model.basic.schedulability rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.priority rt.model.basic.response_time rt.model.basic.response_time rt.model.basic.interference.
rt.model.basic.interference rt.model.basic.interference_bound_fp. Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP. Module ResponseTimeAnalysisFP.
......
Add LoadPath "../../" as rt. Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas. Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.schedule rt.model.basic.workload_bound. Require Import rt.model.basic.schedule.
Require Import rt.analysis.basic.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric. Module InterferenceBoundGeneric.
......
...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.workload_bound rt.model.basic.priority rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
rt.model.basic.schedulability rt.model.basic.interference rt.model.basic.interference rt.model.basic.interference_edf.
rt.model.basic.interference_edf rt.model.basic.interference_bound. Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDF. Module InterferenceBoundEDF.
......
Add LoadPath "../.." as rt. Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas. Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.workload_bound rt.model.basic.interference rt.model.basic.interference.
rt.model.basic.interference_bound. Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP. Module InterferenceBoundFP.
......
Add LoadPath "../.." as rt. Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.jitter.task rt.model.jitter.task_arrival Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference
rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.workload rt.model.jitter.schedulability
rt.model.jitter.priority rt.model.jitter.platform rt.model.jitter.response_time. rt.model.jitter.priority rt.model.jitter.platform rt.model.jitter.response_time.
Require Import rt.model.jitter.job rt.model.jitter.workload_bound Require Import rt.analysis.jitter.workload_bound
rt.model.jitter.interference_bound_edf. rt.analysis.jitter.interference_bound_edf.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDFJitter. Module ResponseTimeAnalysisEDFJitter.
......
...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.platform_fp rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.platform_fp
rt.model.jitter.workload rt.model.jitter.workload_bound rt.model.jitter.schedulability rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority
rt.model.jitter.priority rt.model.jitter.response_time rt.model.jitter.interference rt.model.jitter.response_time rt.model.jitter.interference.
rt.model.jitter.workload_bound rt.model.jitter.interference_bound_fp. Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound_fp.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP. Module ResponseTimeAnalysisFP.
......
...@@ -2,7 +2,7 @@ Add LoadPath "../../" as rt. ...@@ -2,7 +2,7 @@ Add LoadPath "../../" as rt.
Require Import rt.util.lemmas. Require Import rt.util.lemmas.
Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule
rt.model.jitter.interference rt.model.jitter.priority. rt.model.jitter.interference rt.model.jitter.priority.
Require Import rt.model.jitter.workload_bound. Require Import rt.analysis.jitter.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundJitter. Module InterferenceBoundJitter.
......
Add LoadPath "../../" as rt. Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround. Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.jitter.task rt.model.jitter.task_arrival Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
rt.model.jitter.interference rt.model.jitter.interference_edf. rt.model.jitter.interference rt.model.jitter.interference_edf.
Require Import rt.model.jitter.job rt.model.jitter.workload_bound rt.model.jitter.interference_bound. Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDFJitter. Module InterferenceBoundEDFJitter.
......
...@@ -2,7 +2,7 @@ Add LoadPath "../.." as rt. ...@@ -2,7 +2,7 @@ Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas. Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload
rt.model.jitter.interference. rt.model.jitter.interference.
Require Import rt.model.jitter.workload_bound rt.model.jitter.interference_bound. Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP. Module InterferenceBoundFP.
......
...@@ -2,9 +2,9 @@ Add LoadPath "../../" as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.divround. Require Import rt.util.Vbase rt.util.divround.
Require Import rt.model.basic.job rt.model.basic.task Require Import rt.model.basic.job rt.model.basic.task
rt.model.basic.schedule rt.model.basic.schedulability rt.model.basic.schedule rt.model.basic.schedulability
rt.model.basic.workload_bound rt.model.basic.priority rt.model.basic.platform.
rt.model.basic.interference_bound_edf Require Import rt.analysis.basic.workload_bound
rt.model.basic.priority rt.model.basic.platform rt.analysis.basic.interference_bound_edf
rt.analysis.basic.bertogna_edf_comp. rt.analysis.basic.bertogna_edf_comp.
Require Import rt.implementation.basic.job Require Import rt.implementation.basic.job
rt.implementation.basic.task rt.implementation.basic.task
......
...@@ -2,9 +2,9 @@ Add LoadPath "../../" as rt. ...@@ -2,9 +2,9 @@ Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.divround. Require Import rt.util.Vbase rt.util.divround.
Require Import rt.model.jitter.job rt.model.jitter.task Require Import rt.model.jitter.job rt.model.jitter.task
rt.model.jitter.schedule rt.model.jitter.schedulability rt.model.jitter.schedule rt.model.jitter.schedulability
rt.model.jitter.workload_bound rt.model.jitter.priority rt.model.jitter.platform.
rt.model.jitter.interference_bound_edf Require Import rt.analysis.jitter.workload_bound
rt.model.jitter.priority rt.model.jitter.platform rt.analysis.jitter.interference_bound_edf
rt.analysis.jitter.bertogna_edf_comp. rt.analysis.jitter.bertogna_edf_comp.
Require Import rt.implementation.jitter.job Require Import rt.implementation.jitter.job
rt.implementation.jitter.task rt.implementation.jitter.task
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment