.gitlab-ci.yml

@@ -2,16 +2,32 @@ stages:
   - build
   - process
 
-.build:
+.build-common:
   stage: build
+  script:
+    - opam update -y
+    - opam remove -y coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable  # Check coq-mathcomp-ssreflect is enough
+    - opam pin add -n -y -k path coq-prosa .
+    - opam install -y -v -j ${NJOBS} coq-prosa
+
+.build:
   image: mathcomp/mathcomp:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-dev:
+  image: mathcomp/mathcomp-dev:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-for-process:
+  stage: build
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
   script:
     - ./create_makefile.sh --without-classic
     - make -j ${NJOBS}
 
-.build-classic:
+.build-for-process-classic:
   stage: build
-  image: mathcomp/mathcomp:1.9.0-coq-8.10
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
   script:
     - ./create_makefile.sh --only-classic
     - make -j ${NJOBS}
@@ -44,14 +60,32 @@ stages:
     - "*/*/*/*/*/*/*/*/*/*.glob"
     expire_in: 1 week
 
+1.9.0-coq-8.9:
+  extends: .build
+
 1.9.0-coq-8.10:
+  extends: .build
+
+1.9.0-coq-8.11:
+  extends: .build
+
+1.10.0-coq-8.9:
+  extends: .build
+
+1.10.0-coq-8.10:
+  extends: .build
+
+1.10.0-coq-8.11:
+  extends: .build
+
+build-for-process:
   extends:
-    - .build
+    - .build-for-process
     - .collect-vo-files
 
-1.9.0-coq-8.10-classic:
+build-for-process-classic:
   extends:
-    - .build-classic
+    - .build-for-process-classic
     - .collect-vo-files
 
 proof-length:
@@ -66,40 +100,37 @@ spell-check:
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 
-1.9.0-coq-8.9:
-  extends: .build
-
-1.10.0-coq-dev:
+coq-8.10:
   extends:
-    - .build
-  # it's ok to fail with an unreleased version of Coq
+    - .build-dev
+  # it's ok to fail with an unreleased version of ssreflect
   allow_failure: true
 
-latest-coq-8.10:
+coq-dev:
   extends:
-    - .build
-  # it's ok to fail with an unreleased version of ssreflect
+    - .build-dev
+  # it's ok to fail with an unreleased version of ssreflect and Coq
   allow_failure: true
 
 validate:
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.10
-  needs: ["1.9.0-coq-8.10"]
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  needs: ["build-for-process"]
   dependencies:
-    - 1.9.0-coq-8.10
+    - build-for-process
   script: make validate
 
 validate-classic:
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.10
-  needs: ["1.9.0-coq-8.10-classic"]
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  needs: ["build-for-process-classic"]
   dependencies:
-    - 1.9.0-coq-8.10-classic
+    - build-for-process-classic
   script: make validate
 
 .doc: 
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.10
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
   script:
     - make html -j ${NJOBS}
     - mv html with-proofs
@@ -111,9 +142,9 @@ validate-classic:
 doc:
   extends:
     - .doc
-  needs: ["1.9.0-coq-8.10"]  
+  needs: ["build-for-process"]
   dependencies:
-    - 1.9.0-coq-8.10
+    - build-for-process
   artifacts:
     name: "prosa-spec-$CI_COMMIT_REF_NAME"
     paths:
@@ -125,9 +156,9 @@ doc:
 doc-classic:
   extends:
     - .doc
-  needs: ["1.9.0-coq-8.10-classic"]  
+  needs: ["build-for-process-classic"]
   dependencies:
-    - 1.9.0-coq-8.10-classic
+    - build-for-process-classic
   artifacts:
     name: "prosa-classic-spec-$CI_COMMIT_REF_NAME"
     paths:
@@ -138,10 +169,10 @@ doc-classic:
 
 proof-state:
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.10
-  needs: ["1.9.0-coq-8.10"]  
+  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  needs: ["build-for-process"]
   dependencies:
-    - 1.9.0-coq-8.10
+    - build-for-process
   script:
     - find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . prosa -w -notation-overriden,-parsing' --timeout 20
     - scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`

LICENSE

+BSD 2-Clause License
+
+Copyright (c) 2014–2020, 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.

README.md

@@ -33,13 +33,28 @@ All results published prior to 2020 build on this "classic" version of Prosa.
 - [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
 - [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
 
-## Dependencies 
+## Installation
+
+### With OPAM
+
+Prosa can be installed using the [OPAM package manager](https://opam.ocaml.org/) (>= 2.0)
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
+opam update
+opam install coq-prosa
+```
+
+### From sources
+
+#### Dependencies
 
 Besides Coq itself, Prosa's only external dependency is the ssreflect library of the [Mathematical Components project](https://math-comp.github.io).
 
 Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
 
