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
ce01dfe1
Commit
ce01dfe1
authored
Dec 02, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
address spell-checker complaints in behavior module
parent
085ea530
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
6 additions
and
6 deletions
+6
-6
restructuring/behavior/ready.v
restructuring/behavior/ready.v
+2
-2
restructuring/behavior/schedule.v
restructuring/behavior/schedule.v
+1
-1
restructuring/behavior/time.v
restructuring/behavior/time.v
+3
-3
No files found.
restructuring/behavior/ready.v
View file @
ce01dfe1
...
...
@@ -25,7 +25,7 @@ Class JobReady (Job : JobType) (PState : Type)
(** 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
r
any kinds of jobs and any kind of processor state. *)
Context
{
Job
:
JobType
}
{
PState
:
Type
}.
Context
`
{
ProcessorState
Job
PState
}.
...
...
@@ -79,7 +79,7 @@ Section ValidSchedule.
jobs_must_be_ready_to_execute
.
(** Note that we do not explicitly require that a valid schedule satisfies
jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
[
jobs_must_arrive_to_execute
]
or
[
completed_jobs_dont_execute
]
because these
properties are implied by jobs_must_be_ready_to_execute. *)
End
ValidSchedule
.
restructuring/behavior/schedule.v
View file @
ce01dfe1
...
...
@@ -6,7 +6,7 @@ Require Export rt.restructuring.behavior.arrival_sequence.
(** Rather than choosing a specific schedule representation up front, we define
the notion of a generic processor state, which allows us to state general
definitions of core concepts (such as "how much service has a job
received") that work across many possble scenarios (e.g., ideal
received") that work across many poss
i
ble scenarios (e.g., ideal
uniprocessor schedules, schedules with overheads, variable-speed
processors, multiprocessors, etc.).
...
...
restructuring/behavior/time.v
View file @
ce01dfe1
(** * Model of Time *)
(** Prosa is based on a discrete model of time. Thus, time is simply defined by
the natural numbers. To aid readability, we distinguish between
time
values
that represent duration
s
and
time
values that represent specific
instant
s
. *)
the natural numbers. To aid readability, we distinguish between values
of time
that represent
a
duration and values
of time
that represent
a
specific
instant. *)
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