From bd5383a17b1884645533338b5dbde4e859a3b31d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 14 May 2019 17:28:45 +0200
Subject: [PATCH] port scheduler_executes_job_with_earliest_arrival

---
 behavior/facts/all.v        |  1 +
 behavior/facts/sequential.v | 42 +++++++++++++++++++++++++++++++++++++
 behavior/sequential.v       | 29 +++++++++++++++++++++++++
 behavior/task.v             | 16 +++++++++++++-
 4 files changed, 87 insertions(+), 1 deletion(-)
 create mode 100644 behavior/facts/sequential.v
 create mode 100644 behavior/sequential.v

diff --git a/behavior/facts/all.v b/behavior/facts/all.v
index 534cdb2a7..d455c2ba5 100644
--- a/behavior/facts/all.v
+++ b/behavior/facts/all.v
@@ -1,3 +1,4 @@
 Require Export rt.behavior.facts.service.
 Require Export rt.behavior.facts.completion.
 Require Export rt.behavior.facts.ideal_schedule.
+Require Export rt.behavior.facts.sequential.
diff --git a/behavior/facts/sequential.v b/behavior/facts/sequential.v
new file mode 100644
index 000000000..27cad7cf8
--- /dev/null
+++ b/behavior/facts/sequential.v
@@ -0,0 +1,42 @@
+From rt.behavior Require Export sequential.
+
+Section ExecutionOrder.
+  (* Consider any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... with arrival times and costs ... *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* ... and any kind of processor state model. *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Assume a schedule ... *)
+  Variable sched: schedule PState.
+
+  (* in which the sequential jobs hypothesis holds. *)
+  Hypothesis H_sequential_jobs: sequential_jobs sched.
+
+
+  (* A simple corollary of this hypothesis is that the scheduler
+     executes a job with the earliest arrival time. *)
+  Corollary scheduler_executes_job_with_earliest_arrival:
+    forall j1 j2 t,
+      same_task j1 j2 ->
+      ~~ completed_by sched j2 t ->
+      scheduled_at sched j1 t ->
+      job_arrival j1 <= job_arrival j2.
+  Proof.
+    intros ? ? t TSK NCOMPL SCHED.
+    rewrite /same_task eq_sym in TSK.
+    have SEQ := H_sequential_jobs j2 j1 t TSK.
+    rewrite leqNgt; apply/negP; intros ARR.
+    move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
+      by apply SEQ.
+  Qed.
+
+End ExecutionOrder.
+
diff --git a/behavior/sequential.v b/behavior/sequential.v
new file mode 100644
index 000000000..974e6719a
--- /dev/null
+++ b/behavior/sequential.v
@@ -0,0 +1,29 @@
+From rt.behavior Require Export schedule task.
+
+Section PropertyOfSequentiality.
+  (* Consider any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... with arrival times and costs ... *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* ... and any kind of processor state model. *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Given a schedule ... *)
+  Variable sched: schedule PState.
+
+  (* ...we say that jobs (or, rather, tasks) are sequential if each task's jobs
+     are executed in the order they arrived. *)
+  Definition sequential_jobs :=
+    forall (j1 j2: Job) (t: instant),
+      same_task j1 j2 ->
+      job_arrival j1 < job_arrival j2 ->
+      scheduled_at sched j2 t ->
+      completed_by sched j1 t.
+
+End PropertyOfSequentiality.
diff --git a/behavior/task.v b/behavior/task.v
index 2759d28a6..600edb5d1 100644
--- a/behavior/task.v
+++ b/behavior/task.v
@@ -1,3 +1,4 @@
+From mathcomp Require Export ssrbool.
 From rt.behavior Require Export job.
 
 (* Throughout the library we assume that jobs have decidable equality *)
@@ -6,4 +7,17 @@ Definition TaskType := eqType.
 
 (* Definition of a generic type of parameter relating jobs to tasks *)
 
-Class JobTask (T : TaskType) (J : JobType) := job_task : J -> T.
\ No newline at end of file
+Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
+
+
+Section SameTask.
+  (* For any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1
+     is equal to job_task j2. *)
+  Definition same_task j1 j2 := job_task j1 == job_task j2.
+
+End SameTask.
-- 
GitLab