Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Vedant Chavda
PROSA - Formally Proven Schedulability Analysis
Commits
22a76ba8
Commit
22a76ba8
authored
Dec 02, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
address spell-checking issues in model module
parent
ce01dfe1
Changes
15
Hide whitespace changes
Inline
Side-by-side
Showing
15 changed files
with
84 additions
and
67 deletions
+84
-67
restructuring/model/aggregate/service_of_jobs.v
restructuring/model/aggregate/service_of_jobs.v
+9
-7
restructuring/model/aggregate/task_arrivals.v
restructuring/model/aggregate/task_arrivals.v
+10
-7
restructuring/model/aggregate/workload.v
restructuring/model/aggregate/workload.v
+9
-7
restructuring/model/arrival/arrival_curves.v
restructuring/model/arrival/arrival_curves.v
+20
-16
restructuring/model/preemption/fully_preemptive.v
restructuring/model/preemption/fully_preemptive.v
+1
-1
restructuring/model/preemption/parameter.v
restructuring/model/preemption/parameter.v
+2
-2
restructuring/model/priority/classes.v
restructuring/model/priority/classes.v
+1
-1
restructuring/model/readiness/basic.v
restructuring/model/readiness/basic.v
+1
-1
restructuring/model/readiness/jitter.v
restructuring/model/readiness/jitter.v
+1
-1
restructuring/model/schedule/work_conserving.v
restructuring/model/schedule/work_conserving.v
+9
-6
restructuring/model/task/concept.v
restructuring/model/task/concept.v
+6
-4
restructuring/model/task/preemption/floating_nonpreemptive.v
restructuring/model/task/preemption/floating_nonpreemptive.v
+1
-1
restructuring/model/task/preemption/limited_preemptive.v
restructuring/model/task/preemption/limited_preemptive.v
+2
-2
restructuring/model/task/preemption/parameters.v
restructuring/model/task/preemption/parameters.v
+11
-11
scripts/wordlist.pws
scripts/wordlist.pws
+1
-0
No files found.
restructuring/model/aggregate/service_of_jobs.v
View file @
22a76ba8
...
...
@@ -59,13 +59,15 @@ Section ServiceOfJobs.
(** Let jobs denote any (finite) set of jobs. *)
Variable
jobs
:
seq
Job
.
(** Let tsk be the task to be analyzed. *)
(** Let
[
tsk
]
be the task to be analyzed. *)
Variable
tsk
:
Task
.
(** Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
(** Based on the definition of jobs of higher or equal priority
(with respect to task [tsk]), ... *)
Let
of_higher_or_equal_priority
j
:
=
higher_eq_priority
(
job_task
j
)
tsk
.
(** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
(** ...we define the service received during [[t1, t2)] by jobs of
higher or equal priority. *)
Definition
service_of_higher_or_equal_priority_tasks
(
t1
t2
:
instant
)
:
=
service_of_jobs
of_higher_or_equal_priority
jobs
t1
t2
.
...
...
@@ -87,7 +89,7 @@ Section ServiceOfJobs.
(** Based on the definition of jobs of higher or equal priority, ... *)
Let
of_higher_or_equal_priority
j_hp
:
=
higher_eq_priority
j_hp
j
.
(** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
(** ...we define the service received during
[
[t1, t2)
]
by jobs of higher or equal priority. *)
Definition
service_of_higher_or_equal_priority_jobs
(
t1
t2
:
instant
)
:
=
service_of_jobs
of_higher_or_equal_priority
jobs
t1
t2
.
...
...
@@ -96,14 +98,14 @@ Section ServiceOfJobs.
(** In this section, we define the notion of workload for sets of jobs. *)
Section
ServiceOfTask
.
(** Let tsk be the task to be analyzed... *)
(** Let
[
tsk
]
be the task to be analyzed... *)
Variable
tsk
:
Task
.
(** ... and let jobs denote any (finite) set of jobs. *)
Variable
jobs
:
seq
Job
.
(** We define the cumulative task service received by
the jobs
from the task within time interval [t1, t2). *)
(** We define the cumulative task service received by
the jobs
from the task within time interval
[
[t1, t2)
]
. *)
Definition
task_service_of_jobs_in
t1
t2
:
=
service_of_jobs
(
job_of_task
tsk
)
jobs
t1
t2
.
...
...
restructuring/model/aggregate/task_arrivals.v
View file @
22a76ba8
...
...
@@ -12,22 +12,24 @@ Section TaskArrivals.
Section
Definitions
.
(** Let tsk be any task. *)
(** Let
[
tsk
]
be any task. *)
Variable
tsk
:
Task
.
(** We define the sequence of jobs of tsk arriving at time t. *)
(** We define the sequence of jobs of t
a
sk
[tsk]
arriving at time t. *)
Definition
task_arrivals_at
(
t
:
instant
)
:
seq
Job
:
=
[
seq
j
<-
arrivals_at
arr_seq
t
|
job_task
j
==
tsk
].
(** By concatenation, we construct the list of jobs of tsk
that arrived in the
interval [t1, t2). *)
(** By concatenation, we construct the list of jobs of t
a
sk
[tsk]
that arrived in the
interval
[
[t1, t2)
]
. *)
Definition
task_arrivals_between
(
t1
t2
:
instant
)
:
=
[
seq
j
<-
arrivals_between
arr_seq
t1
t2
|
job_task
j
==
tsk
].
(** Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
(** Based on that, we define the list of jobs of task [tsk] that
arrived up to time t, ...*)
Definition
task_arrivals_up_to
(
t
:
instant
)
:
=
task_arrivals_between
0
t
.+
1
.
(** ...and the list of jobs of tsk that arrived strictly before time t ... *)
(** ...and the list of jobs of task [tsk] that arrived strictly
before time t ... *)
Definition
task_arrivals_before
(
t
:
instant
)
:
=
task_arrivals_between
0
t
.
(** ... and also count the number of job arrivals. *)
...
...
@@ -36,7 +38,8 @@ Section TaskArrivals.
End
Definitions
.
(** We define a predicate for arrival sequences for which jobs come from a taskset. *)
(** We define a predicate for arrival sequences in which all jobs
come from a given task set. *)
Definition
arrivals_come_from_taskset
(
ts
:
seq
Task
)
:
=
forall
j
,
arrives_in
arr_seq
j
->
job_task
j
\
in
ts
.
...
...
restructuring/model/aggregate/workload.v
View file @
22a76ba8
...
...
@@ -41,7 +41,7 @@ Section WorkloadOfJobs.
higher or equal priority. *)
Variable
higher_eq_priority
:
FP_policy
Task
.
(** Let tsk be the task to be analyzed. *)
(** Let
[
tsk
]
be the task to be analyzed. *)
Variable
tsk
:
Task
.
(** Recall the notion of a job of higher or equal priority. *)
...
...
@@ -49,7 +49,7 @@ Section WorkloadOfJobs.
higher_eq_priority
(
job_task
j
)
tsk
.
(** Then, we define the workload of all jobs of tasks with
higher-or-equal priority than tsk. *)
higher-or-equal priority than t
a
sk
[tsk]
. *)
Definition
workload_of_higher_or_equal_priority_tasks
:
=
workload_of_jobs
of_higher_or_equal_priority
.
...
...
@@ -60,7 +60,7 @@ Section WorkloadOfJobs.
Section
PerJobPriority
.
(** Consider any JLFP policy that indicates whether a job has
higher or equal priority. *)
higher or equal priority. *)
Variable
higher_eq_priority
:
JLFP_policy
Job
.
(** Let j be the job to be analyzed. *)
...
...
@@ -79,16 +79,18 @@ Section WorkloadOfJobs.
(** We also define workload of a task. *)
Section
TaskWorkload
.
(** Let tsk be the task to be analyzed. *)
(** Let
[
tsk
]
be the task to be analyzed. *)
Variable
tsk
:
Task
.
(** We define the task workload as the workload of jobs of task tsk. *)
(** We define the task workload as the workload of jobs of task
[tsk]. *)
Definition
task_workload
jobs
:
=
workload_of_jobs
(
job_of_task
tsk
)
jobs
.
(** Next, we recall the definition of the task workload in interval [t1, t2). *)
(** Next, we recall the definition of the task workload in
interval [[t1, t2)]. *)
Definition
task_workload_between
(
t1
t2
:
instant
)
:
=
task_workload
(
arrivals_between
arr_seq
t1
t2
).
End
TaskWorkload
.
End
WorkloadOfJobs
.
\ No newline at end of file
End
WorkloadOfJobs
.
restructuring/model/arrival/arrival_curves.v
View file @
22a76ba8
Require
Export
rt
.
util
.
rel
.
Require
Export
rt
.
restructuring
.
model
.
aggregate
.
task_arrivals
.
(** In this section, we define the notion of arrival curves, which
can
be used to reason about the frequency of job arrivals. *)
(** In this section, we define the notion of arrival curves, which
can
be used to reason about the frequency of job arrivals. *)
Section
ArrivalCurves
.
(** Consider any type of tasks ... *)
...
...
@@ -18,15 +18,17 @@ Section ArrivalCurves.
(** First, we define what constitutes an arrival bound for a task. *)
Section
ArrivalCurves
.
(** We say that num_arrivals is a valid arrival curve for task
tsk iff
[num_arrivals] is a monotonic function that equals 0
for the empty
interval delta = 0. *)
(** We say that
[
num_arrivals
]
is a valid arrival curve for task
[tsk] iff
[num_arrivals] is a monotonic function that equals 0
for the empty
interval
[
delta = 0
]
. *)
Definition
valid_arrival_curve
(
tsk
:
Task
)
(
num_arrivals
:
duration
->
nat
)
:
=
num_arrivals
0
=
0
/\
monotone
num_arrivals
leq
.
(** We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
[max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
(** We say that [max_arrivals] is an upper arrival bound for task
[tsk] iff, for any interval [[t1, t2)], [max_arrivals (t2 -
t1)] bounds the number of jobs of [tsk] that arrive in that
interval. *)
Definition
respects_max_arrivals
(
tsk
:
Task
)
(
max_arrivals
:
duration
->
nat
)
:
=
forall
(
t1
t2
:
instant
),
t1
<=
t2
->
...
...
@@ -42,15 +44,16 @@ Section ArrivalCurves.
Section
SeparationBound
.
(** Then, we say that min_separation is a lower separation bound iff, for any number of jobs
of tsk, min_separation lower-bounds the minimum interval length in which that number
of jobs can be spawned. *)
(** Then, we say that [min_separation] is a lower separation bound
iff, for any number of jobs of task [tsk], [min_separation]
lower-bounds the minimum interval length in which that number
of jobs can be spawned. *)
Definition
respects_min_separation
(
tsk
:
Task
)
(
min_separation
:
nat
->
duration
)
:
=
forall
t1
t2
,
t1
<=
t2
->
min_separation
(
number_of_task_arrivals
arr_seq
tsk
t1
t2
)
<=
t2
-
t1
.
(** We define in the same way upper separation bounds *)
(** We define in the same way upper separation bounds
.
*)
Definition
respects_max_separation
(
tsk
:
Task
)
(
max_separation
:
nat
->
duration
)
:
=
forall
t1
t2
,
t1
<=
t2
->
...
...
@@ -87,16 +90,17 @@ Section ArrivalCurvesModel.
`
{
MaxSeparation
Task
}
`
{
MinSeparation
Task
}.
(** Let ts be an arbitrary task set. *)
(** Let
[
ts
]
be an arbitrary task set. *)
Variable
ts
:
seq
Task
.
(** We say that arrivals is a valid arrival curve for a taskset
if it is valid for any task
in the taskset *)
(** We say that
[
arrivals
]
is a valid arrival curve for a task
set
if it is valid for any task
in the task
set *)
Definition
valid_taskset_arrival_curve
(
arrivals
:
Task
->
duration
->
nat
)
:
=
forall
(
tsk
:
Task
),
tsk
\
in
ts
->
valid_arrival_curve
tsk
(
arrivals
tsk
).
(** We say that max_arrivals is an arrival bound for taskset ts *)
(** iff max_arrival is an arrival bound for any task from ts. *)
(** We say that [max_arrivals] is an arrival bound for a task set
[ts] iff [max_arrivals] is an arrival bound for any task in
[ts]. *)
Definition
taskset_respects_max_arrivals
:
=
forall
(
tsk
:
Task
),
tsk
\
in
ts
->
respects_max_arrivals
arr_seq
tsk
(
max_arrivals
tsk
).
...
...
restructuring/model/preemption/fully_preemptive.v
View file @
22a76ba8
Require
Export
rt
.
restructuring
.
model
.
preemption
.
parameter
.
(** *
Platform for
Fully Premptive Model *)
(** * Fully Pre
e
mptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
preemptive model. *)
Section
FullyPreemptiveModel
.
...
...
restructuring/model/preemption/parameter.v
View file @
22a76ba8
...
...
@@ -76,8 +76,8 @@ Section MaxAndLastNonpreemptiveSegment.
End
MaxAndLastNonpreemptiveSegment
.
(** * Platform with limited preemptions *)
(** In the foll
w
oing, we define properties that any reasonable job
preemption
model must satisfy. *)
(** In the follo
w
ing, we define properties that any reasonable job
preemption
model must satisfy. *)
Section
PreemptionModel
.
(** Consider any type of jobs... *)
...
...
restructuring/model/priority/classes.v
View file @
22a76ba8
...
...
@@ -86,7 +86,7 @@ Section Priorities.
(** Consider any FP policy. *)
Context
`
{
FP_policy
Task
}.
(** We define whether the policy is antisymmetric over a taskset ts. *)
(** We define whether the policy is antisymmetric over a task
set
[
ts
]
. *)
Definition
antisymmetric_over_taskset
(
ts
:
seq
Task
)
:
=
antisymmetric_over_list
hep_task
ts
.
...
...
restructuring/model/readiness/basic.v
View file @
22a76ba8
...
...
@@ -12,7 +12,7 @@ Section LiuAndLaylandReadiness.
Context
{
PState
:
Type
}.
Context
`
{
ProcessorState
Job
PState
}.
(** Supose jobs have an arrival time and a cost. *)
(** Sup
p
ose jobs have an arrival time and a cost. *)
Context
`
{
JobArrival
Job
}
`
{
JobCost
Job
}.
(** In the basic Liu & Layland model, a job is ready iff it is pending. *)
...
...
restructuring/model/readiness/jitter.v
View file @
22a76ba8
...
...
@@ -17,7 +17,7 @@ Section ReadinessOfJitteryJobs.
Context
{
PState
:
Type
}.
Context
`
{
ProcessorState
Job
PState
}.
(** Supose jobs have an arrival time, a cost, and a release jitter bound. *)
(** Sup
p
ose jobs have an arrival time, a cost, and a release jitter bound. *)
Context
`
{
JobArrival
Job
}
`
{
JobCost
Job
}
`
{
JobJitter
Job
}.
(** We say that a job is released at a time after its arrival if the job's
...
...
restructuring/model/schedule/work_conserving.v
View file @
22a76ba8
Require
Export
rt
.
restructuring
.
behavior
.
all
.
(** In this file, we introduce a restrictive definition of work conserving
uniprocessor schedules. The definition is restrictive because it does not
allow for effects such as jitter or self-suspensions that affect whether a
job can be scheduled at a given point in time. A more general notion of work
conservation that is "readiness-aware", as well as a variant that covers
global scheduling, is TBD. *)
(** In this file, we introduce a restrictive definition of work
conserving schedules. The definition is restrictive because it
does not yet cover multiprocessor scheduling (there are plans to
address this in future work). The definition does however cover
effects such as jitter or self-suspensions that affect whether a
job can be scheduled at a given point in time because it is based
on the general notion of a job being [backlogged] (i.e., ready and
not executing), which is parametric in any given job readiness
model. *)
Section
WorkConserving
.
(** Consider any type of job associated with any type of tasks... *)
...
...
restructuring/model/task/concept.v
View file @
22a76ba8
...
...
@@ -20,10 +20,12 @@ Section SameTask.
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, ... *)
(** ... 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
)
:
=
job_task
j1
==
job_task
j2
.
(** ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
(** ... we also say that job [j] is a job of task [tsk] iff
[job_task j] is equal to [tsk]. *)
Definition
job_of_task
(
tsk
:
Task
)
(
j
:
Job
)
:
=
job_task
j
==
tsk
.
End
SameTask
.
...
...
@@ -36,7 +38,7 @@ Section PropertesOfTask.
Context
`
{
TaskCost
Task
}.
Context
`
{
TaskDeadline
Task
}.
(** Next we intr
d
oduce attributes of a valid sporadic task. *)
(** Next we introduce attributes of a valid sporadic task. *)
Section
ValidTask
.
(** Consider an arbitrary task. *)
...
...
@@ -115,7 +117,7 @@ Section PropertesOfTaskSet.
tsk
\
in
ts
->
task_cost_positive
tsk
.
(** All jobs in the arrival sequence come from the taskset. *)
(** All jobs in the arrival sequence come from the task
set. *)
Definition
all_jobs_from_taskset
:
=
forall
j
,
arrives_in
arr_seq
j
->
...
...
restructuring/model/task/preemption/floating_nonpreemptive.v
View file @
22a76ba8
...
...
@@ -23,7 +23,7 @@ Section ModelWithFloatingNonpreemptiveRegions.
Variable
arr_seq
:
arrival_sequence
Job
.
(** We require [task_max_nonpreemptive_segment (job_task j)] to be
an upper bound of the leng
h
t of the max nonpreemptive segment of
an upper bound of the lengt
h
of the max nonpreemptive segment of
job [j]. *)
Definition
job_max_np_segment_le_task_max_np_segment
:
=
forall
(
j
:
Job
),
...
...
restructuring/model/task/preemption/limited_preemptive.v
View file @
22a76ba8
...
...
@@ -37,7 +37,7 @@ Section ModelWithFixedPreemptionPoints.
forall
tsk
,
tsk
\
in
ts
->
last0
(
task_preemption_points
tsk
)
=
task_cost
tsk
.
(** (3) We require the sequence of preemption points
to be a nondecreasing sequence. *)
to be a non
-
decreasing sequence. *)
Definition
task_preemption_points_is_nondecreasing_sequence
:
=
forall
tsk
,
tsk
\
in
ts
->
nondecreasing_sequence
(
task_preemption_points
tsk
).
...
...
@@ -51,7 +51,7 @@ Section ModelWithFixedPreemptionPoints.
size
(
job_preemption_points
j
)
=
size
(
task_preemption_points
(
job_task
j
)).
(** (5) We require lengths of nonpreemptive segments of a job to be bounded
by leng
h
ts of the corresponding segments of its task. *)
by lengt
h
s of the corresponding segments of its task. *)
Definition
lengths_of_task_segments_bound_length_of_job_segments
:
=
forall
j
n
,
arrives_in
arr_seq
j
->
...
...
restructuring/model/task/preemption/parameters.v
View file @
22a76ba8
...
...
@@ -3,7 +3,7 @@ Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
(** Definition of a generic type of parameter relating a task
to the length of the maximum nonpreeptive segment. *)
to the length of the maximum nonpree
m
ptive segment. *)
Class
TaskMaxNonpreemptiveSegment
(
Task
:
TaskType
)
:
=
task_max_nonpreemptive_segment
:
Task
->
work
.
...
...
@@ -98,7 +98,7 @@ Section PreemptionModel.
bounded length. I.e., for any progress [ρ] of job [j] there
exists a preemption point [pp] such that [ρ <= pp <= ρ +
(job_max_nps j - ε)]. That is, in any time interval of length
[job_max_nps j], there exists a pree
e
mption point which lies
[job_max_nps j], there exists a preemption point which lies
in this interval. *)
Definition
nonpreemptive_regions_have_bounded_length
(
j
:
Job
)
:
=
forall
(
ρ
:
duration
),
...
...
@@ -148,7 +148,7 @@ Section ValidTaskRunToCompletionThreshold.
Context
`
{
JobCost
Job
}.
(** In addition, we assume existence of a function
maping jobs to theirs preemption points ... *)
map
p
ing jobs to theirs preemption points ... *)
Context
`
{
JobPreemptable
Job
}.
(** ...and a function mapping tasks to theirs
...
...
@@ -169,10 +169,10 @@ Section ValidTaskRunToCompletionThreshold.
Definition
task_run_to_completion_threshold_le_task_cost
tsk
:
=
task_run_to_completion_threshold
tsk
<=
task_cost
tsk
.
(** We say that the run-to-completion threshold of a task tsk
bounds
the job run-to-completionthreshold iff for any job
j of task tsk
the job run-to-completion threshold is less than
or equal to the
task run-to-completion threshold. *)
(** We say that the run-to-completion threshold of a task
[
tsk
]
bounds
the job run-to-completion
threshold iff for any job
[j]
of task [tsk]
the job
's
run-to-completion threshold is less than
or equal to the
task
's
run-to-completion threshold. *)
Definition
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
tsk
:
=
forall
j
,
arrives_in
arr_seq
j
->
...
...
@@ -180,11 +180,11 @@ Section ValidTaskRunToCompletionThreshold.
job_run_to_completion_threshold
j
<=
task_run_to_completion_threshold
tsk
.
(** We say that task_run_to_completion_threshold is a valid task
run-to-completion threshold for a task tsk iff
run-to-completion threshold for a task
[
tsk
]
iff
[task_run_to_completion_threshold tsk] is (1) no bigger than
tsk's cost, (2) for any job of task tsk
job_run_to_completion_threshold is bounded by
task_run_to_completion_threshold. *)
[
tsk
]
's cost, (2) for any job of task
[
tsk
]
[
job_run_to_completion_threshold
]
is bounded by
[
task_run_to_completion_threshold
]
. *)
Definition
valid_task_run_to_completion_threshold
tsk
:
=
task_run_to_completion_threshold_le_task_cost
tsk
/\
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
tsk
.
...
...
scripts/wordlist.pws
View file @
22a76ba8
...
...
@@ -22,6 +22,7 @@ namespace
nonpreemptive
preemptive
preemptable
preemptions
EDF
FP
JLFP
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment