.ackrc

+# Configuration file for the 'ack' search utility
+# See https://beyondgrep.com/ for details.
+
+# Ignore misc files generated by the build process
+--ignore-file=ext:glob,aux,d,conf,orig
+--ignore-dir=html

.gitattributes

+*.v gitlab-language=coq

.gitignore

+*.d
+*.glob
+*.vo
+*.vos
+*.vok
+*.html
+/html
+*.aux
+Makefile.coq*
+Makefile.conf
+*.crashcoqide
+*.v#
+*.cache
+*~
+*.swp
+*.orig
+*/.#*
+#*#
+.#*
+*.DS_Store
+/proof-state
+/with-proof-state
+/html-alectryon
+_esy
+esy.lock/
+_CoqProject

.gitlab-ci.yml

+###################### 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
+
+###################### Rules and Scripts ##################
+
+.not_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
+
+.only_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH =~ /^wip-.*$/) && ($CI_PIPELINE_SOURCE != "merge_request_event")
+
+.build-common:
+  stage: build
+  script:
+    - 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
+
+.preferred-stable-version:
+    image: registry.mpi-sws.org/mathcomp-for-prosa:2.3.0-coq-8.20
+
+.build:
+  image: registry.mpi-sws.org/mathcomp-for-prosa:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-and-test-POET:
+  extends: .build
+  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
+    - make gallinahtml -j ${NJOBS}
+    - 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:
+      - "with-proofs/"
+      - "without-proofs/"
+      - "pretty/"
+    expire_in: 1 week
+
+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:
+    - make -j ${NJOBS}
+    - 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:
+      - "html-alectryon/"
+    expire_in: 1 week

.mailmap

+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>

BertognaResponseTimeEDFComp.v

