Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
14
Issues
14
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
RTPROOFS
PROSA  Formally Proven Schedulability Analysis
Commits
72f608f3
Commit
72f608f3
authored
Oct 15, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
convert comments in behavior module
parent
81dcfa38
Pipeline
#20324
passed with stages
in 3 minutes and 39 seconds
Changes
6
Pipelines
2
Hide whitespace changes
Inline
Sidebyside
Showing
6 changed files
with
63 additions
and
63 deletions
+63
63
arrival_sequence.v
restructuring/behavior/arrival_sequence.v
+27
27
job.v
restructuring/behavior/job.v
+5
5
ready.v
restructuring/behavior/ready.v
+14
14
schedule.v
restructuring/behavior/schedule.v
+5
5
service.v
restructuring/behavior/service.v
+11
11
time.v
restructuring/behavior/time.v
+1
1
No files found.
restructuring/behavior/arrival_sequence.v
View file @
72f608f3
...
...
@@ 2,110 +2,110 @@ From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
From
rt
.
restructuring
.
behavior
Require
Export
time
job
.
From
rt
.
util
Require
Import
notation
.
(* Definitions and properties of job arrival sequences. *)
(*
*
Definitions and properties of job arrival sequences. *)
(* We begin by defining a job arrival sequence. *)
(*
*
We begin by defining a job arrival sequence. *)
Section
ArrivalSequence
.
(* Given any job type with decidable equality, ... *)
(*
*
Given any job type with decidable equality, ... *)
Variable
Job
:
JobType
.
(* ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
(*
*
..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
Definition
arrival_sequence
:=
instant
>
seq
Job
.
End
ArrivalSequence
.
(* Next, we define properties of jobs in a given arrival sequence. *)
(*
*
Next, we define properties of jobs in a given arrival sequence. *)
Section
JobProperties
.
(* Consider any job arrival sequence. *)
(*
*
Consider any job arrival sequence. *)
Context
{
Job
:
JobType
}.
Variable
arr_seq
:
arrival_sequence
Job
.
(* First, we define the sequence of jobs arriving at time t. *)
(*
*
First, we define the sequence of jobs arriving at time t. *)
Definition
arrivals_at
(
t
:
instant
)
:=
arr_seq
t
.
(* Next, we say that job j arrives at a given time t iff it belongs to the
(*
*
Next, we say that job j arrives at a given time t iff it belongs to the
corresponding sequence. *)
Definition
arrives_at
(
j
:
Job
)
(
t
:
instant
)
:=
j
\
in
arrivals_at
t
.
(* Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
(*
*
Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
whether it belongs to the arrival sequence. *)
Definition
arrives_in
(
j
:
Job
)
:=
exists
t
,
j
\
in
arrivals_at
t
.
End
JobProperties
.
(* Next, we define valid arrival sequences. *)
(*
*
Next, we define valid arrival sequences. *)
Section
ValidArrivalSequence
.
(* Assume that job arrival times are known. *)
(*
*
Assume that job arrival times are known. *)
Context
{
Job
:
JobType
}.
Context
`
{
JobArrival
Job
}.
(* Consider any job arrival sequence. *)
(*
*
Consider any job arrival sequence. *)
Variable
arr_seq
:
arrival_sequence
Job
.
(* We say that arrival times are consistent if any job that arrives in the
(*
*
We say that arrival times are consistent if any job that arrives in the
sequence has the corresponding arrival time. *)
Definition
consistent_arrival_times
:=
forall
j
t
,
arrives_at
arr_seq
j
t
>
job_arrival
j
=
t
.
(* We say that the arrival sequence is a set iff it doesn't contain duplicate
(*
*
We say that the arrival sequence is a set iff it doesn't contain duplicate
jobs at any given time. *)
Definition
arrival_sequence_uniq
:=
forall
t
,
uniq
(
arrivals_at
arr_seq
t
).
(* We say that the arrival sequence is valid iff it is a set and arrival times
(*
*
We say that the arrival sequence is valid iff it is a set and arrival times
are consistent *)
Definition
valid_arrival_sequence
:=
consistent_arrival_times
/\
arrival_sequence_uniq
.
End
ValidArrivalSequence
.
(* Next, we define properties of job arrival times. *)
(*
*
Next, we define properties of job arrival times. *)
Section
ArrivalTimeProperties
.
(* Assume that job arrival times are known. *)
(*
*
Assume that job arrival times are known. *)
Context
{
Job
:
JobType
}.
Context
`
{
JobArrival
Job
}.
(* Let j be any job. *)
(*
*
Let j be any job. *)
Variable
j
:
Job
.
(* We say that job j has arrived at time t iff it arrives at some time t_0
(*
*
We say that job j has arrived at time t iff it arrives at some time t_0
with t_0 <= t. *)
Definition
has_arrived
(
t
:
instant
)
:=
job_arrival
j
<=
t
.
(* Next, we say that job j arrived before t iff it arrives at some time t_0
(*
*
Next, we say that job j arrived before t iff it arrives at some time t_0
with t_0 < t. *)
Definition
arrived_before
(
t
:
instant
)
:=
job_arrival
j
<
t
.
(* Finally, we say that job j arrives between t1 and t2 iff it arrives at
(*
*
Finally, we say that job j arrives between t1 and t2 iff it arrives at
some time t with t1 <= t < t2. *)
Definition
arrived_between
(
t1
t2
:
instant
)
:=
t1
<=
job_arrival
j
<
t2
.
End
ArrivalTimeProperties
.
(* In this section, we define arrival sequence prefixes, which are useful to
(*
*
In this section, we define arrival sequence prefixes, which are useful to
define (computable) properties over sets of jobs in the schedule. *)
Section
ArrivalSequencePrefix
.
(* Assume that job arrival times are known. *)
(*
*
Assume that job arrival times are known. *)
Context
{
Job
:
JobType
}.
Context
`
{
JobArrival
Job
}.
(* Consider any job arrival sequence. *)
(*
*
Consider any job arrival sequence. *)
Variable
arr_seq
:
arrival_sequence
Job
.
(* By concatenation, we construct the list of jobs that arrived in the
(*
*
By concatenation, we construct the list of jobs that arrived in the
interval [t1, t2). *)
Definition
arrivals_between
(
t1
t2
:
instant
)
:=
\
cat_
(
t1
<=
t
<
t2
)
arrivals_at
arr_seq
t
.
(* Based on that, we define the list of jobs that arrived up to time t, ...*)
(*
*
Based on that, we define the list of jobs that arrived up to time t, ...*)
Definition
arrivals_up_to
(
t
:
instant
)
:=
arrivals_between
0
t
.+
1
.
(* ...and the list of jobs that arrived strictly before time t. *)
(*
*
...and the list of jobs that arrived strictly before time t. *)
Definition
arrivals_before
(
t
:
instant
)
:=
arrivals_between
0
t
.
End
ArrivalSequencePrefix
.
restructuring/behavior/job.v
View file @
72f608f3
From
rt
.
restructuring
.
behavior
Require
Export
time
.
From
mathcomp
Require
Export
eqtype
ssrnat
.
(* Throughout the library we assume that jobs have decidable equality. *)
(*
*
Throughout the library we assume that jobs have decidable equality. *)
Definition
JobType
:=
eqType
.
(* We define 'work' to denote the unit of service received or needed. In a
(*
*
We define 'work' to denote the unit of service received or needed. In a
real system, this corresponds to the number of processor cycles. *)
Definition
work
:=
nat
.
(* Definition of a generic type of parameter relating jobs to a discrete cost. *)
(*
*
Definition of a generic type of parameter relating jobs to a discrete cost. *)
Class
JobCost
(
Job
:
JobType
)
:=
job_cost
:
Job
>
work
.
(* Definition of a generic type of parameter for job_arrival. *)
(*
*
Definition of a generic type of parameter for job_arrival. *)
Class
JobArrival
(
Job
:
JobType
)
:=
job_arrival
:
Job
>
instant
.
(* Definition of a generic type of parameter relating jobs to an absolute deadline. *)
(*
*
Definition of a generic type of parameter relating jobs to an absolute deadline. *)
Class
JobDeadline
(
Job
:
JobType
)
:=
job_deadline
:
Job
>
instant
.
restructuring/behavior/ready.v
View file @
72f608f3
...
...
@@ 2,7 +2,7 @@ From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From
rt
.
restructuring
.
behavior
Require
Export
service
.
(* We define a general notion of readiness of a job: a job can be
(*
*
We define a general notion of readiness of a job: a job can be
scheduled only when it is ready. This notion of readiness is a general
concept that is used to model jitter, selfsuspensions, etc. Crucially, we
require that any sensible notion of readiness is a refinement of the notion
...
...
@@ 14,61 +14,61 @@ Class JobReady (Job : JobType) (PState : Type)
any_ready_job_is_pending
:
forall
sched
j
t
,
job_ready
sched
j
t
>
pending
sched
j
t
;
}.
(* Based on the general notion of readiness, we define what it means to be
(*
*
Based on the general notion of readiness, we define what it means to be
backlogged, i.e., ready to run but not executing. *)
Section
Backlogged
.
(* Conside any kinds of jobs and any kind of processor state. *)
(*
*
Conside any kinds of jobs and any kind of processor state. *)
Context
{
Job
:
JobType
}
{
PState
:
Type
}.
Context
`
{
ProcessorState
Job
PState
}.
(* Allow for any notion of readiness. *)
(*
*
Allow for any notion of readiness. *)
Context
`
{
JobReady
Job
PState
}.
(* Job j is backlogged at time t iff it is ready and not scheduled. *)
(*
*
Job j is backlogged at time t iff it is ready and not scheduled. *)
Definition
backlogged
(
sched
:
schedule
PState
)
(
j
:
Job
)
(
t
:
instant
)
:=
job_ready
sched
j
t
&&
~~
scheduled_at
sched
j
t
.
End
Backlogged
.
(* With the readiness concept in place, we define the notion of valid schedules. *)
(*
*
With the readiness concept in place, we define the notion of valid schedules. *)
Section
ValidSchedule
.
(* Consider any kinds of jobs and any kind of processor state. *)
(*
*
Consider any kinds of jobs and any kind of processor state. *)
Context
{
Job
:
JobType
}
{
PState
:
Type
}.
Context
`
{
ProcessorState
Job
PState
}.
(* Consider any schedule. *)
(*
*
Consider any schedule. *)
Variable
sched
:
schedule
PState
.
Context
`
{
JobArrival
Job
}.
(* We define whether jobs come from some arrival sequence... *)
(*
*
We define whether jobs come from some arrival sequence... *)
Definition
jobs_come_from_arrival_sequence
(
arr_seq
:
arrival_sequence
Job
)
:=
forall
j
t
,
scheduled_at
sched
j
t
>
arrives_in
arr_seq
j
.
(* ..., whether a job can only be scheduled if it has arrived ... *)
(*
*
..., whether a job can only be scheduled if it has arrived ... *)
Definition
jobs_must_arrive_to_execute
:=
forall
j
t
,
scheduled_at
sched
j
t
>
has_arrived
j
t
.
Context
`
{
JobCost
Job
}.
Context
`
{
JobReady
Job
PState
}.
(* ..., whether a job can only be scheduled if it is ready ... *)
(*
*
..., whether a job can only be scheduled if it is ready ... *)
Definition
jobs_must_be_ready_to_execute
:=
forall
j
t
,
scheduled_at
sched
j
t
>
job_ready
sched
j
t
.
(* ... and whether a job cannot be scheduled after it completes. *)
(*
*
... and whether a job cannot be scheduled after it completes. *)
Definition
completed_jobs_dont_execute
:=
forall
j
t
,
scheduled_at
sched
j
t
>
service
sched
j
t
<
job_cost
j
.
(* We say that the schedule is valid iff
(*
*
We say that the schedule is valid iff
 jobs come from some arrival sequence
 a job is scheduled if it is ready *)
Definition
valid_schedule
(
arr_seq
:
arrival_sequence
Job
)
:=
jobs_come_from_arrival_sequence
arr_seq
/\
jobs_must_be_ready_to_execute
.
(* Note that we do not explicitly require that a valid schedule satisfies
(*
*
Note that we do not explicitly require that a valid schedule satisfies
jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
properties are implied by jobs_must_be_ready_to_execute. *)
...
...
restructuring/behavior/schedule.v
View file @
72f608f3
From
mathcomp
Require
Export
ssreflect
ssrnat
ssrbool
eqtype
fintype
bigop
.
From
rt
.
restructuring
.
behavior
Require
Export
arrival_sequence
.
(* We define the notion of a generic processor state. The processor state type
(*
*
We define the notion of a generic processor state. The processor state type
determines aspects of the execution environment are modeled (e.g., overheads, spinning).
In the most simple case (i.e., Ideal.processor_state), at any time,
either a particular job is either scheduled or it is idle. *)
Class
ProcessorState
(
Job
:
JobType
)
(
State
:
Type
)
:=
{
(* For a given processor state, the [scheduled_in] predicate checks whether a given
(*
*
For a given processor state, the [scheduled_in] predicate checks whether a given
job is running in that state. *)
scheduled_in
:
Job
>
State
>
bool
;
(* For a given processor state, the [service_in] function determines how much
(*
*
For a given processor state, the [service_in] function determines how much
service a given job receives in that state. *)
service_in
:
Job
>
State
>
work
;
(* For a given processor state, a job does not receive service if it is not scheduled
(*
*
For a given processor state, a job does not receive service if it is not scheduled
in that state *)
service_implies_scheduled
:
forall
j
s
,
~~
scheduled_in
j
s
>
service_in
j
s
=
0
}.
(* A schedule maps an instant to a processor state *)
(*
*
A schedule maps an instant to a processor state *)
Definition
schedule
(
PState
:
Type
)
:=
instant
>
PState
.
restructuring/behavior/service.v
View file @
72f608f3
...
...
@@ 7,19 +7,19 @@ Section Service.
Variable
sched
:
schedule
PState
.
(* First, we define whether a job j is scheduled at time t, ... *)
(*
*
First, we define whether a job j is scheduled at time t, ... *)
Definition
scheduled_at
(
j
:
Job
)
(
t
:
instant
)
:=
scheduled_in
j
(
sched
t
).
(* ... and the instantaneous service received by
(*
*
... and the instantaneous service received by
job j at time t. *)
Definition
service_at
(
j
:
Job
)
(
t
:
instant
)
:=
service_in
j
(
sched
t
).
(* Based on the notion of instantaneous service, we define the
(*
*
Based on the notion of instantaneous service, we define the
cumulative service received by job j during any interval [t1, t2). *)
Definition
service_during
(
j
:
Job
)
(
t1
t2
:
instant
)
:=
\
sum_
(
t1
<=
t
<
t2
)
service_at
j
t
.
(* Using the previous definition, we define the cumulative service
(*
*
Using the previous definition, we define the cumulative service
received by job j up to time t, i.e., during interval [0, t). *)
Definition
service
(
j
:
Job
)
(
t
:
instant
)
:=
service_during
j
0
t
.
...
...
@@ 27,32 +27,32 @@ Section Service.
Context
`
{
JobDeadline
Job
}.
Context
`
{
JobArrival
Job
}.
(* Next, we say that job j has completed by time t if it received enough
(*
*
Next, we say that job j has completed by time t if it received enough
service in the interval [0, t). *)
Definition
completed_by
(
j
:
Job
)
(
t
:
instant
)
:=
service
j
t
>=
job_cost
j
.
(* We say that job j completes at time t if it has completed by time t but
(*
*
We say that job j completes at time t if it has completed by time t but
not by time t  1 *)
Definition
completes_at
(
j
:
Job
)
(
t
:
instant
)
:=
~~
completed_by
j
t
.
1
&&
completed_by
j
t
.
(* We say that R is a response time bound of a job j if j has completed
(*
*
We say that R is a response time bound of a job j if j has completed
by R units after its arrival *)
Definition
job_response_time_bound
(
j
:
Job
)
(
R
:
duration
)
:=
completed_by
j
(
job_arrival
j
+
R
).
(* We say that a job meets its deadline if it completes by its absolute deadline *)
(*
*
We say that a job meets its deadline if it completes by its absolute deadline *)
Definition
job_meets_deadline
(
j
:
Job
)
:=
completed_by
j
(
job_deadline
j
).
(* Job j is pending at time t iff it has arrived but has not yet completed. *)
(*
*
Job j is pending at time t iff it has arrived but has not yet completed. *)
Definition
pending
(
j
:
Job
)
(
t
:
instant
)
:=
has_arrived
j
t
&&
~~
completed_by
j
t
.
(* Job j is pending earlier and at time t iff it has arrived before time t
(*
*
Job j is pending earlier and at time t iff it has arrived before time t
and has not been completed yet. *)
Definition
pending_earlier_and_at
(
j
:
Job
)
(
t
:
instant
)
:=
arrived_before
j
t
&&
~~
completed_by
j
t
.
(* Let's define the remaining cost of job j as the amount of service
(*
*
Let's define the remaining cost of job j as the amount of service
that has to be received for its completion. *)
Definition
remaining_cost
j
t
:=
job_cost
j

service
j
t
.
...
...
restructuring/behavior/time.v
View file @
72f608f3
(* Time is defined as a natural number. *)
(*
*
Time is defined as a natural number. *)
Definition
duration
:=
nat
.
Definition
instant
:=
nat
.
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