-## Compiling Prosa
+#### Compiling Prosa
 
 Assuming ssreflect is available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
 

analysis/facts/behavior/service.v

@@ -374,6 +374,18 @@ Section RelationToScheduled.
       rewrite /service_during big_nat_eq0 => IS_ZERO.
       by apply (IS_ZERO t); apply /andP; split => //.
     Qed.
+    
+    (** Conversely, if a job is not scheduled during an interval, then
+        it does not receive any service in that interval *)
+    Lemma not_scheduled_during_implies_zero_service:
+      forall t1 t2,
+        (forall t, t1 <= t < t2 -> ~~ scheduled_at sched j t) -> 
+        service_during sched j t1 t2 = 0.
+    Proof.
+      intros t1 t2 NSCHED.
+      apply big_nat_eq0; move=> t NEQ.
+      by apply no_service_not_scheduled, NSCHED.
+    Qed.
 
     (** If a job is scheduled at some point in an interval, it receives
        positive cumulative service during the interval... *)
@@ -578,3 +590,56 @@ Section RelationToScheduled.
 
 End RelationToScheduled.
 
+Section ServiceInTwoSchedules.
+  
+  (** Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any two given schedules... *)
+  Variable sched1 sched2: schedule PState.
+  
+  (** Given an interval in which the schedules provide the same service 
+      to a job at each instant, we can prove that the cumulative service 
+      received during the interval has to be the same. *)
+  Section ServiceDuringEquivalentInterval.
+    
+    (** Consider two time instants...  *)
+    Variable t1 t2 : instant.
+
+    (** ...and a given job that is to be scheduled. *)
+    Variable j: Job.
+
+    (** Assume that, in any instant between [t1] and [t2] the service 
+        provided to [j] from the two schedules is the same. *)
+    Hypothesis H_sched1_sched2_same_service_at:
+      forall t, t1 <= t < t2 ->
+           service_at sched1 j t = service_at sched2 j t.
+
+    (** It follows that the service provided during [t1] and [t2]
+        is also the same. *)
+    Lemma same_service_during:
+      service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
+    Proof.
+      rewrite /service_during.
+      apply eq_big_nat.
+      by apply H_sched1_sched2_same_service_at.
+    Qed.
+
+  End ServiceDuringEquivalentInterval.
+
+  (** We can leverage the previous lemma to conclude that two schedules
+      that match in a given interval will also have the same cumulative
+      service across the interval. *)
+  Corollary equal_prefix_implies_same_service_during:
+    forall t1 t2,
+      (forall t, t1 <= t < t2 -> sched1 t = sched2 t) ->
+      forall j, service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
+  Proof.
+    move=> t1 t2 SCHED_EQ j.
+    apply same_service_during => t' RANGE.
+    by rewrite /service_at SCHED_EQ.
+  Qed.
+
+End ServiceInTwoSchedules.

analysis/transform/wc_trans.v