-Require Import Vbase ScheduleDefs BertognaResponseTimeDefs divround helper
-               ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
-
-Module ResponseTimeIterationEDF.
-
-  Import Schedule ResponseTimeAnalysis.
-
-  Section Analysis.
-    
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_period: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    
-    Let task_with_response_time := (sporadic_task * nat)%type.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-
-    Variable num_cpus: nat.
-
-    (* Next we define the fixed-point iteration for computing
-       Bertogna's response-time bound for any task in ts. *)
-    
-    (*Computation of EDF on list of pairs (T,R)*)
-    
-    Let max_steps (ts: taskset_of sporadic_task) :=
-      \max_(tsk <- ts) task_deadline tsk.
-
-    Let response_time_bound (tsk: sporadic_task) (rt_bounds: seq task_with_response_time)
-                            (delta: time) :=
-      task_cost tsk +
-      div_floor
-       (total_interference_bound_jlfp task_cost task_period tsk rt_bounds delta)
-       num_cpus.
-    
-    Let initial_state (ts: taskset_of sporadic_task) :=
-      map (fun t => (t, task_cost t)) ts.
-    
-    Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
-      map (fun pair : task_with_response_time =>
-             let (tsk, R) := pair in
-               (tsk, response_time_bound tsk rt_bounds R))
-          rt_bounds.
-
-    Definition R_le_deadline (pair: task_with_response_time) :=
-      let (tsk, R) := pair in
-        R <= task_deadline tsk.
-    
-    Definition R_list_edf (ts: taskset_of sporadic_task) :=
-      let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
-        if (all R_le_deadline R_values) then
-          Some R_values
-        else None.
-    
-    (* The schedulability test simply checks if we got a list of
-       response-time bounds (i.e., if the computation did not fail). *)
-    Definition edf_schedulable (ts: taskset_of sporadic_task) :=
-      R_list_edf ts != None.
-    
-    Section AuxiliaryLemmas.
-
-    End AuxiliaryLemmas.
-    
-    Section Proof.
-
-      (* Consider a task set ts. *)
-      Variable ts: taskset_of sporadic_task.
-      
-      (* Assume the task set has no duplicates, ... *)
-      Hypothesis H_ts_is_a_set: uniq ts.
-
-      (* ...all tasks have valid parameters, ... *)
-      Hypothesis H_valid_task_parameters:
-        valid_sporadic_taskset task_cost task_period task_deadline ts.
-
-      (* ...restricted deadlines, ...*)
-      Hypothesis H_restricted_deadlines:
-        forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
-
-      (* ...and tasks are ordered by increasing priorities. *)
-      (*Hypothesis H_sorted_ts: sorted EDF ts.*)
-
-      (* Next, consider any arrival sequence such that...*)
-      Context {arr_seq: arrival_sequence Job}.
-
-     (* ...all jobs come from task set ts, ...*)
-      Hypothesis H_all_jobs_from_taskset:
-        forall (j: JobIn arr_seq), job_task j \in ts.
-      
-      (* ...they have valid parameters,...*)
-      Hypothesis H_valid_job_parameters:
-        forall (j: JobIn arr_seq),
-          valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
-      
-      (* ... and satisfy the sporadic task model.*)
-      Hypothesis H_sporadic_tasks:
-        sporadic_task_model task_period arr_seq job_task.
-      
-      (* Then, consider any platform with at least one CPU and unit
-         unit execution rate, where...*)
-      Variable rate: Job -> processor num_cpus -> nat.
-      Variable sched: schedule num_cpus arr_seq.
-      Hypothesis H_at_least_one_cpu :
-        num_cpus > 0.
-      Hypothesis H_rate_equals_one :
-        forall j cpu, rate j cpu = 1.
-
-      (* ...jobs only execute after they arrived and no longer
-         than their execution costs,... *)
-      Hypothesis H_jobs_must_arrive_to_execute:
-        jobs_must_arrive_to_execute sched.
-      Hypothesis H_completed_jobs_dont_execute:
-        completed_jobs_dont_execute job_cost rate sched.
-
-      (* ...and do not execute in parallel. *)
-      Hypothesis H_no_parallelism:
-        jobs_dont_execute_in_parallel sched.
-
-      (* Assume the platform satisfies the global scheduling invariant. *)
-      Hypothesis H_global_scheduling_invariant:
-        forall (tsk: sporadic_task) (j: JobIn arr_seq) (t: time),
-          tsk \in ts ->
-          job_task j = tsk ->
-          backlogged job_cost rate sched j t ->
-          count
-            (fun tsk_other : _ =>
-               is_interfering_task_jlfp tsk tsk_other &&
-               task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
-
-      Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
-        task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
-      Definition no_deadline_missed_by_job :=
-        job_misses_no_deadline job_cost job_deadline rate sched.
-
-      Section HelperLemma.
-        
-        (* The following lemma states that the response-time bounds
-           computed using R_list are valid. *)
-        Lemma R_list_has_response_time_bounds :
-          forall rt_bounds tsk R,
-            R_list_edf ts = Some rt_bounds ->
-            (tsk, R) \in rt_bounds ->
-            forall j : JobIn arr_seq,
-              job_task j = tsk ->
-              completed job_cost rate sched j (job_arrival j + R).
-        Proof.
-          rename H_valid_job_parameters into JOBPARAMS,
-                 H_valid_task_parameters into TASKPARAMS,
-                 H_restricted_deadlines into RESTR,
-                 H_completed_jobs_dont_execute into COMP,
-                 H_jobs_must_arrive_to_execute into MUSTARRIVE,
-                 H_global_scheduling_invariant into INVARIANT,
-                 (*H_transitive into TRANS,
-                 H_unique_priorities into UNIQ,
-                 H_total into TOTAL,*)
-                 H_all_jobs_from_taskset into ALLJOBS,
-                 H_ts_is_a_set into SET.
-          clear ALLJOBS.
-
-          intros rt_bounds tsk R SOME IN j JOBj.
-          unfold R_list_edf, edf_rta_iteration in *.
-          assert (FIXED: forall tsk R,
-                           (tsk, R) \in rt_bounds ->
-                           R = task_cost tsk + response_time_bound tsk rt_bounds R).
-          {
-            admit.
-          }
-          generalize dependent j.
-          generalize dependent R.
-          generalize dependent tsk.
-
-          cut ((forall tsk R, (tsk, R) \in rt_bounds -> R = task_cost tsk + response_time_bound tsk rt_bounds R) -> (forall tsk R (j: JobIn arr_seq), (tsk, R) \in rt_bounds -> job_task j = tsk -> completed job_cost rate sched j (job_arrival j + R))).
-          {
-            by intro ASSUMP; ins; apply ASSUMP with (tsk := tsk).
-          }
-          {
-            ins.
-            admit.
-          }
-
-          (*
-          ins. 
-          unfold edf_schedulable, R_list_edf in *.
-
-
-          ins. 
-          induction ts as [| ts' tsk_i IH] using last_ind.
-          {
-            intros rt_bounds tsk R SOME IN.
-            by inversion SOME; subst; rewrite in_nil in IN.
-          }
-          {
-           intros rt_bounds tsk R SOME IN j JOBj.
-             destruct (lastP rt_bounds) as [| hp_bounds (tsk_lst, R_lst)];
-              first by rewrite in_nil in IN.
-            rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
-            destruct IN as [LAST | BEGINNING]; last first.
-            {
-              apply IH with (rt_bounds := hp_bounds) (tsk := tsk); try (by ins).
-              by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
-              by ins; red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
-              by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
-              by apply sorted_rcons_prefix in SORT.
-              {
-                intros tsk0 j0 t IN0 JOB0 BACK0.
-                exploit (INVARIANT tsk0 j0 t); try (by ins);
-                  [by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
-                rewrite -cats1 count_cat /= in INV.
-                unfold is_interfering_task_fp in INV.
-                generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
-                assert (HP: higher_eq_priority tsk_lst tsk0 = false).
-                {
-                  apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
-                  apply negbTE; apply/negP; unfold not; intro BUG.
-                  exploit UNIQ; [by apply/andP; split; [by apply SORT | by ins] | intro EQ].
-                  by rewrite rcons_uniq -EQ IN0 in SET.
-                }              
-                by rewrite HP 2!andFb 2!addn0 in INV.
-              }
-              by apply R_list_rcons_prefix in SOME.
-            }
-            {
-              move: LAST => /eqP LAST.
-              inversion LAST as [[EQ1 EQ2]].
-              rewrite -> EQ1 in *; rewrite -> EQ2 in *; clear EQ1 EQ2 LAST.
-              generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
-              generalize SOME; apply R_list_rcons_prefix in SOME; intro SOME'.
-              have BOUND := bertogna_cirinei_response_time_bound_fp.
-              unfold is_response_time_bound_of_task, job_has_completed_by in BOUND.
-              apply BOUND with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst)
-                               (ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
-                               (higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
-              by apply R_list_unzip1 with (R := R_lst).
-              {
-                intros hp_tsk R0 HP j0 JOB0.
-                apply IH with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
-                by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
-                by red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
-                by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
-                by apply sorted_rcons_prefix in SORT.
-                {
-                  intros tsk0 j1 t IN0 JOB1 BACK0.
-                  exploit (INVARIANT tsk0 j1 t); try (by ins);
-                    [by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
-                  rewrite -cats1 count_cat /= addn0 in INV.
-                  unfold is_interfering_task_fp in INV.
-                  assert (NOINTERF: higher_eq_priority tsk_lst tsk0 = false).
-                  {
-                    apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
-                    apply negbTE; apply/negP; unfold not; intro BUG.
-                    exploit UNIQ; [by apply/andP; split; [by apply BUG | by ins] | intro EQ].
-                    by rewrite rcons_uniq EQ IN0 in SET.
-                  }
-                  by rewrite NOINTERF 2!andFb addn0 in INV.
-                }
-              }
-              by ins; apply R_list_ge_cost with (ts' := ts') (rt_bounds := hp_bounds).
-              by ins; apply R_list_le_deadline with (ts' := ts') (rt_bounds := hp_bounds).
-              {
-                ins; exploit (INVARIANT tsk_lst j0 t); try (by ins).
-                by rewrite mem_rcons in_cons; apply/orP; left.
-              }
-              {
-                rewrite [R_lst](R_list_rcons_response_time ts' hp_bounds tsk_lst); last by ins.
-                rewrite per_task_rta_fold.
-                apply per_task_rta_converges with (ts' := ts'); try (by ins).
-                {
-                  red; ins; apply TASKPARAMS.
-                  by rewrite mem_rcons in_cons; apply/orP; right.
-                }
-                apply R_list_le_deadline with (ts' := rcons ts' tsk_lst)
-                                            (rt_bounds := rcons hp_bounds (tsk_lst, R_lst));
-                  first by apply SOME'.
-                rewrite mem_rcons in_cons; apply/orP; left; apply/eqP.
-                f_equal; symmetry.
-                by apply R_list_rcons_response_time with (ts' := ts'). 
-              }
-            }
-          }*)
-        Qed.
-
-      End HelperLemma.
-      
-      (* If the schedulability test suceeds, ...*)
-      Hypothesis H_test_succeeds: edf_schedulable ts.
-      
-      (*..., then no task misses its deadline,... *)
-      Theorem taskset_schedulable_by_fp_rta :
-        forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
-      Proof.
-        unfold no_deadline_missed_by_task, task_misses_no_deadline,
-               job_misses_no_deadline, completed,
-               edf_schedulable,
-               valid_sporadic_job in *.
-        rename H_valid_job_parameters into JOBPARAMS,
-               H_valid_task_parameters into TASKPARAMS,
-               H_restricted_deadlines into RESTR,
-               H_completed_jobs_dont_execute into COMP,
-               H_jobs_must_arrive_to_execute into MUSTARRIVE,
-               H_global_scheduling_invariant into INVARIANT,
-               (*H_sorted_ts into SORT,
-               H_transitive into TRANS,
-               H_unique_priorities into UNIQ,
-               H_total into TOTAL,*)
-               H_all_jobs_from_taskset into ALLJOBS,
-               H_test_succeeds into TEST.
-
-        admit.
-        
-        (*move => tsk INtsk j /eqP JOBtsk.
-        have RLIST := (R_list_has_response_time_bounds).
-        have NONEMPTY := (R_list_non_empty ts).
-        have DL := (R_list_le_deadline ts).
-
-        destruct (R_list ts) as [rt_bounds |]; last by ins.
-        exploit (NONEMPTY rt_bounds tsk); [by ins | intros [EX _]; specialize (EX INtsk); des].
-        exploit (RLIST rt_bounds tsk R); [by ins | by ins | by apply JOBtsk | intro COMPLETED].
-        exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
-        
-        rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
-        apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
-        {
-          unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply service_monotonic; rewrite leq_add2l.
-          specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
-          by rewrite JOBtsk.
-        }
-        rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
-        by apply COMPLETED.*)
-      Qed.
-
-      (* ..., and the schedulability test yields safe response-time
-         bounds for each task. *)
-      Theorem fp_schedulability_test_yields_response_time_bounds :
-        forall tsk,
-          tsk \in ts ->
-          exists R,
-            R <= task_deadline tsk /\
-            forall (j: JobIn arr_seq),
-              job_task j = tsk ->
-              completed job_cost rate sched j (job_arrival j + R).
-      Proof.
-        intros tsk IN.
-        admit.
-      (*unfold edf_schedulable in *.
-        have TASKS := R_list_non_empty ts.
-        have BOUNDS := (R_list_has_response_time_bounds).
-        have DL := (R_list_le_deadline ts).
-        destruct (R_list ts) as [rt_bounds |]; last by ins.
-        exploit (TASKS rt_bounds tsk); [by ins | clear TASKS; intro EX].
-        destruct EX as [EX _]; specialize (EX IN); des.
-        exists R; split.
-          by apply DL with (rt_bounds0 := rt_bounds).
-          by ins; apply (BOUNDS rt_bounds tsk). *)
-      Qed.
-
-      (* For completeness, since all jobs of the arrival sequence
-         are spawned by the task set, we conclude that no job misses
-         its deadline. *)
-      Theorem jobs_schedulable_by_fp_rta :
-        forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
-      Proof.
-        intros j.
-        have SCHED := taskset_schedulable_by_fp_rta.
-        unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
-        apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
-        by apply H_all_jobs_from_taskset.
-      Qed.
-      
-    End Proof.
-
-  End Analysis.
-
-End ResponseTimeIterationEDF.
\ No newline at end of file

ExtraRelations.v

-(******************************************************************************)
-(* c11comp: Coq development attached to the paper                             *)
-(*                                                                            *)
-(*  Vafeiadis, Balabonski, Chakraborty, Morisset, and Zappa Nardelli.         *)
-(*  Common compiler optimisations are invalid in the C11 memory model         *)
-(*  and what we can do about it.                                              *)
-(*  In POPL 2015.                                                             *)
-(*                                                                            *)
-(* Copyright (c) MPI-SWS and INRIA                                            *)
-(* Released under a BSD-style license. See README.txt for details.            *)
-(******************************************************************************)
-
-(******************************************************************************)
-(** * Basic properties of relations *)
-(******************************************************************************)
-
-Require Import Vbase List Relations Classical. 
-Set Implicit Arguments.
-
-(** Definitions of relations *)
-(******************************************************************************)
-
-Definition immediate X (rel : relation X) (a b: X) :=
-  rel a b /\ (forall c (R1: rel a c) (R2: rel c b), False).
-
-Definition irreflexive X (rel : relation X) := forall x, rel x x -> False.
-
-Definition asymmetric X (rel : relation X) := forall x y, rel x y /\ rel y x -> False.
-
-Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).
-
-Definition is_total X (cond: X -> Prop) (rel: relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (NEQ: a <> b),
-    rel a b \/ rel b a.
-
-Definition restr_subset X (cond: X -> Prop) (rel rel': relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (REL: rel a b),
-    rel' a b.
-
-Definition restr_rel X (cond : X -> Prop) (rel : relation X) : relation X :=
-  fun a b => rel a b /\ cond a /\ cond b.
-
-Definition restr_eq_rel A B (f : A -> B) rel x y :=
-  rel x y /\ f x = f y.
-
-Definition upward_closed (X: Type) (rel: relation X) (P: X -> Prop) :=
-  forall x y (REL: rel x y) (POST: P y), P x.
-
-Definition max_elt (X: Type) (rel: relation X) (a: X) :=
-  forall b (REL: rel a b), False.
-
-Notation "r 'UNION1' ( a , b )" := 
-  (fun x y => x = a /\ y = b \/ r x y) (at level 100). 
-
-Notation "a <--> b" := (same_relation _ a b)  (at level 110).
-
-
-(** Very basic properties of relations *)
-(******************************************************************************)
-
-
-Lemma clos_trans_mon A (r r' : relation A) a b :
-  clos_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_trans.
-Qed.
-
-Lemma clos_refl_trans_mon A (r r' : relation A) a b :
-  clos_refl_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_refl_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_refl_trans.
-Qed.
-
-
-Lemma clos_refl_transE A r a b :
-  clos_refl_trans A r a b <-> a = b \/ clos_trans A r a b.
-Proof.
-  split; ins; desf; vauto; induction H; desf; vauto. 
-Qed.
-
-Lemma clos_trans_in_rt A r a b :
-  clos_trans A r a b -> clos_refl_trans A r a b.
-Proof.
-  induction 1; vauto. 
-Qed.
-
-Lemma rt_t_trans A r a b c :
-  clos_refl_trans A r a b -> clos_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H; eauto using clos_trans. 
-Qed.
-
-Lemma t_rt_trans A r a b c :
-  clos_trans A r a b -> clos_refl_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H0; eauto using clos_trans. 
-Qed.
-
-
-Lemma t_step_rt A R x y : 
-  clos_trans A R x y <-> exists z, R x z /\ clos_refl_trans A R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_tn1 in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma t_rt_step A R x y : 
-  clos_trans A R x y <-> exists z, clos_refl_trans A R x z /\ R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_t1n in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma clos_trans_of_transitive A R (T: transitive A R) x y : 
-  clos_trans A R x y -> R x y.
-Proof.
-  induction 1; eauto.
-Qed.
-
-Lemma clos_trans_eq :
-  forall X (rel: relation X) Y (f : X -> Y) 
-         (H: forall a b (SB: rel a b), f a = f b) a b
-         (C: clos_trans _ rel a b),
-    f a = f b.
-Proof.
-  ins; induction C; eauto; congruence.
-Qed.
-
-Lemma trans_irr_acyclic : 
-  forall A R, irreflexive R -> transitive A R -> acyclic R.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_of_transitive. 
-Qed.
-
-Lemma restr_rel_trans :
-  forall X dom rel, transitive X rel -> transitive X (restr_rel dom rel).
-Proof.
-  unfold restr_rel; red; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_of_clos_trans1 :
-  forall X rel1 rel2 x y,
-    clos_trans X (fun a b => clos_trans _ rel1 a b \/ rel2 a b) x y <->
-    clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y.
-Proof.
-  split; induction 1; desf; 
-  eauto using clos_trans, clos_trans_mon.
-Qed.
-
-Lemma upward_clos_trans:
-  forall X (rel: X -> X -> Prop) P,
-    upward_closed rel P -> upward_closed (clos_trans _ rel) P.
-Proof.
-  ins; induction 1; by eauto.
-Qed.
-
-Lemma max_elt_clos_trans:
-  forall X rel a b
-         (hmax: max_elt rel a)
-         (hclos: clos_trans X rel a b),
-    False.
-Proof.
-  ins. eapply clos_trans_t1n in hclos. induction hclos; eauto.
-Qed.
-
-Lemma is_total_restr :
-  forall X (dom : X -> Prop) rel,
-    is_total dom rel ->
-    is_total dom (restr_rel dom rel).
-Proof.
-  red; ins; eapply H in NEQ; eauto; desf; vauto.
-Qed.
-
-Lemma clos_trans_restrD :
-  forall X rel f x y, clos_trans X (restr_rel f rel) x y -> f x /\ f y.
-Proof.
-  unfold restr_rel; induction 1; ins; desf. 
-Qed.
-
-Lemma clos_trans_restr_eqD :
-  forall A rel B (f: A -> B) x y, clos_trans _ (restr_eq_rel f rel) x y -> f x = f y.
-Proof.
-  unfold restr_eq_rel; induction 1; ins; desf; congruence. 
-Qed.
-
-Lemma irreflexive_inclusion:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  irreflexive R2 ->
-  irreflexive R1.
-Proof.
-  unfold irreflexive, inclusion.
-  by eauto.
-Qed.
-
-Lemma clos_trans_inclusion:
-  forall X (R: relation X),
-  inclusion X R (clos_trans X R).
-Proof.
-  unfold inclusion. intros.
-  by econstructor; eauto.
-Qed.
-
-Lemma clos_trans_inclusion_clos_refl_trans:
-  forall X (R: relation X),
-  inclusion X (clos_trans X R) (clos_refl_trans X R).
-Proof.
-  unfold inclusion. intros.
-  induction H.
-    by eauto using rt_step.
-    by eauto using rt_trans.
-Qed.
-
-Lemma clos_trans_monotonic:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  inclusion X (clos_trans X R1) (clos_trans X R2).
-Proof.
-  intros.
-  intros x y hR1.
-  eapply clos_t1n_trans.
-  eapply clos_trans_t1n in hR1.
-  induction hR1.
-    by eauto using clos_t1n_trans, t1n_step.
-    (* [t1n_trans] is masked by a notation for [clos_t1n_trans] *)
-    by eauto using clos_t1n_trans, Relation_Operators.t1n_trans.
-Qed.
-
-(******************************************************************************)
-(** Set up setoid rewriting *)
-(******************************************************************************)
-
-Require Import Setoid.
-
-Lemma same_relation_refl: forall A, reflexive _ (same_relation A).
-Proof. split; ins. Qed.
-
-Lemma same_relation_sym: forall A, symmetric _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf. Qed.
-
-Lemma same_relation_trans: forall A, transitive _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf; red; eauto. Qed.
-
-Add Parametric Relation (X : Type) : (relation X) (same_relation X) 
- reflexivity proved by (@same_relation_refl X)
- symmetry proved by (@same_relation_sym X)
- transitivity proved by (@same_relation_trans X)
- as same_rel.
-
-Add Parametric Morphism X : (@union X) with 
-  signature (@same_relation X) ==> (@same_relation X) ==> (@same_relation X) as union_mor.
-Proof.
-  unfold same_relation, union; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X P : (@restr_rel X P) with 
-  signature (@same_relation X) ==> (@same_relation X) as restr_rel_mor.
-Proof.
-  unfold same_relation, restr_rel; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X : (@clos_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@clos_refl_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_relf_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@irreflexive X) with 
-  signature (@same_relation X) ==> iff as irreflexive_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@acyclic X) with 
-  signature (@same_relation X) ==> iff as acyclic_mor.
-Proof.
-  unfold acyclic; ins; rewrite H; reflexivity.
-Qed.
-
-
-Lemma same_relation_restr X (f : X -> Prop) rel rel' :
-   (forall x (CONDx: f x) y (CONDy: f y), rel x y <-> rel' x y) ->
-   (restr_rel f rel <--> restr_rel f rel').
-Proof.
-  unfold restr_rel; split; red; ins; desf; rewrite H in *; eauto.
-Qed.
-
-Lemma union_restr X f rel rel' :
-  union X (restr_rel f rel) (restr_rel f rel')
-  <--> restr_rel f (union _ rel rel').
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_restr X f rel (UC: upward_closed rel f) :
-  clos_trans X (restr_rel f rel) 
-  <--> restr_rel f (clos_trans _ rel).
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-    split; [|by apply clos_trans_restrD in H].
-    by eapply clos_trans_mon; eauto; unfold restr_rel; ins; desf.
-  clear H0; apply clos_trans_tn1 in H.
-  induction H; eauto 10 using clos_trans.
-Qed.
-
-
-(******************************************************************************)
-(** ** Lemmas about cycles *)
-(******************************************************************************)
-
-Lemma path_decomp_u1 X (rel : relation X) a b c d : 
-  clos_trans X (rel UNION1 (a, b)) c d ->
-  clos_trans X rel c d \/ 
-  clos_refl_trans X rel c a /\ clos_refl_trans X rel b d.
-Proof.
-  induction 1; desf; eauto using clos_trans, clos_refl_trans, clos_trans_in_rt.
-Qed.
-
-Lemma cycle_decomp_u1 X (rel : relation X) a b c : 
-  clos_trans X (rel UNION1 (a, b)) c c ->
-  clos_trans X rel c c \/ clos_refl_trans X rel b a.
-Proof.
-  ins; apply path_decomp_u1 in H; desf; eauto using clos_refl_trans.
-Qed.
-
-Lemma path_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x y
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y),
-    clos_trans X rel1 x y \/
-    (exists m n, 
-      clos_refl_trans X rel1 x m /\ clos_trans X rel2 m n /\ clos_refl_trans X rel1 n y) \/
-    (exists m n, 
-      clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; induction C; desf; eauto 8 using rt_refl, clos_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-
-  destruct (classic (m = n0)) as [|NEQ]; desf.
-  by right; left; exists m0, n; eauto using t_trans, rt_trans.
-  eapply T in NEQ; desf.
-    by right; right; exists n0, m; eauto 8 using clos_trans, rt_trans.
-    by right; left; exists m0, n; eauto 8 using clos_trans, rt_trans.
-    by apply t_step_rt in IHC0; desf; eapply D in IHC0; desf.
-    by apply t_rt_step in IHC4; desf; eapply D in IHC6; desf.
-Qed.
-
-Lemma cycle_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x x),
-    clos_trans X rel1 x x \/
-    (exists m n, clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; exploit path_decomp_u_total; eauto; ins; desf; eauto 8 using rt_trans.
-Qed.
-
-Lemma clos_trans_disj_rel :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (R: clos_trans _ rel x y) z
-    (R': clos_trans _ rel' y z),
-    False.
-Proof.
-  ins; induction R; eauto; induction R'; eauto.
-Qed.
-
-Lemma path_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (T: clos_trans X (union X rel rel') x y),
-    clos_trans _ rel x y \/ clos_trans _ rel' x y
-    \/ exists z, clos_trans _ rel' x z /\ clos_trans _ rel z y.
-Proof.
-  unfold union; ins.
- induction T; desf; eauto 6 using clos_trans;
-   try by exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x
-    (T: clos_trans X (union X rel rel') x x),
-    clos_trans _ rel x x \/ clos_trans _ rel' x x. 
-Proof.
-  ins; exploit path_decomp_u_1; eauto; ins; desf; eauto.
-  exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_disj :
-  forall X (rel : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel y z), False) x
-    (T: clos_trans X rel x x), False.
-Proof.
-  ins; inv T; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma clos_trans_restr_trans_mid : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    z (B : rel y z) w
-    (C : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) z w),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x w.
-Proof.
-  ins; eapply t_trans, t_trans; vauto.
-  eapply t_step; repeat split; eauto.
-    by apply clos_trans_restrD in A; desc.
-  by apply clos_trans_restrD in C; desc.
-Qed.
-
-Lemma clos_trans_restr_trans_cycle : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    (B : rel y x),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x x.
-Proof.
-  ins; eapply t_trans, t_step; eauto. 
-  by red; apply clos_trans_restrD in A; desf; auto.
-Qed.
-
-
-Lemma restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B) x y
-         (R: forall x y, rel' x y -> f x = f y),
-   restr_eq_rel f (fun x y => rel x y \/ rel' x y) x y <->
-   restr_eq_rel f rel x y \/ rel' x y.
-Proof.
-  unfold restr_eq_rel; ins; intuition.
-Qed.
-
-Lemma clos_trans_restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B)
-         (R: forall x y, rel' x y -> f x = f y),
-   clos_trans _ (restr_eq_rel f (fun x y => rel x y \/ rel' x y)) <-->
-   clos_trans _ (fun x y => restr_eq_rel f rel x y \/ rel' x y).
-Proof.
-  split; red; ins; eapply clos_trans_mon; eauto; ins; instantiate;
-  rewrite restr_eq_union in *; eauto.
-Qed.
-
-Lemma acyclic_mon X (rel rel' : relation X) :
-  acyclic rel -> inclusion _ rel' rel -> acyclic rel'.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_mon.
-Qed. 
-
-(** Extension of a partial order to a total order *)
-
-Section one_extension.
-
-  Variable X : Type.
-  Variable elem : X.
-  Variable rel : relation X.
-
-  Definition one_ext : relation X := 
-    fun x y =>
-      clos_trans _ rel x y 
-      \/ clos_refl_trans _ rel x elem /\ ~ clos_refl_trans _ rel y elem.
-
-  Lemma one_ext_extends x y : rel x y -> one_ext x y. 
-  Proof. vauto. Qed.
-
-  Lemma one_ext_trans : transitive _ one_ext.
-  Proof. 
-    red; ins; unfold one_ext in *; desf; desf; 
-      intuition eauto using clos_trans_in_rt, t_trans, rt_trans.
-  Qed.
- 
-  Lemma one_ext_irr : acyclic rel -> irreflexive one_ext.
-  Proof.
-    red; ins; unfold one_ext in *; desf; eauto using clos_trans_in_rt.
-  Qed.
-
-  Lemma one_ext_total_elem : 
-    forall x, x <> elem -> one_ext elem x \/ one_ext x elem.
-  Proof.
-    unfold one_ext; ins; rewrite !clos_refl_transE; tauto.
-  Qed.
-
-End one_extension.
-
-Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
-  match dom with 
-    | nil => clos_trans _ rel
-    | x::l => one_ext x (tot_ext l rel) 
-  end.
-
-Lemma tot_ext_extends : 
-  forall X dom (rel : relation X) x y, rel x y -> tot_ext dom rel x y. 
-Proof. 
-  induction dom; ins; eauto using t_step, one_ext_extends.
-Qed.
-
-Lemma tot_ext_trans : forall X dom rel, transitive X (tot_ext dom rel).
-Proof. 
-  induction dom; ins; vauto; apply one_ext_trans. 
-Qed.
-
-Lemma tot_ext_irr : 
-  forall X (dom : list X) rel, acyclic rel -> irreflexive (tot_ext dom rel).
-Proof.
-  induction dom; ins.
-  apply one_ext_irr, trans_irr_acyclic; eauto using tot_ext_trans.
-Qed.
-
-(*Lemma tot_ext_total : 
-  forall X (dom : list X) rel, is_total (fun x => In x dom) (tot_ext dom rel).
-Proof.
-  induction dom; red; ins; desf.
-  eapply one_ext_total_elem in NEQ; desf; eauto.
-  eapply nesym, one_ext_total_elem in NEQ; desf; eauto.
-  eapply IHdom in NEQ; desf; eauto using one_ext_extends.
-Qed.*)
-
-Lemma tot_ext_inv :
-  forall X dom rel (x y : X),
-    acyclic rel -> tot_ext dom rel x y -> ~ rel y x.
-Proof.
-  red; ins; eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; eauto.
-Qed.
-
-
-(** Misc properties *)
-(******************************************************************************)
-
-
-Lemma clos_trans_imm :
-  forall X (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L (ND: NoDup L) a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  intros until 3; induction ND; ins; vauto.
-  destruct (classic (R a x /\ R x b)) as [|N]; desf;
-    [apply t_trans with x|]; eapply IHND; ins;
-    exploit (D c); eauto; intro; desf; exfalso; eauto.
-Qed.
-
-
-(** Remove duplicate list elements (classical) *)
-(******************************************************************************)
-
-Require Import extralib.
-
-Fixpoint undup A dec (l: list A) :=
-  match l with nil => nil
-    | x :: l =>
-      if In_dec dec x l then undup dec l else x :: undup dec l
-  end.
-
-Lemma In_undup X dec (x: X) l : In x (undup dec l) <-> In x l.
-Proof.
-  induction l; ins; des_if; ins; rewrite IHl; split; ins; desf; vauto.
-Qed.
-
-Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).
-Proof.
-  induction l; ins; desf; constructor; eauto; rewrite In_undup; eauto. 
-Qed.
-
-
-Lemma clos_trans_imm2 :
-  forall X (dec : forall x y : X, {x = y} + {x <> y}) 
-         (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  ins; eapply clos_trans_imm with (L := undup dec L); ins;
-  try rewrite In_undup; eauto using NoDup_undup.
-Qed.
-
-
-
-
-Lemma total_immediate_unique:
-  forall X (eq_X_dec: forall (x y: X), {x=y} + {x<>y}) (rel: X -> X -> Prop) (P: X -> Prop)
-         (Tot: is_total P rel)
-         a b c (pa: P a) (pb: P b) (pc: P c)
-         (iac: immediate rel a c)
-         (ibc: immediate rel b c),
-    a = b.
-Proof.
-  ins.
-  destruct (eq_X_dec a b); eauto.
-  exfalso.
-  unfold immediate in *; desf.
-  eapply Tot in n; eauto.
-  desf; eauto.
-Qed.
-

JobDefs.v

-Require Import TaskDefs helper ssrnat ssrbool eqtype.  
-
-Module Job.
-
-  Section ValidJob.
-
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-
-    Variable j: Job.
-
-    Definition job_cost_positive (j: Job) := job_cost j > 0.
-
-  End ValidJob.
-
-  Section ValidRealtimeJob.
-
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    
-    Variable j: Job.
-
-    Definition job_cost_le_deadline := job_cost j <= job_deadline j.
-    Definition job_deadline_positive := job_deadline j > 0.
-        
-    Definition valid_realtime_job :=
-      job_cost_positive job_cost j /\
-      job_cost_le_deadline /\
-      job_deadline_positive.
-
-  End ValidRealtimeJob.
-
-  Section ValidSporadicTaskJob.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-    
-    Variable j: Job.
-
-    Definition job_cost_le_task_cost :=
-      job_cost j <= task_cost (job_task j).
-    Definition job_deadline_eq_task_deadline :=
-      job_deadline j = task_deadline (job_task j).
-
-    Definition valid_sporadic_job :=
-      valid_realtime_job job_cost job_deadline j /\
-      job_cost_le_task_cost /\
-      job_deadline_eq_task_deadline.
-
-  End ValidSporadicTaskJob.
-
-  Section ValidSporadicTaskJobWithJitter.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    Variable task_jitter: sporadic_task -> nat.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-    Variable job_jitter: Job -> nat.
-    
-    Variable j: Job.
-
-    Definition job_jitter_leq_task_jitter :=
-      job_jitter j <= task_jitter (job_task j).
-
-    Let j_is_valid_job :=
-      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
-
-    Definition valid_sporadic_job_with_jitter :=
-      j_is_valid_job /\ job_jitter_leq_task_jitter.
-
-  End ValidSporadicTaskJobWithJitter.
-
-End Job.
\ No newline at end of file

LICENSE

+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.coq.local

+# 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

PlatformDefs.v

-Require Import Vbase ScheduleDefs JobDefs PriorityDefs TaskArrivalDefs
-               ssreflect ssrbool eqtype ssrnat seq.
-
-(*Module Platform.
-
-Import Schedule.
-
-(* A processor platform is simply a set of schedules, \ie.,
-   it specifies the amount of service that jobs receive over time. *)
-Definition processor_platform := schedule_mapping -> Prop.
-
-(* For a processor platform to be valid, it must be able to schedule
-   any possible job arrival sequence. In particular, the constraints
-   of the platform should not be trivially false. *)
-(*Definition valid_platform (plat: processor_platform) :=
-  exists (sched: schedule), plat sched.*)
-
-(* Whether a job receives at most 1 unit of service *)
-Definition max_service_one (sched: schedule) := forall j t, service_at sched j t <= 1.
-
-End Platform.
-
-Module IdenticalMultiprocessor.
-
-Import Job ScheduleOfSporadicTask Platform Priority SporadicTaskArrival.
-
-Section Multiprocessor.
-
-Variable num_cpus: nat.
-Variable higher_eq_priority: jldp_policy.
-Variable sched: schedule.
-
-(* There is at least one processor. *)
-Definition mp_cpus_nonzero := num_cpus > 0.
-
-(* At any time,
-     (a) processors never stay idle when there are pending jobs (work conservation), and,
-     (b) the number of scheduled jobs does not exceed the number of processors. *)
-Definition mp_work_conserving :=
-  forall t, num_scheduled_jobs sched t = minn (num_pending_jobs sched t) num_cpus.
-
-(* If a job is backlogged, then either:
-     (a) there exists an earlier pending job of the same task
-     (b) all processor are busy with (other) jobs with higher or equal priority. *)
-Definition mp_scheduling_invariant :=
-  forall jlow t (ARRIVED: jlow \in prev_arrivals sched t)
-         (BACK: backlogged sched jlow t),
-    exists_earlier_job sched t jlow \/
-    num_interfering_jobs higher_eq_priority sched t jlow = num_cpus.
-
-Definition identical_multiprocessor :=
-  mp_cpus_nonzero /\ mp_scheduling_invariant /\ mp_work_conserving.
-
-End Multiprocessor.
-
-Section Uniprocessor.
-
-(* Uniprocessor is a special case of a multiprocessor *)
-Definition uniprocessor := identical_multiprocessor 1.
-
-End Uniprocessor.
-
-(*Lemma identmp_valid :
-  forall num_cpus higher_eq_priority,
-    valid_platform (identical_multiprocessor num_cpus higher_eq_priority).
-Proof.
-  unfold valid_platform, identical_multiprocessor, mp_cpus_nonzero,
-  mp_scheduling_invariant; ins.
-Qed.*)
-
-End IdenticalMultiprocessor. *)
\ No newline at end of file