Can_be_preempted function
In this issue I want to discuss the semantics of function can_be_preempted.
Context:
At some point we began to consider different models of preemptions (fully preemptive model, fully nonpreemptive model and so on). It turned out that these models are more or less similar and significantly differ only in one hypothesis. The main idea is that at each of the preemption points a job with the highest priority should be executed. For different preemption models, these points will be different.
Each of these models has a different hypothesis of respects_FP_policy (respects_JLFP_policy).
That is, for fully preemptive model it looks like this:
Definition respects_FP_policy :=
forall j j_hp t,
arrives_in arr_seq j ->
backlogged job_arrival job_cost sched j t ->
scheduled_at sched j_hp t ->
higher_eq_priority (job_task j_hp) (job_task j).
And for fully non-preemptive model it looks like this:
Definition respects_FP_policy_at_preemption_point :=
forall j j_hp t,
arrives_in arr_seq j ->
backlogged job_arrival job_cost sched j t ->
scheduled_at sched j_hp t ->
is_preemption_point t -> (* New line *)
higher_eq_priority (job_task j_hp) (job_task j).
It is clear that these hypotheses can be generalized. To do this, we simply consider the more general function is_preemption_point
. Further we call it can_be_preempted
.
Problem:
But there are some difficulties. What exactly is the function can_be_preempted?
There can be at least two options:
can_be_preempted is a function that takes (arrival sequence), schedule, job, and time (not progress) and returns yes/no. That is, for some schedule sched, job j, and some time instant t, function can_be_preempted says whether job j is preemptive at time t in (this specific) schedule sched.
For example. A job can be preempted at a time instant t iff at time t it has not started execution yet or has already been completed. (Note that the service essentially depends on the schedule.)
(* We say that the model is fully nonpreemptive
iff every job cannot be preempted until its completion. *)
Definition fully_nonpreemptive_model (j: Job) (t: time) :=
(service sched j t == 0) || (service sched j t == job_cost j).
I've been using this definition for a while until @bbb said that it was not very intuitive because conceptually function can_be_preempted is just a function that maps progress of a job to yes/no. Here, progress is simply a synonym for service. That is, a job consists of some non-preemptive segments (we may not know exactly which ones). This job is executed in some way. To find out whether the job is preemptive at a time instant t, it is sufficient to (1) compute the service of job j at time instant t, (2) ask function can_be_preempted if j can be preempted at this point of execution.
As a result, we came to the following option:
(* Let can_be_preempted be a function that maps a job j and the progress of j
at some time instant t to a boolean value, i.e., true if job j can be
preempted at this point of execution and false otherwise. *)
Variable can_be_preempted: Job -> time (* = progress *) -> bool.
(* ... *)
(* + Some additional hypotheses. *)
Indeed, such a definition simplifies life for “simple” models, for example:
(* In the fully preemptive model any job can be preempted at any time. *)
Definition fully_preemptive_model (j: Job) (progr: time) := true.
(* We say that the model is fully nonpreemptive
iff every job cannot be preempted until its completion. *)
Definition fully_nonpreemptive_model (j: Job) (progr: time) :=
(progr == 0) || (progr == job_cost j).
(* Given a list of preemption points for each job (i.e., units of received service),
we define the fixed preemption point model as follows. ... *)
Definition fixed_preemption_points_model (j: Job) (progr: time) :=
progr \in job_preemption_points j.
But I’m having difficulties defining for the model with floating nonpreemptive regions (F-NP-R for short).
It is important to note that our abstract hypotheses are general enough to describe this model (you can check them here). But I cannot define the specific function that describes exactly F-NP-R model.
I am going to use the following description. Consider a job j. Assume that job j is executed. At the moment when a job j_hp with higher priority appears, job j becomes non-preemptive for a certain amount of time (this time is bounded by some constant defined by the task). And then becomes preemptive again. Similar definition can be found here.
A floating non-preemptive region starts when the highest priority job is executing on the processor and a higher priority job is released. We denote by Q_i the length of the non-preemptive regions of task tau_i. This means that once a floating non-preemptive region has started, it will last for Q_i time units unless the currently running job completes before. Therefore, the preemption points which lead to the worst-case cumulative preemption delay are subject to the constraint of being distanced by at least Q_i time units apart.
Now let's go back to the can_be_preempted function for F-NP-R model. Consider a job j and some progress of this job p. In the previous models this information is already enough to determine whether the job is preemptive or not (for any schedule).
But now the same job can be both preemptive and non-preemptive for different schedules.
For example. Same job j, same progress p. But job j is preemptive in sched1 and nonpreemptive in sched2.
As you can see, can_be_preempted essentially depends on the schedule and specific time in this schedule.
As a result, I have decided to use this definition. It does not work though, since it simply does not fit the interface of the can_be_preempted function (it is not a function: job -> progress -> bool ).
(* We say that a job j is in a nonpreemptive region at time t_current iff
(1) there exists the first preemption attempt [t_first_attempt] and (2) t_current
lies in the time interval [t_first_attempt, t_first_attempt + job_floating j). *)
Definition is_in_nonpreemptive_region (j: Job) (t_current: time) :=
exists t_first_attempt,
first_preemption_attempt j t_first_attempt t_current /\
t_first_attempt <= t_current < t_first_attempt + job_floating j.
(* In the model with floating nonpreemptive regions a job j can be preempted at
a time moment t if one of the following cases holds: (1) the job j hasn't
scheduled before, or (2) j is completed at the time moment t, or (3) the job
j doesn't execute in a nonpreemptive region. *)
Definition floating_nonpreemptive_regions_model (j: Job) (progr: time) (t: time) :=
(progr == 0) || (progr == job_cost j) || ~~ is_in_nonpreemptive_region j t.
(* Alternatively: *)
Definition floating_nonpreemptive_regions_model (j: Job) (t: time) :=
(service sched j t == 0) || (service sched j t == job_cost j) || ~~ is_in_nonpreemptive_region j t.
What do you think? Do I need to change the definition of the function can_be_preempted back? Or maybe I missed something regarding the definition of the function can_be_preempted for the case of a model with floating nonpreemptive regions?