Add preemption model

restructuring/model/preemption/preemption_model.v

+From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.model Require Import job task.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Platform with limited preemptions *)
+(** Since the notion of preemption points is based on an user-provided 
+    predicate (variable job_can_be_preempted), it does not guarantee that 
+    the scheduler will enforce correct behavior. For that, we must 
+    define additional predicates. *)
+Section ValidPreemptionModel.
+
+  (* Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (*  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* In addition, we assume the existence of a function
+     maping jobs to theirs preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (* Consider any kind of processor state model, ... *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* ... any job arrival sequence, ... *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (* ... and any given schedule. *)
+  Variable sched: schedule PState.
+
+  (* For simplicity, let's define some local names. *)
+  Let job_pending := pending sched.
+  Let job_completed_by := completed_by sched.
+  Let job_scheduled_at := scheduled_at sched.
+
+  (* We require that a job has to be executed at least one time instant
+     in order to reach a nonpreemptive segment. In other words, a job 
+     must start execution to become non-preemptive. *)
+  Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
+    job_preemptable j 0.
+    
+  (* And vice versa, a job cannot remain non-preemptive after its completion. *)
+  Definition job_cannot_be_nonpreemptive_after_completion (j : Job) := 
+    job_preemptable j (job_cost j).
+  
+  (* Next, if a job j is not preemptive at some time instant t, 
+     then j must be scheduled at time t. *)
+  Definition not_preemptive_implies_scheduled (j : Job) :=
+    forall t,
+      ~~ job_preemptable j (service sched j t) ->
+      job_scheduled_at j t. 
+
+  (* A job can start its execution only from a preemption point. *)
+  Definition execution_starts_with_preemption_point (j : Job) := 
+    forall prt,
+      ~~ job_scheduled_at j prt ->
+      job_scheduled_at j prt.+1 ->
+      job_preemptable j (service sched j prt.+1).
+
+  (* We say that a preemption model is a valid preemption model if 
+     all the assumptions given above are satisfied for any job. *)
+  Definition valid_preemption_model :=
+    forall j,
+      arrives_in arr_seq j ->
+      job_cannot_become_nonpreemptive_before_execution j
+      /\ job_cannot_be_nonpreemptive_after_completion j
+      /\ not_preemptive_implies_scheduled j
+      /\ execution_starts_with_preemption_point j.
+  
+End ValidPreemptionModel.
\ No newline at end of file