...
 
Commits (114)
......@@ -7,6 +7,12 @@ Makefile*
_CoqProject
*.crashcoqide
*.v#
*#
*#*
dependtodot.cmi
dependtodot.cmo
*.cache
*~
*.orig
makedot: dependtodot.ml
ocamlc -o $@ -pp camlp4o $<
depend.dot:: $(VFILES) makedot
coqdep -f _CoqProject -noglob | grep -v -e '\.vio:' > depend
sed -i -e 's|[/0-9A-Za-z_]*\.v\.beautified||g' depend
./makedot depend
sed -i -e 's|\./|./rt.|g' $@
depend.png:: depend.dot
dot -Tpng $< -o $@
depend.html:: depend.dot
dot -Tcmapx $< -o $@
doc:: html depend.png depend.html
cp depend.png html/
if ! grep -e 'depend[.]png' html/toc.html; then \
sed -i html/toc.html \
-e 's,id=.main.>,&<img src='\''depend.png'\'' border=0 usemap='\''#depend'\'' />,' \
-e '/<img src='\''depend.png'\''/r depend.html'; \
fi
COQDOCFLAGS = -g --interpolate --utf8 --coqlib https://coq.inria.fr/distrib/current/stdlib/
......@@ -2,6 +2,18 @@
This repository contains the main Coq proof spec & proof development of the RT-PROOFS project.
## Compiling
Dependencies mathcomp and coquelicot can be installed easyli via opam:
```$ opam repo add coq-released https://coq.inria.fr/opam/released```
```$ opam install coq-mathcomp-algebra coq-coquelicot```
Then:
```$ ./create_makefile.sh```
```$ make -j4```
## Directory Structure
The Prosa directory is organized in a hierarchy: while generic, reusable foundations stay in
......@@ -18,6 +30,8 @@ Currently, Prosa contains the following base directories:
- **implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations.
Testing the main theorems in an assumption free environment shows the absence of contradictions.
- **network_calculus/:** a formalization of Network Calculus (ongoing work)
### Internal Directories
The major concepts in Prosa are specified in the *model/* folder.
......@@ -41,11 +55,32 @@ For example, the schedulability analysis for global scheduling with release jitt
- **analysis/global/jitter:** Analysis for global scheduling with release jitter.
- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter.
## Dependencies
- Coq (>= 8.5): http://coq.inria.fr/
- MathComp (>= 1.7): https://github.com/math-comp/math-comp/
- Coquelicot (>= 2.1.1): http://coquelicot.saclay.inria.fr/
The easiest way to install them is to use Opam :
```
$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam install coq coq-mathcomp-algebra coq-coquelicot
```
## Compiling
```
$ ./create_makefile.sh
$ make
```
## Generating HTML Documentation
The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with `Make`:
```$ make gallinahtml -j4```
```$ make doc```
Then look at html/toc.html with your favorite browser.
Since Coqdoc requires object files as input, please make sure that the code is compilable.
......
* Les trucs urgents :Done:
** DONE residual server ré-écriture [3/3]
- [X] faire un server contraint
- [X] Definir residual serveer contraint
- [X] Ajouter dans definition fifo delay.
* Ré-écriture :Done:
** DONE Reprendre les sup et inf selon l'écriture : \sup_{ t \in R}{ ___ | P} [3/3]
DEADLINE: <2019-01-11 ven.>
- [X] Introduire dans fifo.v
- [X] Transferer dans nnR.v
- [X] Compiler/git
* Les fichier de typos :Done:
** TODO Faire preuve LaTeX Lisible [3/3]
DEADLINE: <2019-01-11 ven.>
- [X] Ouvrir fichier Typo
- [X] Faire la preuve à la main
- [X] Valider
file:fifo.v::TODO-FIFO / ligne 758 /
* structuree algébriques (semi anneau, dioides)
** TODO Dioides [1/1]
- [X] Lemmas
file:dioide.v::TODO-DIOIDES
** TODO Dioide Complet [3/3]
- [X] add infinity
- [X] Sub additive closure
- [X] Deconvolution
** TODO Min-plus dioide [1/1]
- [X] Proof de Rmin(min,plus) dioide.
* Présentation JDD
- [X] Plan + Diapo
- [X] Répétition
* Résumé pour projet ANR
* Corriger Coercion Fup ?
Pourquoi elle doit etre écrite à chaque appel ?
* Theorem 11 p 137
- [X] Definition 35 p
- [X] proposition 7
- [X] proposition 31
* définitions serveur/service à mettre dans le bon ordre + ref (min-max-shaper)
* Revoir residual_server_cont avec retour de server
- [ ] Mettre a jour definition de min_plus_service
- [ ] Vérifier fonctionnement dans théorème fifo
* Papier
** Code : calcul des beta residuels (main + preuve)
** Plan pour papier
* Pull-request mathcomp
** DONE Clean up dioid (c.f. TODOs dans dioid.v et kleene.v)
** DONE Ecrite le big Comment début
** DONE Ouvrir la pull request
*** Lien (Ring ssralg.v) -- (semi-Ring dioid.v) ?
*** Expliciter la structure Treillis complet ?
* DONE Finir dflow
* Permuter UIB alt definition ?
* How about maximal arrival ?
- [] Change name (maximal arrival branch)
* Parallèle Gondran
* Take a look on comment of RT-proof
** File comment in parisRTProofs
- [] Bjorn
- [] Sophe
- [] Pierre
* Update coq 8.10
* Update perso : Canonical structure
: ajouter nnR et nnRbar dans la meme structure algébrique que Rbar ?
......@@ -7,10 +7,9 @@ if ([ "$version" == "8.4" ] || [ "$version" == "8.5" ]) then
else
echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
fi
find model implementation analysis util network_calculus -name "*.v" | grep -v "network_calculus/blind_multiplexing.v" >> _CoqProject
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
coq_makefile -f _CoqProject -o Makefile
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and
......
(* Loic Pottier, projet CROAP, INRIA Sophia Antipolis, April 1998. *)
(* Laurent Thry , INRIA Sophia Antipolis, April 2007 *)
(* Convert a dependencies file, in makefile form, into a graph in a file readable by dot.
The function dependtodot takes as input the dependencies file, and create a file with the same name suffixed by ".dot", readable by dot.
*)
let nodecol="#dbc3b6";; (* #add8ff *)
let edgecol="#676767";; (* #ff0000 *)
(* parameters to draw edges and nodes *)
let vnode x =
"l(\"" ^ x
^ "\",n(\"\",[a(\"COLOR\",\""^ nodecol ^"\"),a(\"OBJECT\",\"" ^ x ^ "\")],"
;;
let wstring x = "\""^x^"\""
;;
let vnoder x = "r(\"" ^ x ^ "\")"
;;
let vedge =
"e(\"\",[a(\"_DIR\",\"inverse\"),a(\"EDGEPATTERN\",\"solid\"),a(\"EDGECOLOR\",\"" ^ edgecol ^ "\")],"
;;
let listdv l = match l with
[] -> "[]"
|x::l -> let rec listdvr l = match l with
[] -> ""
|y::l -> "," ^ y ^ (listdvr l)
in "[" ^ x ^ (listdvr l) ^ "]"
;;
let rec visit ht hte x s =
Hashtbl.add ht x x;
try let le=Hashtbl.find hte x in
let rec visit_edge ls le =
match le with
[] -> ls
|b::l ->
try let _ =Hashtbl.find ht b in
(visit_edge (ls@[vedge ^ (vnoder b) ^ ")"]) l)
with Not_found ->
(visit_edge (ls@[vedge ^ (visit ht hte b s) ^ ")"]) l)
in s ^ (vnode x) ^ (listdv (visit_edge [] le)) ^ "))"
with Not_found -> s ^ (vnode x) ^ "[]))"
;;
(* cloture transitive *)
let rec merge_list a b = match a with
[] -> b
|x::a -> if (List.mem x b)
then (merge_list a b)
else x::(merge_list a b)
;;
let ht_graph g =
let ht =Hashtbl.create 50 in
let rec fill g = match g with
[] -> ()
|(a,lb)::g -> Hashtbl.add ht a lb; fill g
in fill g;
ht
;;
let trans_clos1 g =
let ht =ht_graph g in
List.map (fun (a,lb) ->
(a,(let l = ref lb in
let rec addlb lb = match lb with
[] -> ()
|b::lb -> (try l:=(merge_list (Hashtbl.find ht b) !l)
with Not_found -> ()); addlb lb
in addlb lb;
!l))) g
;;
let rec transitive_closure g =
let g1=trans_clos1 g in
if g1=g then g else (transitive_closure g1)
;;
(*
let g=["A",["B"];
"B",["C"];
"C",["D"];
"D",["E"];
"E",["A"]];;
transitive_closure g;;
*)
(* enlever les arcs de transitivite *)
let remove_trans g =
let ht = ht_graph (transitive_closure g) in
List.map (fun (a,lb) ->
(a,(let l=ref [] in
(let rec sel l2 = match l2 with
[] -> ()
|b::l2 -> (let r=ref false in
(let rec testlb l3 = match l3 with
[] -> ()
|c::l3 -> if (not (b=a)) &&(not(b=c)) && (not (a=c)) &&
(try (List.mem b (Hashtbl.find ht c))
with Not_found -> false)
then r:=true
else ();
testlb l3
in testlb lb);
if (!r=false)
then l:=b::!l
else ());
sel l2
in sel lb);
!l))) g
;;
(*
let g1=["Le", ["C";"Lt";"B"; "Plus"];
"Lt", ["A";"Plus"]];;
let g=["A",["B";"C";"D";"E"];
"B",["C"];
"C",["D"];
"D",["E"]];;
remove_trans g;;
*)
let dot g name file=
let chan_out = open_out (file^".dot") in
output_string chan_out "digraph ";
output_string chan_out name;
output_string chan_out " {\n";
output_string chan_out " bgcolor=transparent;\n";
output_string chan_out " splines=true;\n";
output_string chan_out " nodesep=1;\n";
output_string chan_out " node [fontsize=18, shape=rect, color=\"#dbc3b6\", style=filled];\n";
List.iter (fun (x,y) ->
output_string chan_out " ";
output_string chan_out (wstring x);
output_string chan_out " [URL=\"./";
output_string chan_out x;
output_string chan_out ".html\"]\n";
List.iter (fun y ->
output_string chan_out " ";
output_string chan_out (wstring x);
output_string chan_out " -> ";
output_string chan_out (wstring y);
output_string chan_out ";\n") y) g;
flush chan_out;
output_string chan_out "}";
close_out chan_out
;;
(*
example: a complete 5-graph,
let g=["A",["B";"C";"D";"E"];
"B",["A";"C";"D";"E"];
"C",["A";"B";"D";"E"];
"D",["A";"B";"C";"E"];
"E",["A";"B";"C";"D"]];;
daVinci g "g2";;
the file is then g2.daVinci
*)
(***********************************************************************)
open Genlex;;
(* change OP april 28 *)
(*
this parsing produce a pair where the first member is a paire (file,Directory)
and the second is a list of pairs (file,Directory).
from this we can compute the files graph dependency and also the directory graph dependency
*)
let lexer = make_lexer [":";".";"/";"-"];;
let rec parse_dep = parser
[< a=parse_name; 'Kwd ".";'Ident b; _=parse_until_colon;
_=parse_name ;'Kwd "."; 'Ident d;n=parse_rem >] -> (a,n)
and parse_rem = parser
[< a=parse_name;'Kwd ".";'Ident b;n=parse_rem >] -> a::n
| [<>]->[]
and parse_until_colon = parser
[< 'Kwd ":" >] -> ()
| [< 'Kwd _; _=parse_until_colon >] -> ()
| [< 'Int _; _=parse_until_colon >] -> ()
| [< 'Ident _; _=parse_until_colon >] -> ()
and parse_name = parser
[<'Kwd "/";a=parse_ident; b=parse_name_rem a "" >]-> ["." ^ a ^ b]
|[<a=parse_ident; b=parse_name_rem a "" >]-> [a ^ b]
and parse_name2 k = parser
[<d=parse_ident; b=parse_name_rem d k >]-> d ^ b
and parse_name_rem a b= parser
[<'Kwd "/";c=parse_name2 a >]-> "." ^ c
| [<>]->""
and parse_ident = parser
[<'Ident a; b=parse_ident_rem a "" >]-> a ^ b
|[<'Int a; b=parse_ident_rem (string_of_int a) "" >]-> (string_of_int a) ^ b
and parse_ident2 k = parser
[<'Ident d; b=parse_ident_rem d k >]-> d ^ b
|[<'Int d; b=parse_ident_rem (string_of_int d) k >]-> (string_of_int d) ^ b
and parse_ident_rem a b= parser
[<'Kwd "-";c=parse_ident2 a >]-> "-" ^ c
| [<>]-> ""
;;
(*
parse_name(lexer(Stream.of_string "u/sanglier/0/croap/pottier/Coq/Dist/contrib/Rocq/ALGEBRA/CATEGORY_THEORY/NT/YONEDA_LEMMA/NatFun.vo: "));;
parse_ident(lexer(Stream.of_string "ARITH-OMEGA-ggg-2.vo:"));; PROBLEME
*)
(* reads the depend file *)
let read_depend file=
let st =open_in file in
let lr =ref [] in
let rec other() =
(try
let d=parse_dep(lexer(Stream.of_string (input_line st))) in
lr:=d::(!lr);
other()
with _ ->[])
in (let _ = other() in ());
!lr;;
(* graph of a directory (given by a path) *)
let rec is_prefix p q = match p with
[] -> true
|a::p -> match q with [] -> false
|b::q -> if a=b then (is_prefix p q) else false
;;
let rec after_prefix p q = match p with
[] ->(match q with
[] -> "unknown"
|a::_ -> a)
|a::p -> match q with [] -> "unknown"
|b::q -> (after_prefix p q)
;;
let rec proj_graph p g = match g with
[] -> []
|(q,l)::g -> if (is_prefix p q)
then let rec proj_edges l = match l with
[] -> []
|r::l -> if (is_prefix p r)
then (after_prefix p r)::(proj_edges l)
else (proj_edges l)
in ((after_prefix p q),(proj_edges l))
::(proj_graph p g)
else (proj_graph p g)
;;
let rec start_path p = match p with
[] ->[]
|a::p -> match p with
[] ->[]
|b::q -> a::(start_path p)
;;
(* the list of all the paths and subpaths in g *)
let all_path g =
let ht =Hashtbl.create 50 in
let add_path p = Hashtbl.remove ht p;Hashtbl.add ht p true in
let rec add_subpath p = match p with
[] ->()
|_ -> add_path p; add_subpath (start_path p) in
let rec all_path g = match g with
[] -> ()
|(q,l)::g -> add_subpath (start_path q);
let rec all_pathl l = match l with
[] -> ()
|a::l -> add_subpath (start_path a);
all_pathl l
in all_pathl l;
all_path g
in all_path g;
let lp=ref [] in
Hashtbl.iter (fun x y -> lp:=x::!lp) ht;
!lp
;;
(*
let g=read_depend "depend";;
proj_graph ["theories"] g;;
*)
let rec endpath p = match p with
[] ->""
|a::p -> match p with
[] ->a
|_ -> endpath p
;;
let rec fpath p = match p with
[] ->""
|a::p -> a ^ "/" ^ (fpath p)
;;
let rec spath p = match p with
[] -> ""
|a::p -> match p with
[] ->a
|b::q -> a ^ "/" ^ (spath p)
;;
(* creates graphs for all paths *)
let dependtodot file=
let g =(read_depend file) in
let lp1 = all_path g in
let lp = (if lp1=[] then [[]] else lp1) in
let rec ddv lp = match lp with
[] -> ()
|p::lp -> let name = (let f = (endpath p) in
if f="" then file else f) in
let filep = file in
(* let filep = (let f = (spath p) in
* if f="" then file else f) in *)
dot (remove_trans (proj_graph p g))
name filep;
ddv lp
in ddv lp
;;
let _ =
if (Array.length Sys.argv) == 2 then
dependtodot Sys.argv.(1)
else print_string "makedot depend";
print_newline()
Require Import rt.model.time rt.model.arrival.basic.task_record.
Import Time. (* This Time module in time module seems useless *)
From mathcomp
Require Import ssreflect ssrnat ssrbool eqtype seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* Properties of different types of job: *)
Section Job.
(* A type for the identifiers of tasks *)
Variable T : eqType.
(* 1) Basic Job *)
Record validJob := ValidJob {
job_id :> T;
job_cost : time;
job_cost_positive : job_cost > 0
}.
(* 2) real-time job (with a deadline) *)
Record validRealTimeJob := ValidRealTimeJob {
rt_job :> validJob;
job_deadline : time;
job_deadline_positive : job_deadline > 0;
job_cost_le_deadline : job_cost rt_job <= job_deadline
}.
(* 3) Job of sporadic task *)
Record validSporadicTaskJob := ValidSporadicTaskJob {
task_job :> validRealTimeJob;
task : basicTask T;
_ : job_cost task_job <= task_cost task;
_ : job_deadline task_job = task_deadline task
}.
End Job.
Require Import rt.model.time.
Import Time. (* This Time module in time module seems useless *)
From mathcomp
Require Import ssreflect ssrnat ssrbool eqtype seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Task.
(* A type for the identifiers of tasks *)
Variable T : eqType.
(* A basicTask holds and id, a cost, a period and a deadline *)
Record basicTask := {
basicTask_id_cost_period_deadline : T * time * time * time;
_ : let: (_, cost, period, deadline) := basicTask_id_cost_period_deadline in
[&& cost > 0, period > 0, deadline > 0,
cost <= deadline & cost <= period]
}.
(* We have an eqType on basicTasks *)
Canonical basicTask_subType := [subType for basicTask_id_cost_period_deadline].
Definition basicTask_eqMixin := Eval hnf in [eqMixin of basicTask by <:].
Canonical basicTask_eqType := Eval hnf in EqType basicTask basicTask_eqMixin.
(* constructor *)
Program Definition BasicTask
(id : T)
(cost : time)
(period : time)
(deadline : time)
(cost_positive : cost > 0)
(period_positive : period > 0)
(deadline_positive : deadline > 0)
(cost_le_deadline : cost <= deadline)
(cost_le_period : cost <= period) :=
@Build_basicTask (id, cost, period, deadline) _.
Next Obligation.
rewrite cost_positive period_positive deadline_positive.
by rewrite cost_le_deadline cost_le_period.
Qed.
(* destructors *)
Coercion task_id (t : basicTask) : T :=
let: (id, _, _, _) := basicTask_id_cost_period_deadline t in id.
Definition task_cost (t : basicTask) : time :=
let: (_, c, _, _) := basicTask_id_cost_period_deadline t in c.
Definition task_period (t : basicTask) : time :=
let: (_, _, p, _) := basicTask_id_cost_period_deadline t in p.
Definition task_deadline (t : basicTask) : time :=
let: (_, _, _, d) := basicTask_id_cost_period_deadline t in d.
Lemma task_cost_positive (t : basicTask) : task_cost t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /=.
by move=> /and5P [].
Qed.
Lemma task_period_positive (t : basicTask) : task_period t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_period /=.
by move=> /and5P [].
Qed.
Lemma task_deadline_positive (t : basicTask) : task_deadline t > 0.
case t => [] [] [] [] id cost period deadline.
rewrite /task_deadline /=.
by move=> /and5P [].
Qed.
Lemma task_cost_le_deadline (t : basicTask) : task_cost t <= task_deadline t.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /task_deadline /=.
by move=> /and5P [].
Qed.
Lemma task_cost_le_period (t : basicTask) : task_cost t <= task_period t.
case t => [] [] [] [] id cost period deadline.
rewrite /task_cost /task_period /=.
by move=> /and5P [].
Qed.
(* A task set is defined as a sequence of tasks with no duplicates. *)
Record taskSet := TaskSet {
taskset :> seq basicTask;
_ : uniq [seq task_id t | t <- taskset]
}.
Variable ts : taskSet.
(* A task set can satisfy one of three deadline models:
implicit, constrained, or arbitrary. *)
Definition implicit_deadline_model :=
forall tsk,
tsk \in (taskset ts) -> task_deadline tsk = task_period tsk.
Definition constrained_deadline_model :=
forall tsk,
tsk \in (taskset ts) -> task_deadline tsk <= task_period tsk.
Definition arbitrary_deadline_model := True.
End Task.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence
rt.model.arrival.basic.task_arrival.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.
(* In this section, we define the notion of arrival curves, which
can be used to reason about the frequency of job arrivals. *)
Module ArrivalCurves.
Import ArrivalSequence TaskArrival.
Section DefiningArrivalCurves.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job -> Task.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and let tsk be any task to be analyzed. *)
Variable tsk: Task.
(* Recall the job arrivals of tsk in a given interval [t1, t2). *)
Let arrivals_of_tsk := arrivals_of_task_between job_task arr_seq tsk.
Let num_arrivals_of_tsk := num_arrivals_of_task job_task arr_seq tsk.
(* First, we define what constitutes an arrival bound for task tsk. *)
Section ArrivalBound.
(* Let max_arrivals denote any function that takes an interval length and
returns the associated number of job arrivals of tsk.
(This corresponds to the eta+ function in the literature.) *)
Variable max_arrivals: time -> nat.
(* Then, we say that num_arrivals is an arrival bound iff, for any interval [t1, t2),
(num_arrivals (t2 - t1)) bounds the number of jobs of tsk that arrive in that interval. *)
Definition is_arrival_bound :=
forall t1 t2,
t1 <= t2 ->
num_arrivals_of_tsk t1 t2 <= max_arrivals (t2 - t1).
End ArrivalBound.
(* Next, we define the notion of a separation bound for task tsk, i.e., the smallest
interval length in which a certain number of jobs of tsk can be spawned. *)
Section SeparationBound.
(* Let min_length denote any function that takes a number of jobs and
returns an associated interval length.
(This corresponds to the delta- function in the literature.) *)
Variable min_length: nat -> time.
(* Then, we say that min_length is a separation bound iff, for any number of jobs
of tsk, min_separation lower-bounds the minimum interval length in which that number
of jobs can be spawned. *)
Definition is_separation_bound :=
forall t1 t2,
t1 <= t2 ->
min_length (num_arrivals_of_tsk t1 t2) <= t2 - t1.
End SeparationBound.
End DefiningArrivalCurves.
End ArrivalCurves.
\ No newline at end of file
Require Import Coq.Logic.ConstructiveEpsilon.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.arrival.curves.bounds.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.
(* In this section, we show how to convert between arrival bounds and separation bounds. *)
Module ArrivalConversion.
Import ArrivalSequence ArrivalCurves.
(* For simplicity, we redefine some names. *)
Definition linear_search := constructive_indefinite_ground_description_nat.
(* Next, we show how to perform the conversion. *)
Section Conversion.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_task: Job -> Task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and let tsk be any task to be analyzed. *)
Variable tsk: Task.
(* First, we convert an arrival bound into a separation bound. *)
Section ArrivalToSeparation.
(* Let max_arrivals be any arrival bound of tsk. *)
Variable max_arrivals: time -> nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound job_task arr_seq tsk max_arrivals.
(* Assume that jobs of each task arrive infinitely often. *)
Hypothesis H_jobs_arrive_infinitely_often:
forall j1,
exists j2,
job_task j1 = job_task j2 /\
job_arrival j1 <= job_arrival j2.
(* Next, given any number of job arrivals, we show how to compute the minimum interval
length that can contain all these arrivals.
The computation is done using a linear search for larger values. *)
Section ComputingSeparationBound.
(* Consider any number of job arrivals. *)
Variable num_arrivals: time.
(* Then, we define a predicate that checks whether an interval delta is a separation
bound for this number of arrivals, ... *)
Definition contains_all_arrivals (delta: nat) :=
max_arrivals delta >= num_arrivals.
(* ...which we prove to be decidable (since it is a boolean). *)
Lemma contains_all_arrivals_decidable:
forall delta, {contains_all_arrivals delta} + {~ contains_all_arrivals delta}.
Proof.
by intros delta; apply Bool.bool_dec.
Qed.
(* Next, using the fact that jobs arrive infinitely often, we show that there always
exist an interval delta that contains this number of arrivals, ...*)
Lemma interval_exists:
exists delta, contains_all_arrivals delta.
Proof.
Admitted.
(* ...we run a linear search that looks for this delta. This returns
a value delta and a proof that delta contains all the arrivals. *)
Definition find_delta := linear_search contains_all_arrivals
contains_all_arrivals_decidable
interval_exists.
(* Next, we prove that this linear serch finds the minimum element that
satisfies the property.
(TODO: This proof is optional, just for tightness.
Also, it might require dealing with ConstructiveEpsilon). *)
Lemma find_delta_returns_min: true.
Admitted.
(* To conclude, we define the conversion from arrival bound to separation bound
as this number returned by the linear search. *)
Definition convert_to_separation_bound := proj1_sig find_delta.
End ComputingSeparationBound.
(* Based on the computation above, we prove that any value that is returned is indeed
a separation bound. *)
Lemma conversion_to_separation_bound_is_valid:
is_separation_bound job_task arr_seq tsk convert_to_separation_bound.
Proof.
intros t1 t2 LE.
Admitted.
End ArrivalToSeparation.
(* Next, we convert a separation bound into an arrival bound. *)
Section SeparationToArrival.
(* Let min_length be any separation bound of tsk. *)
Variable min_length: nat -> time.
Hypothesis H_is_separation_bound:
is_separation_bound job_task arr_seq tsk min_length.
(* Then, by computing xxxxxx, ...*)
Definition convert_to_arrival_bound (k: time) := 0. (* TODO: FIX *)
(* ...we transform min_length to obtain an arrival bound. *)
Lemma conversion_to_upper_curve_succeeds:
is_arrival_bound job_task arr_seq tsk convert_to_arrival_bound.
Proof.
Admitted.
End SeparationToArrival.
End Conversion.
End ArrivalConversion.
\ No newline at end of file
Require Import ssreflect.
From mathcomp
Require Import eqtype ssrnat ssrbool.
Require Import rt.model.time.
Import Time.
Require Import nnR.
Require Import Reals.
Require Import Coquelicot.Markov.
Local Open Scope R_scope.
(** time is nat, let's define real_time as non negative reals *)
Definition real_time := nnR.
(** ** Definitions of [clock] and reverse function [next_tick] *)
Record clock := {
(** A clock is just a function from clokc tick index (time := nat)
to a real time (real_time = R). *)
clock_tick_time :> time -> real_time;
(** First tick happens at time 0 *)
clock_0 : clock_tick_time O = 0%nnR;
clock_eps : posreal;
(** Clock ticks are separated enough in time (this hypothesis
prevents painful Zeno phenomena) *)
clock_incr : forall n, clock_tick_time n + clock_eps <= clock_tick_time n.+1
}.
Lemma clock_gt_n_eps (c : clock) :
forall n, INR n * clock_eps c <= c n.
Proof.
move=> n; elim: n => [|n IHn].
{ by rewrite Rmult_0_l; apply nnR_pos. }
rewrite S_INR.
rewrite Rmult_plus_distr_r Rmult_1_l.
apply (Rle_trans _ _ _ (Rplus_le_compat_r _ _ _ IHn)).
by case c.
Qed.
Lemma next_tick_ex (c : clock) (r : real_time) :
{ n | r <= c n /\ forall n', (n' < n)%nat -> c n' < r }.
Proof.
pose P := fun n => r <= c n.
have HP : forall n, P n \/ ~(P n).
{ by move=> n; rewrite /P; case (Rle_dec r (c n)) => H; [left|right]. }
move: (LPO_min P HP) => [[n [Hn Hn']]|Hn].
{ exists n; split => [//|n' Hn'n].
by apply /Rnot_le_lt /Hn' /ltP. }
exfalso.
pose z := up (r / clock_eps c).
move: (archimed (r / clock_eps c)); rewrite -/z => [] [].
have Pr_d_eps : 0 <= r / clock_eps c.
{ apply Rmult_le_pos; [by apply nnR_pos|].
by apply Rlt_le, Rinv_0_lt_compat; case (clock_eps c). }
case z => [|p|p]; move=> H _; move: H; apply Rle_not_gt.
{ by []. }
{ apply (Rmult_le_reg_r (clock_eps c)); [by case (clock_eps c)|].
rewrite Rmult_assoc Rinv_l; [|by apply Rgt_not_eq; case (clock_eps c)].
rewrite Rmult_1_r -positive_nat_Z -INR_IZR_INZ.
apply (Rle_trans _ _ _ (clock_gt_n_eps _ _)).
by apply (Rle_trans _ (c (Pos.to_nat p)));
[right|apply Rlt_le, Rnot_le_lt, Hn]. }
by apply (Rle_trans _ 0); [apply IZR_le|].
Qed.
(** Return the index of next tick after real time r (or exactly at time r). *)
Definition next_tick (c : clock) (r : real_time) : time :=
proj1_sig (next_tick_ex c r).
(** ** Some properties on clocks *)
Lemma next_tick_prop (c : clock) (t : real_time) :
t <= c (next_tick c t) /\ forall n, (n < next_tick c t)%nat -> c n < t.
Proof. by rewrite /next_tick; case next_tick_ex => /=. Qed.
Lemma non_decr_clock (c : clock) (x y : time) : (x <= y)%nat -> c x <= c y.
Proof.
elim: y => [|y IHy]; [by case x => [_|//]; right|].
rewrite leq_eqVlt ltnS => /orP [/eqP ->|Hx]; [by right|].
apply (Rle_trans _ _ _ (IHy Hx)).
move: (clock_incr c y); apply Rle_trans.
rewrite -{1}(Rplus_0_r (c y)); apply Rplus_le_compat_l, Rlt_le, cond_pos.
Qed.
Lemma non_decr_next_tick (c : clock) (t t' : real_time) :
t <= t' -> (next_tick c t <= next_tick c t')%nat.
Proof.
move=> Htt'; rewrite leqNgt; apply /negP => H; move: Htt'; apply Rlt_not_le.
move: (proj2 (next_tick_prop c t) _ H); apply Rle_lt_trans, next_tick_prop.
Qed.
Lemma next_tick_clock_tick (c : clock) (n : time) : next_tick c (c n) = n.
Proof.
rewrite /next_tick.
case (next_tick_ex _ _) => t [Ht Ht'] /=.
apply /anti_leq /andP; split.
{ by rewrite leqNgt; apply /negP => Hnt; move: (Ht' _ Hnt); apply Rlt_irrefl. }
rewrite leqNgt; apply /negP => Htn.
move: (non_decr_clock c _ _ Htn); apply Rlt_not_le, (Rle_lt_trans _ _ _ Ht).
move: (clock_incr c t); apply Rlt_le_trans.
rewrite -{1}(Rplus_0_r (c t)); apply Rplus_lt_compat_l, cond_pos.
Qed.
Lemma next_tick_0 (c : clock) : next_tick c 0%nnR = 0%N.
Proof. by rewrite -(clock_0 c) next_tick_clock_tick. Qed.
(** ** A few specific clocks *)
(** Periodic clocks are a simple example of clock *)
Program Definition periodic_clock (period : posreal) : clock :=
Build_clock (fun n => mk_nnR (INR n * period) _) _ period _.
Next Obligation.
by apply Rmult_le_pos; [apply pos_INR|apply Rlt_le; case period].
Qed.
Next Obligation.
by apply nnR_inj; rewrite /= Rmult_0_l.
Qed.
Next Obligation.
case n => [|n'].
{ by rewrite Rmult_0_l Rplus_0_l Rmult_1_l; right. }
by rewrite Rmult_plus_distr_r Rmult_1_l; right.
Qed.
This diff is collapsed.
######################################################################
## Case study of article: encoding into network calculus (using
## RTaW minplus interpreter format).
##
## Run in http://realtimeatwork.com/minplus-playground#
## Sizes: bits
## Time unit: ms
d0:= delay(0)
TenPow5:= 100000
###################################
## Input data flows
## Frame/Burst size: 1000 bytes = 8000 bits
## Throughput: 20Mb/s = 20Kb/ms
f1:= bucket(20000, 8000)
f2:= f1
f3:= f1
f4:= f1
f5:= f1
###################################
## First server : S1
## Throughput: 100Mb/s = 100Kb/ms
## Input: f1, f2, f3
capacity:= affine(TenPow5,0)
S1_input:= f1 + f2
S1_input:= S1_input + f3
S1_FIFO_delay:= hdev(S1_input, capacity)
S1_FIFO_delay
S1_FIFO_service:= delay( S1_FIFO_delay )
plot( S1_FIFO_service, S1_input, capacity, xlim=[0,1], ylim=[0,50000], main="Server S1: total input, capacity and delay")
f1_S1:= ( f1 / S1_FIFO_service )
f2_S1:= ( f2 / S1_FIFO_service )
f3_S1:= ( f3 / S1_FIFO_service )
###################################
## Second server : S2
## Made of 3 output ports called internally
## S2_f1, S2_f2, S2_f3
S2_f1_FIFO_delay:= hdev( f1_S1, capacity )
S2_f1_FIFO_service:= delay( S2_f1_FIFO_delay )
f1_S2:= ( f1_S1 / S2_f1_FIFO_service )
S2_f2_FIFO_delay:= hdev( f2_S1, capacity )
S2_f2_FIFO_service:= delay( S2_f2_FIFO_delay )
f2_S2:= ( f2_S1 / S2_f2_FIFO_service )
S2_f3_FIFO_delay:= hdev( f3_S1, capacity )
S2_f3_FIFO_service:= delay( S2_f3_FIFO_delay )
f3_S2:= ( f3_S1 / S2_f3_FIFO_service )
###################################
## Third server: S3
## Throughput: 100Mb/s = 100Kb/ms
## Input: f1, f4
S3_input:= f1_S2 + f4
S3_FIFO_delay:= hdev(S3_input, capacity)
S3_FIFO_service:= delay( S3_FIFO_delay )
plot( S3_FIFO_service, S3_input, capacity, xlim=[0,1], ylim=[0,50000], main="Server S3: total input, capacity and delay")
f1_S3:= ( f1_S2 / S3_FIFO_service )
f4_S3:= ( f4 / S3_FIFO_service )
###################################
## Fourth server: S4
## Throughput: 100Mb/s = 100Kb/ms
## Input: f3, f5
S4_input:= f3_S2 + f5
S4_FIFO_delay:= hdev(S4_input, capacity)
S4_FIFO_service:= delay( S4_FIFO_delay )
f3_S4:= ( f3_S2 / S4_FIFO_service )
f5_S4:= ( f5 / S4_FIFO_service )
###################################
## Fifth server/ first port: S5
## Throughput: 100Mb/s = 100Kb/ms
## Input: f1,f2,f3
S5_input:= f1_S3 + f2_S2
S5_input:= S5_input + f3_S4
S5_FIFO_delay:= hdev(S5_input, capacity)
S5_FIFO_service:= delay( S5_FIFO_delay )
###################################
## Fifth server/ second port: S6
## Throughput: 100Mb/s = 100Kb/ms
## Input: f4,f5
S6_input:= f4_S3 + f5_S4
S6_FIFO_delay:= hdev(S6_input, capacity)
S6_FIFO_service:= delay( S6_FIFO_delay )
###################################
## End-to-end delays
f1_E2E_service:= ( S1_FIFO_service * S3_FIFO_service ) * S5_FIFO_service
f1_E2E_service:= f1_E2E_service * S2_f1_FIFO_service
f1_E2E_delay:= hdev(f1, f1_E2E_service)
f1_E2E_delay
# 3612/3125 = 1.15584ms
f2_E2E_service:= S1_FIFO_service * S5_FIFO_service
f2_E2E_service:= f2_E2E_service * S2_f2_FIFO_service
f2_E2E_delay:= hdev(f2, f2_E2E_service)
f2_E2E_delay
# 2882/3125 = 0.92224 ms
f3_E2E_service:= ( S1_FIFO_service * S4_FIFO_service ) * S5_FIFO_service
f3_E2E_service:= f3_E2E_service * S2_f3_FIFO_service
f3_E2E_delay:= hdev(f3, f3_E2E_service)
f3_E2E_delay
# 3612/3125 = 1.15584ms
f4_E2E_service:= S3_FIFO_service * S6_FIFO_service
f4_E2E_delay:= hdev(f4, f4_E2E_service)
f4_E2E_delay
# 1522/3125 = 0.48704 ms
f5_E2E_service:= S4_FIFO_service * S6_FIFO_service
f5_E2E_delay:= hdev(f5, f5_E2E_service)
f5_E2E_delay
# 1522/3125 = 0.48704 ms
This diff is collapsed.
This diff is collapsed.
COQ_PROJ := _CoqProject
COQ_MAKEFILE := Makefile.coq
COQ_MAKE := +$(MAKE) -f $(COQ_MAKEFILE)
ifneq "$(COQBIN)" ""
COQBIN := $(COQBIN)/
else
COQBIN := $(dir $(shell which coqc))
endif
export COQBIN
all html gallinahtml deps.dot deps.png doc: $(COQ_MAKEFILE)
$(COQ_MAKE) $@
%.vo: %.v
$(COQ_MAKE) $@
clean:
-$(COQ_MAKE) clean
$(RM) $(COQ_MAKEFILE) $(COQ_MAKEFILE).conf *~ depend depend.dot depend.png depend.html makedot
$(COQ_MAKEFILE): $(COQ_PROJ)
$(COQBIN)coq_makefile -f $< -o $@
.PHONY: all install clean
Dependencies
============
- Coq (>= 8.5) : http://coq.inria.fr/
- Coquelicot (>= 2.1.1) : http://coquelicot.saclay.inria.fr/
The easiest way to install them is to use Opam :
% opam repo add coq-released https://coq.inria.fr/opam/released
% opam install coq coq-mathcomp-algebra coq-coquelicot
Compilation
===========
% make
Documentation
=============
% make doc # requires camlp4 (opam install camlp4)
Then look at html/toc.html with your favorite browser.
This diff is collapsed.
(**
This file is part of the CoqApprox formalization of rigorous
polynomial approximation in Coq:
http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and Inria.
This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
*)
(** * Define algebraic canonical structures from Ssreflect on R
(this enables in particular the use of the bigops (\sum, \prod)). *)
Require Import Rdefinitions Raxioms RIneq Rbasic_fun.
Require Import Epsilon FunctionalExtensionality.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
From mathcomp Require Import choice bigop ssralg.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope R_scope.
Definition eqr (r1 r2 : R) : bool :=
if Req_EM_T r1 r2 is left _ then true else false.
Lemma eqrP : Equality.axiom eqr.
Proof.
by move=> r1 r2; rewrite /eqr; case: Req_EM_T=> H; apply: (iffP idP).
Qed.
Canonical Structure real_eqMixin := EqMixin eqrP.
Canonical Structure real_eqType := Eval hnf in EqType R real_eqMixin.
Fact inhR : inhabited R.
Proof. exact: (inhabits 0). Qed.
Definition pickR (P : pred R) (n : nat) :=
let x := epsilon inhR P in if P x then Some x else None.
Fact pickR_some P n x : pickR P n = Some x -> P x.
Proof. by rewrite /pickR; case: (boolP (P _)) => // Px [<-]. Qed.
Fact pickR_ex (P : pred R) :
(exists x : R, P x) -> exists n, pickR P n.
Proof. by rewrite /pickR; move=> /(epsilon_spec inhR)->; exists 0%N. Qed.
Fact pickR_ext (P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.
Proof.
move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _.
suff->: u = v by rewrite PEQ.
by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ.
Qed.
Definition R_choiceMixin : choiceMixin R :=
Choice.Mixin pickR_some pickR_ex pickR_ext.
Canonical R_choiceType := Eval hnf in ChoiceType R R_choiceMixin.
Fact RplusA : associative (Rplus).
Proof. by move=> *; rewrite Rplus_assoc. Qed.
Definition real_zmodMixin := ZmodMixin RplusA Rplus_comm Rplus_0_l Rplus_opp_l.
Canonical Structure real_zmodType := Eval hnf in ZmodType R real_zmodMixin.
Fact RmultA : associative (Rmult).
Proof. by move=> *; rewrite Rmult_assoc. Qed.
Fact R1_neq_0 : R1 != R0.
Proof. by apply/eqP/R1_neq_R0. Qed.
Definition real_ringMixin := RingMixin RmultA Rmult_1_l Rmult_1_r
Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.
Canonical Structure real_ringType := Eval hnf in RingType R real_ringMixin.
Canonical Structure real_comringType := Eval hnf in ComRingType R Rmult_comm.
Import Monoid.
Canonical Radd_monoid := Law RplusA Rplus_0_l Rplus_0_r.
Canonical Radd_comoid := ComLaw Rplus_comm.
Canonical Rmul_monoid := Law RmultA Rmult_1_l Rmult_1_r.
Canonical Rmul_comoid := ComLaw Rmult_comm.
Canonical Rmul_mul_law := MulLaw Rmult_0_l Rmult_0_r.
Canonical Radd_add_law := AddLaw Rmult_plus_distr_r Rmult_plus_distr_l.
This diff is collapsed.
This diff is collapsed.
From mathcomp Require Import ssreflect ssrnat
eqtype finfun seq fintype bigop tuple ssrfun ssrbool.
Require Import Reals.
Require Import Coquelicot_complements nnR.
Require Import dioid kleene RminStruct.
Require Import network_calculus_definition interval_bounding fifo.
Require Import FunctionalExtensionality.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope dioid_scope.
Import GDioid.
Program Definition server_concat (S1 S2 : server) :=
@Build_server (fun A C => exists B, server_f S1 A B /\ server_f S2 B C) _.
Next Obligation.
move : H0 H1.
case S1 => S1' S1'_leq.
case S2 => S2' S2'_leq.
move => /= S1_f S2_f.
apply (Rle_trans _ _ _ (S2'_leq _ _ S2_f t) (S1'_leq _ _ S1_f t)).
Qed.
Lemma server_concatE (S1 S2 : server) A C :
server_concat S1 S2 A C <-> exists B, S1 A B /\ S2 B C.
Proof.
case S1 => S1' S1'_leq.
case S2 => S2' S2'_leq.
split.
{
rewrite /server_concat /=.
move => [A' [C' [HAA' [HCC' [B' [HAB' HBC']]]]]].
exists B'.
split.
{
exists A', B'.
by do 2 (split ; [by []|]).
}
exists B', C'.
by do 2 (split ; [by []|]).
}
move => [B [[A' [B' [HAA' [HBB' /= HAB']]]]]].
move => [B'' [C' [HBB'' [HCC' /= HBC']]]].
exists A', C'.
do 2 (split ; [by []|]).
exists B'.
split; [by []|].
rewrite -server_FplusE.
rewrite -(Fplus_inj HBB').
rewrite (Fplus_inj HBB'').
by rewrite server_FplusE.
Qed.
Notation "S1 * S2" := (server_concat S1 S2) : Server_scope.
Delimit Scope Server_scope with S.
Theorem server_concat_conv (S1 S2 : server) (beta1 beta2 : Fup) :
is_min_service S1 beta1 -> is_min_service S2 beta2 ->
is_min_service (S1 * S2)%S (beta1 * beta2).
Proof.
move => H1 H2 A D.
move => [A' [D' [HAA [HDD [B]]]]].
rewrite -!server_FplusE => [] [S1' S2'].
move : (H1 _ _ S1').
rewrite (Fplus_dflow HAA) => {H1} H1.
move : (H2 _ _ S2').
rewrite (Fplus_dflow HDD) => {H2} H2.
apply (led_trans H2).
rewrite muldA.
by apply led_mul2r.
Qed.
(* Loic Pottier, projet CROAP, INRIA Sophia Antipolis, April 1998. *)
(* Laurent Thry , INRIA Sophia Antipolis, April 2007 *)
(* Convert a dependencies file, in makefile form, into a graph in a file readable by dot.
The function dependtodot takes as input the dependencies file, and create a file with the same name suffixed by ".dot", readable by dot.
*)
let nodecol="#dbc3b6";; (* #add8ff *)
let edgecol="#676767";; (* #ff0000 *)
(* parameters to draw edges and nodes *)
let vnode x =
"l(\"" ^ x
^ "\",n(\"\",[a(\"COLOR\",\""^ nodecol ^"\"),a(\"OBJECT\",\"" ^ x ^ "\")],"
;;
let wstring x = "\""^x^"\""
;;
let vnoder x = "r(\"" ^ x ^ "\")"
;;
let vedge =
"e(\"\",[a(\"_DIR\",\"inverse\"),a(\"EDGEPATTERN\",\"solid\"),a(\"EDGECOLOR\",\"" ^ edgecol ^ "\")],"
;;