Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
K
klee_tutorial
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Edvin Åkerfeldt
klee_tutorial
Commits
5b12942e
Commit
5b12942e
authored
4 years ago
by
Edvin Åkerfeldt
Browse files
Options
Downloads
Patches
Plain Diff
cli done
parent
73d4b319
No related branches found
No related tags found
No related merge requests found
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
srp_analysis/src/aux.rs
+7
-3
7 additions, 3 deletions
srp_analysis/src/aux.rs
srp_analysis/src/main.rs
+239
-92
239 additions, 92 deletions
srp_analysis/src/main.rs
with
246 additions
and
95 deletions
srp_analysis/src/aux.rs
+
7
−
3
View file @
5b12942e
...
@@ -11,6 +11,10 @@ pub struct TaskTimes {
...
@@ -11,6 +11,10 @@ pub struct TaskTimes {
pub
i
:
u32
// Preumtion time
pub
i
:
u32
// Preumtion time
}
}
pub
fn
task_load
(
task
:
&
Task
)
->
f32
{
return
task
.get_wcet
()
as
f32
/
task
.inter_arrival
as
f32
;
}
/// Returns the total load factor, L(t) = C(t) / A(t) (Where C(t) is WCET and A(t) is the inter-arrival time of the task).
/// Returns the total load factor, L(t) = C(t) / A(t) (Where C(t) is WCET and A(t) is the inter-arrival time of the task).
///
///
/// See: https://gitlab.henriktjader.com/pln/klee_tutorial/-/blob/master/HOME_EXAM.md#L85
/// See: https://gitlab.henriktjader.com/pln/klee_tutorial/-/blob/master/HOME_EXAM.md#L85
...
@@ -22,7 +26,7 @@ pub struct TaskTimes {
...
@@ -22,7 +26,7 @@ pub struct TaskTimes {
pub
fn
total_cpu_load
(
tasks
:
&
Vec
<
Task
>
)
->
f32
{
pub
fn
total_cpu_load
(
tasks
:
&
Vec
<
Task
>
)
->
f32
{
let
mut
total_l
:
f32
=
0.0
;
let
mut
total_l
:
f32
=
0.0
;
for
task
in
tasks
{
for
task
in
tasks
{
total_l
+=
task
.get_wcet
()
as
f32
/
task
.inter_arrival
as
f32
;
total_l
+=
task
_load
(
&
task
)
;
}
}
return
total_l
;
return
total_l
;
}
}
...
@@ -150,7 +154,7 @@ pub fn preemption_time(task: &Task, task_set: &Tasks, bp_approx: bool) -> Result
...
@@ -150,7 +154,7 @@ pub fn preemption_time(task: &Task, task_set: &Tasks, bp_approx: bool) -> Result
let
wcet
=
task
.get_wcet
();
let
wcet
=
task
.get_wcet
();
let
block_t
=
blocking_time
(
&
task
,
&
task_set
);
let
block_t
=
blocking_time
(
&
task
,
&
task_set
);
// Give us the first estimate
// Give us the first estimate
(initial condition)
let
mut
r_estimate
=
wcet
+
block_t
;
let
mut
r_estimate
=
wcet
+
block_t
;
loop
{
loop
{
...
@@ -159,7 +163,7 @@ pub fn preemption_time(task: &Task, task_set: &Tasks, bp_approx: bool) -> Result
...
@@ -159,7 +163,7 @@ pub fn preemption_time(task: &Task, task_set: &Tasks, bp_approx: bool) -> Result
if
prev_r_est
>
task
.deadline
{
if
prev_r_est
>
task
.deadline
{
// Our busy period is deviating, break it of
// Our busy period is deviating, break it of
return
Err
(
"The
busy period deviated...
."
)
return
Err
(
"The
task is not scheduable given the current task set
."
)
}
}
let
mut
preemp_t_est
=
0
;
let
mut
preemp_t_est
=
0
;
...
...
This diff is collapsed.
Click to expand it.
srp_analysis/src/main.rs
+
239
−
92
View file @
5b12942e
pub
mod
common
;
pub
mod
common
;
pub
mod
aux
;
pub
mod
aux
;
use
std
::
fs
;
use
std
::
fs
::
File
;
use
std
::
io
::
prelude
::
*
;
use
std
::
path
::
Path
;
use
std
::
path
::
PathBuf
;
use
std
::
path
::
PathBuf
;
use
structopt
::
StructOpt
;
use
structopt
::
StructOpt
;
use
structopt
::
clap
::
arg_enum
;
use
common
::
*
;
use
common
::
*
;
use
aux
::
*
;
use
aux
::
*
;
/*
enum Example {
POSSIBLE,
IMPOSSIBLE
}*/
arg_enum!
{
#[derive(Debug)]
enum
Example
{
POSSIBLE
,
IMPOSSIBLE
}
}
/// A basic example
/// A basic example
#[derive(StructOpt,
Debug)]
#[derive(StructOpt,
Debug)]
#[structopt(name
=
"srp_analysis"
,
about
=
"asdasdasdasd"
)]
#[structopt(name
=
"srp_analysis"
,
about
=
"
Running
cargo run -- --generate_example -o example.json
cargo run -- --approximate -i example.json
cargo run -- --help
"
)]
struct
Opt
{
struct
Opt
{
// A flag, true if used in the command line. Note doc comment will
// A flag, true if used in the command line. Note doc comment will
// be used for the help message of the flag. The name of the
// be used for the help message of the flag. The name of the
...
@@ -18,49 +43,175 @@ struct Opt {
...
@@ -18,49 +43,175 @@ struct Opt {
#[structopt(name
=
"approximate"
,
long)]
#[structopt(name
=
"approximate"
,
long)]
approx_bp
:
bool
,
approx_bp
:
bool
,
// The number of occurrences of the `v/verbose` flag
/// Verbose mode (-v, -vv, -vvv, etc.)
#[structopt(short,
long,
parse(from_occurrences))]
verbose
:
u8
,
/// Generate an example file
/// Generate an example file
#[structopt(long)]
//
#[structopt(long)]
//
generate
:
bool
,
generate
:
bool
,
#[structopt(short
=
"ex"
,
long
=
"example"
,
possible_values
=
&
Example::variants(),
case_insensitive
=
true
,
default_value
=
"possible"
)]
example
:
Example
,
/// Output file for generated example
/// Output file for generated example
#[structopt(short,
long,
parse(from_os_str))]
#[structopt(short,
long,
parse(from_os_str))]
output
:
Option
<
PathBuf
>
,
output
:
Option
<
PathBuf
>
,
///
Out
put file for
generated example
///
In
put file for
for task definition
#[structopt(short,
long,
parse(from_os_str),
required_unless
=
"generate"
)]
#[structopt(short,
long,
parse(from_os_str),
required_unless
=
"generate"
)]
input
:
Option
<
PathBuf
>
,
input
:
Option
<
PathBuf
>
,
}
/*
// Genarate a certain example (schedulable, non-schedulable)
#[structopt(short = "ex", long = "example", default_value = "schedulable")]
example: Example,
*/
fn
main
()
{
let
exit_code
=
real_main
();
std
::
process
::
exit
(
exit_code
);
}
}
fn
real_main
()
->
i32
{
let
opt
=
Opt
::
from_args
();
macro_rules!
verbose_p
{
(
$format:expr
,
$s
:
expr
,
$verbose_lvl
:
expr
)
=>
{
if
opt
.verbose
>=
$verbose_lvl
{
println!
(
$format
,
$s
)
}
}
}
// The number of occurrences of the `v/verbose` flag
verbose_p!
(
"Parameters: {:?}"
,
opt
,
1
);
/// Verbose mode (-v, -vv, -vvv, etc.)
if
opt
.generate
{
//#[structopt(short, long, parse(from_occurrences))]
let
tasks
=
match
opt
.example
{
//verbose: u8,
Example
::
POSSIBLE
=>
{
verbose_p!
(
"{}"
,
"Generating a schedulable task set"
,
1
);
schedulable_task_set
()
},
Example
::
IMPOSSIBLE
=>
{
verbose_p!
(
"{}"
,
"Generating a non-schedulable task set"
,
1
);
non_schedulable_task_set
()
}
};
// Convert the task vector to a JSON string.
let
serialized
=
serde_json
::
to_string
(
&
tasks
)
.unwrap
();
/// Set speed
if
let
Some
(
output_file
)
=
opt
.output
{
//#[structopt(short, long, default_value = "42")]
let
path
=
Path
::
new
(
&
output_file
);
//speed: f64,
let
display
=
path
.display
();
// Code taken from: https://doc.rust-lang.org/rust-by-example/std_misc/file/create.html
// Open a file in write-only mode, returns `io::Result<File>`
let
mut
file
=
match
File
::
create
(
&
path
)
{
Err
(
why
)
=>
panic!
(
"couldn't create {}: {}"
,
display
,
why
),
Ok
(
file
)
=>
file
,
};
// the long option will be translated by default to kebab case,
// Write the serialized data to `file`, returns `io::Result<()>`
// i.e. `--nb-cars`.
match
file
.write_all
(
serialized
.as_bytes
())
{
/// Number of cars
Err
(
why
)
=>
panic!
(
"couldn't write to {}: {}"
,
display
,
why
),
//#[structopt(short = "c", long)]
Ok
(
_
)
=>
println!
(
"successfully wrote example data wrote to: {}"
,
display
),
//nb_cars: Option<i32>,
}
/// admin_level to consider
}
else
{
//#[structopt(short, long)]
println!
(
"{}"
,
serialized
);
//level: Vec<String>,
}
/// Files to process
return
0
;
//#[structopt(name = "FILE", parse(from_os_str))]
}
//files: Vec<PathBuf>,
fn
main
()
{
let
input_file
=
opt
.input
.unwrap
();
// Let it panic, if it has reached this stage and panics we've fucked up our StructOpt config
let
serialized_data
=
fs
::
read_to_string
(
input_file
)
.unwrap
();
let
tasks
:
Tasks
=
serde_json
::
from_str
(
&
serialized_data
)
.unwrap
();
verbose_p!
(
"Data from file: {}"
,
serialized_data
,
2
);
verbose_p!
(
"Parsed data: {:?}"
,
&
tasks
,
3
);
let
(
ip
,
tr
)
=
pre_analysis
(
&
tasks
);
verbose_p!
(
"ip: {:?}"
,
ip
,
1
);
verbose_p!
(
"tr: {:?}"
,
tr
,
1
);
match
opt
.approx_bp
{
false
=>
{
println!
(
"=== Running analysis (realistic) ==="
);
println!
(
"Note: While running without approximation, busy period (Bp(t)) will be computed in relation to all other tasks.
\n
"
);
},
true
=>
{
println!
(
"=== Running analysis (approximation) ==="
);
println!
(
"Note: While running with approximation, busy period (Bp(t)) will be defined as the deadline time (D(t)) of a task.
\n
"
);
}
}
println!
(
"=== Task analysis: results ==="
);
for
t
in
tasks
.iter
()
{
println!
(
"-> {:?}"
,
&
t
.id
);
match
response_time
(
&
t
,
&
tasks
,
opt
.approx_bp
)
{
Ok
(
re
)
=>
println!
(
":: Response time = {:?}"
,
re
),
Err
(
_
)
=>
println!
(
":: Response time = INCONC"
)
}
match
preemption_time
(
&
t
,
&
tasks
,
opt
.approx_bp
)
{
Ok
(
re
)
=>
println!
(
":: Preemption time = {:?}"
,
re
),
Err
(
_
)
=>
println!
(
":: Preemption time = INCONC"
)
}
/*
println!(":: Response time (safe approx) = {:?}", response_time(&t, &tasks, true).unwrap());
println!(":: Preemption time (safe approx) = {:?}", preemption_time(&t, &tasks, true).unwrap());
match response_time(&t, &tasks, false) {
Ok(re) => println!(":: Response time (realistic) = {:?}", re),
Err(_) => println!(":: Response time (realistic) = INCONC")
}
match preemption_time(&t, &tasks, false) {
Ok(re) => println!(":: Preemption time (realistic) = {:?}", re),
Err(_) => println!(":: Preemption time (realistic) = INCONC")
}
*/
println!
(
":: Blocking time = {:?}"
,
blocking_time
(
&
t
,
&
tasks
));
println!
(
":: WCET = {:?}"
,
t
.get_wcet
());
println!
(
""
);
}
verbose_p!
(
"Combined result = {:?}"
,
times_as_vec
(
&
tasks
,
false
),
1
);
println!
(
"=== Schedulability analysis: results ==="
);
println!
(
"-> Loadfactor"
);
for
task
in
&
tasks
{
let
t_load
=
task_load
(
&
task
);
if
t_load
<=
1.0
{
println!
(
"{:?} : {:?} - OK"
,
task
.id
,
t_load
);
}
else
{
println!
(
"{:?} : {:?} - TO HIGH"
,
task
.id
,
t_load
);
}
}
let
l
=
total_cpu_load
(
&
tasks
);
if
l
<=
1.0
{
println!
(
"Total loadfactor: {:?} - OK"
,
l
)
}
else
{
println!
(
"Total loadfactor: {:?} - Task set not schedulable"
,
l
)
}
println!
(
"-> response time, R(t) < D(t) ?"
);
let
mut
inconc
:
Vec
<
String
>
=
vec!
[];
for
task
in
&
tasks
{
match
response_time
(
task
,
&
tasks
,
opt
.approx_bp
)
{
Ok
(
re
)
=>
println!
(
"{:?} : {:?} - OK"
,
task
.id
,
re
),
Err
(
_
)
=>
{
println!
(
"{:?} : INCONC - R(t) >= {:?}"
,
task
.id
,
task
.deadline
);
inconc
.push
(
task
.id
.clone
()
.to_string
());
}
}
}
if
inconc
.len
()
>
0
||
l
>
1.0
{
println!
(
"--> Analysis result: Task set NOT schedulable <--"
);
return
1
;
}
else
{
println!
(
"--> Analysis result: Task set schedulable <--"
);
return
0
;
}
}
fn
schedulable_task_set
()
->
Tasks
{
let
t1
=
Task
{
let
t1
=
Task
{
id
:
"T1"
.to_string
(),
id
:
"T1"
.to_string
(),
prio
:
1
,
prio
:
1
,
...
@@ -123,75 +274,71 @@ fn main() {
...
@@ -123,75 +274,71 @@ fn main() {
},
},
};
};
// builds a vector of tasks t1, t2, t3
return
vec!
[
t1
,
t2
,
t3
];
let
tasks
:
Tasks
=
vec!
[
t1
,
t2
,
t3
];
// Example for running
// cargo run -- --generate_example -o hej.json
// cargo run -- -i hej.json --approximate
// cargo run -- --help
let
opt
=
Opt
::
from_args
();
//println!("{:?}", opt);
if
opt
.generate
{
// Convert the Point to a JSON string.
let
serialized
=
serde_json
::
to_string
(
&
tasks
)
.unwrap
();
// Prints serialized = {"x":1,"y":2}
if
let
Some
(
output_file
)
=
opt
.output
{
println!
(
"Saving example file to: {:?}"
,
output_file
);
}
else
{
println!
(
"{}"
,
serialized
);
}
}
// Convert the JSON string back to a Point.
//let deserialized: [Task; 3] = serde_json::from_str(&serialized).unwrap();
// Prints deserialized = Point { x: 1, y: 2 }
//println!("deserialized = {:?}", deserialized);
return
;
fn
non_schedulable_task_set
()
->
Tasks
{
}
let
t1
=
Task
{
id
:
"T1"
.to_string
(),
//let input_file = opt.input.unwrap(); // Let it panic, if it has reached this stage we've fucked up our StructOpt config
prio
:
1
,
deadline
:
100
,
println!
(
"tasks {:?}"
,
&
tasks
);
inter_arrival
:
100
,
// println!("tot_util {}", tot_util(&tasks));
trace
:
Trace
{
id
:
"T1"
.to_string
(),
let
(
ip
,
tr
)
=
pre_analysis
(
&
tasks
);
start
:
0
,
end
:
10
,
println!
(
"ip: {:?}"
,
ip
);
inner
:
vec!
[],
println!
(
"tr: {:?}"
,
tr
);
},
};
let
_approximate_bp
=
false
;
println!
(
"=== Running analysis ==="
);
for
t
in
tasks
.iter
()
{
println!
(
"-> {:?}"
,
&
t
.id
);
println!
(
":: Response time (safe approx) = {:?}"
,
response_time
(
&
t
,
&
tasks
,
true
)
.unwrap
());
let
t2
=
Task
{
println!
(
":: Preemption time (safe approx) = {:?}"
,
preemption_time
(
&
t
,
&
tasks
,
true
)
.unwrap
());
id
:
"T2"
.to_string
(),
match
response_time
(
&
t
,
&
tasks
,
false
)
{
prio
:
2
,
Ok
(
re
)
=>
println!
(
":: Response time (realistic) = {:?}"
,
re
),
deadline
:
40
,
Err
(
_
)
=>
println!
(
":: Response time (realistic) = INCONC"
)
inter_arrival
:
100
,
}
trace
:
Trace
{
match
preemption_time
(
&
t
,
&
tasks
,
false
)
{
id
:
"T2"
.to_string
(),
Ok
(
re
)
=>
println!
(
":: Preemption time (realistic) = {:?}"
,
re
),
start
:
0
,
Err
(
_
)
=>
println!
(
":: Preemption time (realistic) = INCONC"
)
end
:
30
,
}
inner
:
vec!
[
println!
(
":: Blocking time = {:?}"
,
blocking_time
(
&
t
,
&
tasks
));
Trace
{
println!
(
":: WCET = {:?}"
,
t
.get_wcet
());
id
:
"R1"
.to_string
(),
println!
(
""
);
start
:
10
,
}
end
:
20
,
inner
:
vec!
[
Trace
{
id
:
"R2"
.to_string
(),
start
:
12
,
end
:
16
,
inner
:
vec!
[],
}],
},
Trace
{
id
:
"R1"
.to_string
(),
start
:
22
,
end
:
28
,
inner
:
vec!
[],
},
],
},
};
println!
(
"{:?}"
,
times_as_vec
(
&
tasks
,
false
));
let
t3
=
Task
{
let
l
=
total_cpu_load
(
&
tasks
);
id
:
"T3"
.to_string
(),
if
l
<=
1.0
{
prio
:
3
,
println!
(
"Loadfactor: {:?} - OK"
,
l
)
deadline
:
50
,
}
else
{
inter_arrival
:
50
,
println!
(
"Loadfactor: {:?} - FAILED"
,
l
)
trace
:
Trace
{
}
id
:
"T3"
.to_string
(),
start
:
0
,
end
:
30
,
inner
:
vec!
[
Trace
{
id
:
"R2"
.to_string
(),
start
:
10
,
end
:
20
,
inner
:
vec!
[],
}],
},
};
return
vec!
[
t1
,
t2
,
t3
];
}
}
\ No newline at end of file
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment