Commit 8313f7c6 authored by Sergey Bozhko's avatar Sergey Bozhko Committed by Björn Brandenburg

update task and job models in preparation of aRTA port

Also removes an unnecessary module in rt.util.epsilon.
parent 0fbee8da
Pipeline #19445 passed with stages
in 6 minutes and 27 seconds
......@@ -15,8 +15,8 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTA.
Import Job Epsilon UniprocessorSchedule Service ResponseTime
AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction.
Import Job UniprocessorSchedule Service ResponseTime AbstractRTADefinitions
AbstractRTALockInService AbstractRTAReduction.
(* In this section we prove that the maximum among the solutions of the response-time bound
recurrence is a response time bound for tsk. Note that in this section we do not rely on
......
......@@ -23,7 +23,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
and sequential jobs. *)
Module AbstractSeqRTA.
Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
Import Job ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
Service ResponseTime MaxArrivalsWorkloadBound
AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction AbstractRTA.
......
......@@ -9,7 +9,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTADefinitions.
Import Job Epsilon UniprocessorSchedule.
Import Job UniprocessorSchedule.
(* In this section, we introduce all the abstract notions required by the analysis. *)
Section Definitions.
......
......@@ -10,7 +10,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
Module AbstractRTAReduction.
Import Epsilon UniprocessorSchedule.
Import UniprocessorSchedule.
(* The response-time analysis we are presenting in this series of documents is based on searching
over all possible values of A, the relative arrival time of the job respective to the beginning
......
......@@ -12,7 +12,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
receives enough service to become nonpreemptive. *)
Module AbstractRTALockInService.
Import Job Epsilon UniprocessorSchedule Service AbstractRTADefinitions.
Import Job UniprocessorSchedule Service AbstractRTADefinitions.
(* Previously we defined the notion of lock-in service (see limited.schedule.v file).
Lock-in service is the amount of service after which a job cannot be preempted until
......
......@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(4) EDF with floating nonpreemptive regions. *)
Module RTAforConcreteModels.
Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
FullyNonPreemptivePlatform FullyPreemptivePlatform AbstractRTAforEDFwithArrivalCurves.
......
......@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this module we prove a general RTA theorem for EDF-schedulers. *)
Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
AbstractRTAforEDFwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded.
......
......@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
EDF uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTAforEDFwithArrivalCurves.
Import Job Epsilon ArrivalCurves TaskArrival ScheduleOfTask Priority
Import Job ArrivalCurves TaskArrival ScheduleOfTask Priority
UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
BusyIntervalJLFP LimitedPreemptionPlatform RBF Service JLFPInstantiation.
......
......@@ -24,7 +24,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(4) FP with floating nonpreemptive regions. *)
Module RTAforConcreteModels.
Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
FullyNonPreemptivePlatform FullyPreemptivePlatform.
......
......@@ -21,7 +21,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this module we prove a general RTA theorem for FP-schedulers *)
Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
AbstractRTAforFPwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded.
......
......@@ -25,7 +25,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
FP uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Module AbstractRTAforFPwithArrivalCurves.
Import Epsilon Job ArrivalCurves TaskArrival Priority ScheduleOfTask
Import Job ArrivalCurves TaskArrival Priority ScheduleOfTask
UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
LimitedPreemptionPlatform RBF BusyIntervalJLFP JLFPInstantiation.
......
......@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
predicate for various preemption models. *)
Module LimitedPreemptionPlatform.
Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority Service.
Import Job SporadicTaskset UniprocessorSchedule Priority Service.
(* In this section, we define a processor platform with limited preemptions. *)
Section Properties.
......
......@@ -13,7 +13,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
model with floating nonpreemptive regions. *)
Module ModelWithLimitedPreemptions.
Import Epsilon Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
Import Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
(* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)
......
......@@ -17,7 +17,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
can_be_preempted for the fully nonpreemptive model and prove its correctness. *)
Module FullyNonPreemptivePlatform.
Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
Import Job SporadicTaskset UniprocessorSchedule Priority
Service LimitedPreemptionPlatform.
Section FullyNonPreemptiveModel.
......
......@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
can_be_preempted for the fully preemptive model and prove its correctness. *)
Module FullyPreemptivePlatform.
Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
Import Job SporadicTaskset UniprocessorSchedule Priority
Service LimitedPreemptionPlatform.
Section FullyPreemptiveModel.
......
......@@ -15,7 +15,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
is bounded. *)
Module PriorityInversionIsBounded.
Import Epsilon Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP.
Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP.
Section PriorityInversionIsBounded.
......
......@@ -7,7 +7,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In this file, we provide additional definitions and
lemmas about lock-in-serivce-compliant schedules. *)
Import Job Epsilon Service UniprocessorSchedule.
Import Job Service UniprocessorSchedule.
Section Definitions.
......
From rt.restructuring.behavior Require Export time.
From mathcomp Require Export eqtype.
From mathcomp Require Export eqtype ssrnat.
(* Throughout the library we assume that jobs have decidable equality *)
Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J -> duration.
(* Definition of a generic type of parameter for job_arrival *)
Class JobArrival (J : JobType) := job_arrival : J -> instant.
(* Definition of a generic type of parameter relating jobs to an absolute deadline *)
Class JobDeadline (J : JobType) := job_deadline : J -> instant.
(* Definition of a generic type of release jitter parameter. *)
Class JobJitter (J : JobType) := job_jitter : J -> duration.
Class JobJitter (J : JobType) := job_jitter : J -> duration.
\ No newline at end of file
From rt.restructuring.behavior Require Export time job.
From mathcomp Require Export eqtype ssrnat.
(* In this section, we introduce properties of a job. *)
Section PropertesOfJob.
(* Assume that job costs are known. *)
Context {Job : JobType}.
Context `{JobCost Job}.
(* Consider an arbitrary job. *)
Variable j: Job.
(* The job cost must be positive. *)
Definition job_cost_positive := job_cost j > 0.
End PropertesOfJob.
\ No newline at end of file
......@@ -25,4 +25,5 @@ Section Priority.
backlogged sched j t ->
scheduled_at sched j_hp t ->
hep_job_at t j_hp j.
End Priority.
......@@ -2,9 +2,10 @@ From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.model Require Export task.
Section PropertyOfSequentiality.
(* Consider any type of job associated with any type of tasks... *)
Context {Job: JobType}.
Context {Task: TaskType}.
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(* ... with arrival times and costs ... *)
......
From rt.restructuring.model Require Import task.
From rt.restructuring.behavior Require Import schedule ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Due to historical reasons this file defines the notion of a schedule of
a task for the ideal uniprocessor model. This is not a fundamental limitation
and the notion can be further generalized to an arbitrary model. *)
(** * Schedule of task *)
(** In this section we define properties of schedule of a task *)
Section ScheduleOfTask.
(* 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}.
(* Let sched be any ideal uniprocessor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
Section TaskProperties.
(* Let tsk be any task. *)
Variable tsk : Task.
(* Next we define whether a task is scheduled at time t, ... *)
Definition task_scheduled_at (t : instant) :=
if sched t is Some j then
job_task j == tsk
else false.
(* ...which also corresponds to the instantaneous service it receives. *)
Definition task_service_at (t: instant) := task_scheduled_at t.
(* Based on the notion of instantaneous service, we define the
cumulative service received by tsk during any interval [t1, t2)... *)
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
(* ...and the cumulative service received by tsk up to time t2,
i.e., in the interval [0, t2). *)
Definition task_service (t2 : instant) := task_service_during 0 t2.
End TaskProperties.
End ScheduleOfTask.
\ No newline at end of file
From mathcomp Require Export ssrbool.
From rt.restructuring.behavior Require Export job.
From rt.restructuring.behavior Require Export arrival_sequence.
(* Throughout the library we assume that tasks have decidable equality *)
Definition TaskType := eqType.
(* Definition of a generic type of parameter relating jobs to tasks *)
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}.
......@@ -21,12 +22,112 @@ Section SameTask.
End SameTask.
(* Definition of a generic type of parameter for task deadlines *)
Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
(* Given task deadlines and a mapping from jobs to tasks we provide a generic definition of job_deadline *)
Instance job_deadline_from_task_deadline
(Job : JobType) (Task : TaskType)
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} :
JobDeadline Job := fun j => job_arrival j + task_deadline (job_task j).
(Job : JobType) (Task : TaskType)
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JobDeadline Job :=
fun j => job_arrival j + task_deadline (job_task j).
(* Definition of a generic type of parameter for task cost *)
Class TaskCost (T : TaskType) := task_cost : T -> duration.
(* In this section, we introduce properties of a task. *)
Section PropertesOfTask.
(* Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
(* Next we intrdoduce attributes of a valid sporadic task. *)
Section ValidTask.
(* Consider an arbitrary task. *)
Variable tsk: Task.
(* The cost and deadline of the task must be positive. *)
Definition task_cost_positive := task_cost tsk > 0.
Definition task_deadline_positive := task_deadline tsk > 0.
(* The task cost cannot be larger than the deadline or the period. *)
Definition task_cost_le_deadline := task_cost tsk <= task_deadline tsk.
End ValidTask.
(* Job of task *)
Section ValidJobOfTask.
(* Consider any type of jobs associated with the tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
(* Consider an arbitrary job. *)
Variable j: Job.
(* The job cost cannot be larger than the task cost. *)
Definition job_cost_le_task_cost :=
job_cost j <= task_cost (job_task j).
End ValidJobOfTask.
(* Jobs of task *)
Section ValidJobsTask.
(* Consider any type of jobs associated with the tasks ... *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
(* ... and any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(* The cost of a job from the arrival sequence cannot
be larger than the task cost. *)
Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
forall j,
arrives_in arr_seq j ->
job_cost_le_task_cost j.
End ValidJobsTask.
End PropertesOfTask.
(* In this section, we introduce properties of a task set. *)
Section PropertesOfTaskSet.
(* 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 `{JobCost Job}.
(* ... and any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(* Consider an arbitrary task set. *)
Variable ts : seq Task.
(* Tasks from the task set have a positive cost. *)
Definition tasks_cost_positive :=
forall tsk,
tsk \in ts ->
task_cost_positive tsk.
(* All jobs in the arrival sequence come from the taskset. *)
Definition all_jobs_from_taskset :=
forall j,
arrives_in arr_seq j ->
job_task j \in ts.
End PropertesOfTaskSet.
\ No newline at end of file
......@@ -3,15 +3,18 @@ From rt.restructuring.model Require Export task.
(* In this file we provide basic definitions related to tasks on arrival sequences *)
Section TaskArrivals.
Context {Job : JobType} {Task : TaskType}.
(* Consider any type of job associated with any type of tasks. *)
Context {Job: JobType}.
Context {Task: TaskType}.
Context `{JobTask Job Task}.
(* Consider any job arrival sequence, *)
(* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
Section Definitions.
(* And a given task *)
(* Let tsk be any task. *)
Variable tsk : Task.
(* We define the sequence of jobs of tsk arriving at time t *)
......
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
Section TaskCost.
Context {T : TaskType}.
Variable (task_cost : duration).
Definition valid_task_cost := task_cost > 0.
End TaskCost.
(* Definition of a generic type of parameter for task cost *)
Class TaskCost (T : TaskType) := task_cost : T -> duration.
Section TasksetCosts.
Context {T : TaskType} `{TaskCost T}.
Variable ts : seq T.
Definition valid_taskset_costs :=
forall tsk : T,
tsk \in ts ->
task_cost tsk > 0.
Context {J : JobType} `{JobTask J T} `{JobCost J}.
Variable arr_seq : arrival_sequence J.
Definition respects_taskset_costs :=
forall j,
arrives_in arr_seq j ->
job_cost j <= task_cost (job_task j).
End TasksetCosts.
Module Epsilon.
Section Epsilon.
(* ε is defined as the smallest positive number. *)
Definition ε := 1.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment