Add notion of non-preemptive schedule

restructuring/analysis/basic_facts/sequential.v

@@ -17,8 +17,8 @@ Section ExecutionOrder.
   (** Assume a schedule ... *)
   Variable sched: schedule PState.
 
-  (** in which the sequential jobs hypothesis holds. *)
-  Hypothesis H_sequential_jobs: sequential_jobs sched.
+  (** in which the sequential tasks hypothesis holds. *)
+  Hypothesis H_sequential_tasks: sequential_tasks sched.
 
 
   (** A simple corollary of this hypothesis is that the scheduler
@@ -32,7 +32,7 @@ Section ExecutionOrder.
   Proof.
     intros ? ? t TSK NCOMPL SCHED.
     rewrite /same_task eq_sym in TSK.
-    have SEQ := H_sequential_jobs j2 j1 t TSK.
+    have SEQ := H_sequential_tasks j2 j1 t TSK.
     rewrite leqNgt; apply/negP; intros ARR.
     move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
       by apply SEQ.

restructuring/model/schedule/nonpreemptive.v

+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.model Require Import job.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(** In this section we introduce the notion of a non-preemptive schedule. *)
+Section NonpreemptiveSchedule.
+
+  (** Consider any type of jobs ... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... and any kind of processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+  
+  (** Consider any uniprocessor schedule. *)
+  Variable sched : schedule PState.
+
+  (** We define a schedule to be nonpreemptive iff every job remains scheduled until completion. *)
+  Definition is_nonpreemptive_schedule := 
+    forall (j : Job) (t t' : instant),
+      t <= t' -> 
+      scheduled_at sched j t ->
+      ~~ completed_by sched j t' -> 
+      scheduled_at sched j t'. 
+
+End NonpreemptiveSchedule.
\ No newline at end of file

restructuring/model/schedule/sequential.v

@@ -19,9 +19,9 @@ Section PropertyOfSequentiality.
   (** Given a schedule ... *)
   Variable sched: schedule PState.
 
-  (** ...we say that jobs (or, rather, tasks) are sequential if each task's jobs
+  (** ...we say that tasks are sequential if each task's jobs
      are executed in the order they arrived. *)
-  Definition sequential_jobs :=
+  Definition sequential_tasks :=
     forall (j1 j2: Job) (t: instant),
       same_task j1 j2 ->
       job_arrival j1 < job_arrival j2 ->