Skip to content
Snippets Groups Projects
Commit ee8c1f78 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Add definition of idle cpu

parent cf99d3e5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
ScheduleDefs.v
+ 3
− 0
View file @ ee8c1f78
...@@ -123,6 +123,9 @@ Module Schedule. ...@@ -123,6 +123,9 @@ Module Schedule.
Definition scheduled (t: time) := Definition scheduled (t: time) :=
[exists cpu in 'I_(num_cpus), sched cpu t == Some j]. [exists cpu in 'I_(num_cpus), sched cpu t == Some j].
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
sched cpu t = None.
Definition service_at (t: time) := Definition service_at (t: time) :=
\sum_(cpu < num_cpus | sched cpu t == Some j) rate j cpu. \sum_(cpu < num_cpus | sched cpu t == Some j) rate j cpu.
......
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