Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
C
cortex-m-rtfm-klee
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
Model registry
Operate
Environments
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
KLEE
cortex-m-rtfm-klee
Commits
ee15ce17
"src/parse.rs" did not exist on "7f2de6c9f85fa9978acf16167f90f6427f04635a"
Commit
ee15ce17
authored
Mar 5, 2018
by
Per Lindgren
Browse files
Options
Downloads
Patches
Plain Diff
resource updated
parent
080de7e9
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
examples/resource.rs
+25
-17
25 additions, 17 deletions
examples/resource.rs
with
25 additions
and
17 deletions
examples/resource.rs
+
25
−
17
View file @
ee15ce17
...
@@ -73,7 +73,7 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
...
@@ -73,7 +73,7 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
fn
exti3
(
t
:
&
mut
Threshold
,
mut
r
:
EXTI3
::
Resources
)
{
fn
exti3
(
t
:
&
mut
Threshold
,
mut
r
:
EXTI3
::
Resources
)
{
r
.X
.claim_mut
(
t
,
|
x
,
_
|
{
r
.X
.claim_mut
(
t
,
|
x
,
_
|
{
*
x
+=
1
;
*
x
+=
1
;
})
;
})
}
}
#[inline(never)]
#[inline(never)]
...
@@ -172,6 +172,12 @@ fn idle() -> ! {
...
@@ -172,6 +172,12 @@ fn idle() -> ! {
// The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
// The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
// of each resource. This allows you to monitor the number of clock cyckles using gdb.
// of each resource. This allows you to monitor the number of clock cyckles using gdb.
//
//
// Connect your Nucleo64 board with the `stm32f401re` (or `stm32f411re`) MCU.
// Start openocd in a separate terminal (and let it run there).
//
// > openocd -f interface/stlink.cfg -f target/stm32f4x.cfg
// (You may use `-f inteface/stlink-v2-1.cfg`, if `stlink.cfg` is missing.)
//
// Start gdb.
// Start gdb.
// > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
// > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
//
//
...
@@ -183,15 +189,15 @@ fn idle() -> ! {
...
@@ -183,15 +189,15 @@ fn idle() -> ! {
// tb main
// tb main
// continue
// continue
//
//
// Line by line it
// Line by line
,
it
:
// - connects to the target (the MCU)
// - connects to the target (the MCU)
// - resets the MCU
// - resets the MCU
// - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
// - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
// - sets a temporary breakpoint to `main`
// - sets a temporary breakpoint to `main`
, and
// - continues executing until `main` is reached.
// - continues executing until `main` is reached.
//
//
// At the point the MCU hits `main`
you will be promted to continue working <return> or quit
// At the point the MCU hits `main`
it stops.
// press <return>
//
(You may be promted to continue working <return> or quit, in such case
press <return>
.)
//
//
// Now you can inspect where the processor halted.
// Now you can inspect where the processor halted.
// > (gdb) list
// > (gdb) list
...
@@ -250,16 +256,16 @@ fn idle() -> ! {
...
@@ -250,16 +256,16 @@ fn idle() -> ! {
// 0x08000276 <+14>: bx lr
// 0x08000276 <+14>: bx lr
// End of assembler dump.
// End of assembler dump.
//
//
// Here you go, cannot be simpler that this, it
// Here you go, cannot be simpler that this, it
:
// - sets up the address to X in r0
// - sets up the address to X in r0
// - reads the old value
// - reads the old value
// - adds 1 (wrapping arithmetics)
// - adds 1 (wrapping arithmetics)
// - stores the new value in X
// - stores the new value in X
, and
// - it returns
// - it returns
// (On Cortex M functions and inerrupt handlers are essentially treated the same way)
// (On Cortex M functions and inerrupt handlers are essentially treated the same way)
//
//
// So now you can check the value of X. See above...
// So now you can check the value of X. See above...
//
++
your answer here **
//
**
your answer here **
//
//
// Now let us turn to EXTI2.
// Now let us turn to EXTI2.
// (gdb) mon mww 0xe0001004 0
// (gdb) mon mww 0xe0001004 0
...
@@ -267,7 +273,7 @@ fn idle() -> ! {
...
@@ -267,7 +273,7 @@ fn idle() -> ! {
// (gdb) mon mrw 0xe0001004
// (gdb) mon mrw 0xe0001004
// 13
// 13
//
//
// Also in this case we see that the resource (
Y
) was granted without overhead
// Also in this case we see that the resource (
`Y`
) was granted without overhead
// The code took a few additional clock cycles (its contians a condition, right).
// The code took a few additional clock cycles (its contians a condition, right).
// Figure out which path was triggered by this test.
// Figure out which path was triggered by this test.
// ** your answer here **
// ** your answer here **
...
@@ -303,10 +309,12 @@ fn idle() -> ! {
...
@@ -303,10 +309,12 @@ fn idle() -> ! {
// End of assembler dump.
// End of assembler dump.
//
//
// This one is a bit harder to understand.
// This one is a bit harder to understand.
// What it does essentially is to store -1 in r2
// What it does essentially is:
// and conditionally overwrite the r2 by a 1 if `Y < 10`
// - read `Y` into r1,
// and then add r2 to r1 (the current value of `Y`)
// - store -1 in r2
// and update `Y` to r1.
// - conditionally overwrite the r2 by a 1 if `Y < 10`
// - add r2 to r1 (the value of `Y`),
// - update `Y`.
//
//
// So this is beautiful, the COSTLY branch is replaced by a CHEAP
// So this is beautiful, the COSTLY branch is replaced by a CHEAP
// condtitonal assigmnet `movcc`.
// condtitonal assigmnet `movcc`.
...
@@ -462,11 +470,11 @@ fn idle() -> ! {
...
@@ -462,11 +470,11 @@ fn idle() -> ! {
// At this point you should find that the worst case time stays the same ...
// At this point you should find that the worst case time stays the same ...
//
//
// Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
// Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
// What it does is that it figures out that we actually inc
l
eas
Y
, by the value of
X
.
// What it does is that it figures out that we actually inc
r
eas
e `Y`
, by the value of
`X`
.
// So the loop is all gone, optimized out, and replaced by a simple addition.
// So the loop is all gone, optimized out, and replaced by a simple addition.
//
//
// Now lets look at best case execution time.
// Now lets look at best case execution time.
// Figure out an assignment of
X
, that might actually reduce the execution time.
// Figure out an assignment of
`X`
, that might actually reduce the execution time.
// ** your answer here **
// ** your answer here **
//
//
// Redo the experiment with this value. How many clock cycles did you get?
// Redo the experiment with this value. How many clock cycles did you get?
...
@@ -489,7 +497,7 @@ fn idle() -> ! {
...
@@ -489,7 +497,7 @@ fn idle() -> ! {
//
//
// Look at the generated tests.
// Look at the generated tests.
// Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
// Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
// ** your a
s
nwers (5) here **
// ** your an
s
wers (5) here **
//
//
// Were the optimized tests sufficient to cover the execution time behavior.
// Were the optimized tests sufficient to cover the execution time behavior.
// ** your answer here **
// ** your answer here **
...
@@ -511,4 +519,4 @@ fn idle() -> ! {
...
@@ -511,4 +519,4 @@ fn idle() -> ! {
//
//
// For the future we intend the framework to cover the reading and writing to peripherals, and the
// For the future we intend the framework to cover the reading and writing to peripherals, and the
// sequenced access to resources. In class we will further discuss current limitations, and
// sequenced access to resources. In class we will further discuss current limitations, and
// oportuniti
o
s to improvements.
// oportuniti
e
s to improvements.
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