From 9fa2acb3cf74f7ca07a489e722ad9673c2195647 Mon Sep 17 00:00:00 2001
From: Vedant Chavda <f20180209@goa.bits-pilani.ac.in>
Date: Thu, 26 Mar 2020 23:01:27 +0530
Subject: [PATCH] add notion of hyperperiod for periodic tasks

---
 analysis/definitions/hyperperiod.v | 33 ++++++++++++++++++++
 scripts/wordlist.pws               |  1 +
 util/lcmseq.v                      | 48 ++++++++++++++++++++++++++++++
 3 files changed, 82 insertions(+)
 create mode 100644 analysis/definitions/hyperperiod.v
 create mode 100644 util/lcmseq.v

diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
new file mode 100644
index 000000000..700f9f790
--- /dev/null
+++ b/analysis/definitions/hyperperiod.v
@@ -0,0 +1,33 @@
+Require Export prosa.model.task.arrival.periodic.
+Require Export prosa.util.lcmseq.
+From mathcomp Require Import div.
+
+(** In this file we define the notion of a hyperperiod for periodic tasks. *)
+Section Hyperperiod.
+
+  (** Consider periodic tasks. *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** Consider any task set [ts]... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any task [tsk] that belongs to this task set. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** The hyperperiod of a task set is defined as the least common multiple
+   (LCM) of the periods of all tasks in the task set. **)
+  Definition hyperperiod : duration := lcml (map task_period ts).        
+
+  (** Consequently, a task set's hyperperiod is an integral multiple
+   of each task's period in the task set. **)
+  Lemma hyperperiod_int_mult_of_any_task : 
+    exists k, hyperperiod = k * task_period tsk.
+  Proof.
+    apply lcm_seq_is_mult_of_all_ints.
+    apply map_f.
+    by apply H_tsk_in_ts.
+  Qed.
+
+End Hyperperiod.
+
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 6288451fa..51df7c7b3 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -48,3 +48,4 @@ runtime
 bursty
 TODO
 mathcomp
+hyperperiod
diff --git a/util/lcmseq.v b/util/lcmseq.v
new file mode 100644
index 000000000..4407c40db
--- /dev/null
+++ b/util/lcmseq.v
@@ -0,0 +1,48 @@
+From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
+
+(** A function to calculate the least common multiple 
+    of all integers in a sequence [xs], denoted by [lcml xs]  **)
+Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.
+
+(** Any integer [a] that is contained in the sequence [xs] divides [lcml xs]. **)
+Lemma int_divides_lcm_in_seq : 
+  forall (a : nat) (xs : seq nat), a %| lcml (a :: xs).
+Proof.
+  intros.
+  rewrite /lcml.
+  induction xs.
+  - rewrite /foldr.
+    now apply dvdn_lcml.
+  - rewrite -cat1s.
+    rewrite foldr_cat /foldr.
+    by apply dvdn_lcml.
+Qed.
+
+(** Also, [lcml xs1] divides [lcml xs2] if [xs2] contains one extra element as compared to [xs1]. *)
+Lemma lcm_seq_divides_lcm_super : 
+  forall (x : nat) (xs : seq nat), 
+  lcml xs %| lcml (x :: xs).
+Proof.
+  intros.
+  rewrite /lcml.
+  induction xs; first by auto.
+  rewrite -cat1s foldr_cat /foldr.
+  by apply dvdn_lcmr.
+Qed.
+
+(** All integers in a sequence [xs] divide [lcml xs]. *)
+Lemma lcm_seq_is_mult_of_all_ints : 
+  forall (sq : seq nat) (a : nat), a \in sq -> exists k, lcml sq = k * a. 
+Proof.
+  intros xs x IN.
+  induction xs as [ | z sq IH_DIVIDES]; first by easy.
+  rewrite in_cons in IN.
+  move : IN => /orP [/eqP EQ | IN].
+  + apply /dvdnP.
+    rewrite EQ /lcml.
+    by apply int_divides_lcm_in_seq.
+  + move : (IH_DIVIDES IN) => [k EQ].
+    exists ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) * k).
+    rewrite -mulnA -EQ divnK /lcml //.
+    by apply lcm_seq_divides_lcm_super.
+Qed.
-- 
GitLab