port scheduler_executes_job_with_earliest_arrival

behavior/facts/all.v

 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.

behavior/facts/sequential.v

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

behavior/sequential.v

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

behavior/task.v

+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.
+Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
\ No newline at end of file
+
+
+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.