+Require Export prosa.analysis.transform.swap.
+Require Export prosa.analysis.transform.prefix.
+Require Export prosa.util.search_arg.
+Require Export prosa.util.list.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Export prosa.model.processor.ideal.
+
+(** In this file we define the transformation from any ideal uniprocessor schedule 
+    into a work-conserving one. The procedure is to patch the idle allocations
+    with future job allocations. Note that a job cannot be allocated before
+    its arrival, therefore there could still exist idle instants between any two
+    job allocations. *)
+Section WCTransformation.
+  
+  (** Consider any type of jobs with arrival times, costs, and deadlines... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobDeadline Job}.
+  
+  (** ...an ideal uniprocessor schedule... *)
+  Let PState := ideal.processor_state Job.
+  
+  (** ...and any valid job arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
+  
+  (** We say that a state is relevant (for the purpose of the
+      transformation) if it is not idle and if the job scheduled in it
+      has arrived prior to some given reference time. *)
+  Definition relevant_pstate reference_time pstate :=
+    match pstate with
+    | None => false
+    | Some j => job_arrival j <= reference_time
+    end.
+  
+  (** In order to patch an idle allocation, we look in the future for another allocation 
+      that could be moved there. The limit of the search is the maximum deadline of
+      every job arrived before the given moment. *)
+  Definition max_deadline_for_jobs_arrived_before arrived_before :=
+    let deadlines := map job_deadline (arrivals_up_to arr_seq arrived_before)
+    in max0 deadlines.
+  
+  (** Next, we define a central element of the work-conserving transformation
+      procedure: given an idle allocation at [t], find a job allocation in the future
+      to swap with. *)
+  Definition find_swap_candidate sched t :=
+    let order _ _ := false (* always take the first result *)
+    in 
+    let max_dl := max_deadline_for_jobs_arrived_before t
+    in
+    let search_result := search_arg sched (relevant_pstate t) order t max_dl
+    in
+    if search_result is Some t_swap
+    then t_swap
+    else t. (* if nothing is found, swap with yourself *)
+  
+  (** The point-wise transformation procedure: given a schedule and a
+      time [t1], ensure that the schedule is work-conserving at time
+      [t1]. *)
+  Definition make_wc_at sched t1 :=
+    match sched t1 with
+    | Some j => sched (* leave working instants alone *)
+    | None =>
+      let
+        t2 := find_swap_candidate sched t1
+      in swapped sched t1 t2
+    end.
+  
+  (** To transform a finite prefix of a given reference schedule, apply
+      [make_wc_at] to every point up to the given finite horizon. *)
+  Definition wc_transform_prefix sched horizon :=
+    prefix_map sched make_wc_at horizon.
+
+  (** Finally, a fully work-conserving schedule (i.e., one that is 
+      work-conserving at any time) is obtained by first computing a 
+      work-conserving prefix up to and including the requested time [t], 
+      and by then looking at the last point of the prefix. *)
+  Definition wc_transform sched t :=
+    let
+      wc_prefix := wc_transform_prefix sched t.+1
+    in wc_prefix t.
+
+End WCTransformation.

coq-prosa.opam

+opam-version: "2.0"
+version: "dev"
+maintainer: "Pierre Roux <pierre.roux@onera.fr>"
+
+homepage: "https://prosa.mpi-sws.org/"
+dev-repo: "git+https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git"
+bug-reports: "https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/issues"
+license: "BSD"
+
+build: [
+  ["./create_makefile.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+depends: [
+  "coq" {((>= "8.9" & < "8.12~") | = "dev")}
+  "coq-mathcomp-ssreflect" {((>= "1.9" & < "1.11~") | = "dev")}
+]
+
+tags: [
+  "keyword:prosa"
+  "keyword:real-time"
+  "keyword:schedulability analysis"
+  "logpath:prosa"
+]
+authors: [
+  "Felipe Cerqueira"
+  "Björn Brandenburg"
+  "Maxime Lesourd"
+  "Sergey Bozhko"
+  "Xiaojie Guo"
+  "Sophie Quinton"
+  "Marco Perronet"
+]
+synopsis: "A Foundation for Formally Proven Schedulability Analysis"
+description: """Prosa is a repository of definitions and proofs for
+real-time schedulability analysis built with Coq. Prosa’s
+distinguishing characteristic is that Prosa prioritizes readability
+over all other concerns to ensure that specifications remain
+accessible to readers without a background in formal proofs. (A
+background in real-time scheduling is assumed.)"""
+url {
+  src: "git+https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git"
+}

util/bigcat.v

 Require Export prosa.util.tactics prosa.util.notation.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-(* Lemmas about the big concatenation operator. *)
+(** In this section, we introduce useful lemmas about the concatenation operation performed
+    over an arbitrary range of sequences. *)
 Section BigCatLemmas.
 
-  Lemma mem_bigcat_nat:
-    forall (T: eqType) x m n j (f: _ -> list T),
-      m <= j < n ->
-      x \in (f j) ->
-      x \in \cat_(m <= i < n) (f i).
-  Proof.
-    intros T x m n j f LE IN; move: LE => /andP [LE LE0].
-    rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
-    rewrite mem_cat; apply/orP; right.
-    destruct n; first by rewrite ltn0 in LE0.
-    rewrite big_nat_recl; last by ins.
-    by rewrite mem_cat; apply/orP; left.
-  Qed.
+  (** Consider any type supporting equality comparisons... *)
+  Variable T: eqType.
 
-  Lemma mem_bigcat_nat_exists :
-    forall (T: eqType) x m n (f: nat -> list T),
-      x \in \cat_(m <= i < n) (f i) ->
-      exists i, x \in (f i) /\
-                m <= i < n.
-  Proof.
-    intros T x m n f IN.
-    induction n; first by rewrite big_geq // in IN.
-    destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
-    rewrite big_nat_recr // /= mem_cat in IN.
-    move: IN => /orP [HEAD | TAIL].
-    {
-      apply IHn in HEAD; destruct HEAD; exists x0.  move: H => [H /andP [H0 H1]].
-      split; first by done.
-      by apply/andP; split; [by done | by apply ltnW].
-    }
-    {
-      exists n; split; first by done.
-      apply/andP; split; [by done | by apply ltnSn].
-    }
-  Qed.
+  (** ...and a function that, given an index, yields a sequence. *)
+  Variable f: nat -> list T.
 
-  Lemma bigcat_nat_uniq :
-    forall (T: eqType) n1 n2 (F: nat -> list T),
-      (forall i, uniq (F i)) ->
-      (forall x i1 i2,
-         x \in (F i1) -> x \in (F i2) -> i1 = i2) ->
-      uniq (\cat_(n1 <= i < n2) (F i)).
-  Proof.
-    intros T n1 n2 f SINGLE UNIQ.
-    case (leqP n1 n2) => [LE | GT]; last by rewrite big_geq // ltnW.
-    rewrite -[n2](addKn n1).
-    rewrite -addnBA //; set delta := n2 - n1.
-    induction delta; first by rewrite addn0 big_geq.
-    rewrite addnS big_nat_recr /=; last by apply leq_addr.
-    rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
-    apply /andP; split; last by apply SINGLE.
-    rewrite -all_predC; apply/allP; intros x INx.
-    simpl; apply/negP; unfold not; intro BUG.
-    apply mem_bigcat_nat_exists in BUG.
-    move: BUG => [i [IN /andP [_ LTi]]].
-    apply UNIQ with (i1 := i) in INx; last by done.
-    by rewrite INx ltnn in LTi.
-  Qed.
+  (** In this section, we prove that the concatenation over sequences works as expected: 
+      no element is lost during the concatenation, and no new element is introduced. *)
+  Section BigCatElements.
+    
+    (** First, we show that the concatenation comprises all the elements of each sequence; 
+        i.e. any element contained in one of the sequences will also be an element of the 
+        result of the concatenation. *)
+    Lemma mem_bigcat_nat:
+      forall x m n j,
+        m <= j < n ->
+        x \in f j ->
+        x \in \cat_(m <= i < n) (f i).
+    Proof.
+      intros x m n j LE IN; move: LE => /andP [LE LE0].
+      rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
+      rewrite mem_cat; apply/orP; right.
+      destruct n; first by rewrite ltn0 in LE0.
+      rewrite big_nat_recl; last by ins.
+        by rewrite mem_cat; apply/orP; left.
+    Qed.
+
+    (** Conversely, we prove that any element belonging to a concatenation of sequences 
+        must come from one of the sequences. *)
+    Lemma mem_bigcat_nat_exists :
+      forall x m n,
+        x \in \cat_(m <= i < n) (f i) ->
+        exists i,
+          x \in f i /\ m <= i < n.
+    Proof.
+      intros x m n IN.
+      induction n; first by rewrite big_geq // in IN.
+      destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
+      rewrite big_nat_recr // /= mem_cat in IN.
+      move: IN => /orP [HEAD | TAIL].
+      {
+        apply IHn in HEAD; destruct HEAD; exists x0.  move: H => [H /andP [H0 H1]].
+        split; first by done.
+          by apply/andP; split; [by done | by apply ltnW]. }
+      {
+        exists n; split; first by done.
+        apply/andP; split; [by done | by apply ltnSn]. }
+    Qed.
+    
+  End BigCatElements.
+
+  (** In this section, we show how we can preserve uniqueness of the elements 
+      (i.e. the absence of a duplicate) over a concatenation of sequences. *)
+  Section BigCatDistinctElements.
+
+    (** Assume that there are no duplicates in each of the possible
+        sequences to concatenate... *)
+    Hypothesis H_uniq_seq: forall i, uniq (f i).
+
+    (** ...and that there are no elements in common between the sequences. *)
+    Hypothesis H_no_elements_in_common:
+      forall x i1 i2, x \in f i1 -> x \in f i2 -> i1 = i2.
+    
+    (** We prove that the concatenation will yield a sequence with unique elements. *)
+    Lemma bigcat_nat_uniq :
+      forall n1 n2,
+        uniq (\cat_(n1 <= i < n2) (f i)).
+    Proof.
+      intros n1 n2.
+      case (leqP n1 n2) => [LE | GT]; last by rewrite big_geq // ltnW.
+      rewrite -[n2](addKn n1).
+      rewrite -addnBA //; set delta := n2 - n1.
+      induction delta; first by rewrite addn0 big_geq.
+      rewrite addnS big_nat_recr /=; last by apply leq_addr.
+      rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
+      apply /andP; split; last by apply H_uniq_seq.
+      rewrite -all_predC; apply/allP; intros x INx.
+      simpl; apply/negP; unfold not; intro BUG.
+      apply mem_bigcat_nat_exists in BUG.
+      move: BUG => [i [IN /andP [_ LTi]]].
+      apply H_no_elements_in_common with (i1 := i) in INx; last by done.
+      by rewrite INx ltnn in LTi.
+    Qed.
+    
+  End BigCatDistinctElements.
   
 End BigCatLemmas.