Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • devel
  • master
  • trustit
3 results

Target

Select target project
  • pln/klee-examples
  • grammers/klee-examples
2 results
Select Git revision
  • master
1 result
Show changes
Commits on Source (21)
Hide whitespace changes
Inline Side-by-side
Showing
with 899 additions and 102 deletions
.gitignore
View file @ 132b7de7
/target
**/*.rs.bk
ktest/target
runner/target
cargo-trust/target
\ No newline at end of file
.vscode/settings.json 0 → 100644
View file @ 132b7de7
{
"cSpell.ignoreWords": [
"backtrace",
"eabihf",
"em",
"fffffffd",
"file",
"istats",
"ktest",
"ktest file",
"libc",
"libcore",
"lldb",
"llvm",
"maybe",
"maybe uninit",
"openocd",
"satisfiability",
"sigabrt",
"thumbv",
"thumbv em",
"trustit",
"uninit",
"vcell",
"x",
"x fffffffd"
]
}
\ No newline at end of file
Cargo.lock
View file @ 132b7de7
......@@ -4,37 +4,40 @@
name = "aligned"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
dependencies = [
"as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
"as-slice",
]
[[package]]
name = "as-slice"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
dependencies = [
"generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
"stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.12.3",
"generic-array 0.13.2",
"stable_deref_trait",
]
[[package]]
name = "bare-metal"
version = "0.2.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
dependencies = [
"rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
"rustc_version",
]
[[package]]
name = "cortex-m"
version = "0.6.1"
source = "git+https://github.com/perlindgren/cortex-m.git?branch=trustit#b2fa26f1044509a34006d4ad6303abc52ea09bce"
source = "git+https://github.com/perlindgren/cortex-m.git?branch=trustit#d8f28518c429febf488baf0dd8d3488779edaa0e"
dependencies = [
"aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"aligned",
"bare-metal",
"klee-sys",
"volatile-register",
]
[[package]]
......@@ -42,10 +45,10 @@ name = "cortex-m-rt"
version = "0.6.11"
source = "git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit#8d2686097e168e8b82d51ae1ea17d9ebe6d567e0"
dependencies = [
"cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
"cortex-m-rt-macros 0.1.7 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m",
"cortex-m-rt-macros",
"klee-sys",
"r0",
]
[[package]]
......@@ -53,91 +56,99 @@ name = "cortex-m-rt-macros"
version = "0.1.7"
source = "git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit#8d2686097e168e8b82d51ae1ea17d9ebe6d567e0"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.13 (registry+https://github.com/rust-lang/crates.io-index)",
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "cortex-m-semihosting"
version = "0.3.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
dependencies = [
"cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
"cortex-m",
]
[[package]]
name = "cstr_core"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
dependencies = [
"cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
"memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)",
"cty",
"memchr",
]
[[package]]
name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
[[package]]
name = "generic-array"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
"typenum",
]
[[package]]
name = "generic-array"
version = "0.13.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
"typenum",
]
[[package]]
name = "klee-examples"
version = "0.1.0"
dependencies = [
"cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
"cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
"cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
"stm32f4 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
"vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m",
"cortex-m-rt",
"cortex-m-semihosting",
"klee-sys",
"lm3s6965",
"panic-halt",
"panic-klee",
"stm32f4",
"vcell",
"volatile-register",
]
[[package]]
name = "klee-sys"
version = "0.1.0"
source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#c8275a34cffb895984d6bdea80e9c6ff9079f769"
source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#3e49ed21f5514e7a3244a21c3cbebfcc4042929c"
dependencies = [
"cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
"cstr_core",
]
[[package]]
name = "lm3s6965"
version = "0.1.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
dependencies = [
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
"bare-metal",
"cortex-m-rt",
]
[[package]]
name = "memchr"
version = "2.2.1"
version = "2.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3197e20c7edb283f87c071ddfc7a2cca8f8e0b888c242959846a6fce03c72223"
[[package]]
name = "panic-halt"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
[[package]]
name = "panic-klee"
......@@ -148,123 +159,104 @@ source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff
name = "proc-macro2"
version = "1.0.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0319972dcae462681daf4da1adeeaa066e3ebd29c69be96c6abb1259d2ee2bcc"
dependencies = [
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"unicode-xid",
]
[[package]]
name = "quote"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"proc-macro2",
]
[[package]]
name = "r0"
version = "0.2.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
[[package]]
name = "rustc_version"
version = "0.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
dependencies = [
"semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
"semver",
]
[[package]]
name = "semver"
version = "0.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
dependencies = [
"semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
"semver-parser",
]
[[package]]
name = "semver-parser"
version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
[[package]]
name = "stable_deref_trait"
version = "1.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
[[package]]
name = "stm32f4"
version = "0.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "88640ad08c62e0651a1320187f38c3655d025ed580a10f0e4d85a2cc4829069f"
dependencies = [
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)",
"cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)",
"vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
"bare-metal",
"cortex-m",
"cortex-m-rt",
"vcell",
]
[[package]]
name = "syn"
version = "1.0.13"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1e4ff033220a41d1a57d8125eab57bf5263783dfdcc18688b1dacc6ce9651ef8"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"proc-macro2",
"quote",
"unicode-xid",
]
[[package]]
name = "typenum"
version = "1.11.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
[[package]]
name = "unicode-xid"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
[[package]]
name = "vcell"
version = "0.1.2"
source = "git+https://github.com/perlindgren/vcell.git?branch=trustit#4eb44a012d65860c596556d6a63af9e0fa31853a"
dependencies = [
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"klee-sys",
]
[[package]]
name = "volatile-register"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
dependencies = [
"vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
"vcell",
]
[metadata]
"checksum aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
"checksum cortex-m 0.6.1 (git+https://github.com/perlindgren/cortex-m.git?branch=trustit)" = "<none>"
"checksum cortex-m-rt 0.6.11 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)" = "<none>"
"checksum cortex-m-rt-macros 0.1.7 (git+https://github.com/perlindgren/cortex-m-rt.git?branch=trustit)" = "<none>"
"checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
"checksum generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)" = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
"checksum generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)" = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
"checksum klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)" = "<none>"
"checksum lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
"checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
"checksum proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)" = "0319972dcae462681daf4da1adeeaa066e3ebd29c69be96c6abb1259d2ee2bcc"
"checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
"checksum stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
"checksum stm32f4 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "88640ad08c62e0651a1320187f38c3655d025ed580a10f0e4d85a2cc4829069f"
"checksum syn 1.0.13 (registry+https://github.com/rust-lang/crates.io-index)" = "1e4ff033220a41d1a57d8125eab57bf5263783dfdcc18688b1dacc6ce9651ef8"
"checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
"checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
"checksum vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)" = "<none>"
"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
Cargo.toml
View file @ 132b7de7
......@@ -33,7 +33,9 @@ version = "0.1.0"
[dependencies.klee-sys]
git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
# path = "../klee-sys"
version = "0.1.0"
#features = ["inline-asm"]
# [dependencies.cortex-m-rtfm]
# path = "../cortex-m-rtpro"
......@@ -48,21 +50,23 @@ vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
#vcell = { path = "../vcell" }
cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
# cortex-m = { path = "../cortex-m" }
#cortex-m = { path = "../cortex-m" }
cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
# cortex-m-rt = { path = "../cortex-m-rt" }
[features]
# default = ["f4"] # uncomment to enable as default feature
klee-analysis = [
"klee-sys/klee-analysis",
"vcell/klee-analysis",
"cortex-m/klee-analysis",
"cortex-m-rt/klee-analysis"
]
inline-asm = ["cortex-m/inline-asm"]
klee-replay = [ "klee-sys/klee-replay"]
inline-asm = ["cortex-m/inline-asm", "klee-sys/inline-asm"]
# rtpro = [ "cortex-m-rtfm/klee-analysis", "cortex-m-rt/rtpro", "lm3s6965" ]
f4 = ["stm32f4/stm32f401", "stm32f4/rt", "cortex-m-semihosting", "cortex-m-rt"]
f4 = ["stm32f4/stm32f401", "stm32f4/rt", "cortex-m-semihosting", "cortex-m-rt", "cortex-m"]
[profile.dev]
panic = "abort"
......
EXAM.md 0 → 100644
View file @ 132b7de7
# Home Exam January 2020.
## Grading:
3) Implement the response time analysis, and overall schedulability test.
4) Generate report on the alaysis results, this could be as a generated html (or xml and use same xml rendering engine) or however you feel like results are best reported and visualized, as discussed in class.
5) Integrate your analysis to the “trustit” framework (KLEE + automated test bed). The complete testbed will be provided later.
## Procedure
Start by reading 1, 2 and 3:
1) [A Stack-Based Resource Allocation Policy for Realtime Processes](https://www.math.unipd.it/~tullio/RTS/2009/Baker-1991.pdf), which refers to
2) [Stack-Based Scheduling of Realtime Processes](https://link.springer.com/content/pdf/10.1007/BF00365393.pdf), journal publication based on technical report [3] of the 1991 paper. The underlying model is the same in both papers.
3) [Rate Monotonic Analysis](http://www.di.unito.it/~bini/publications/2003BinButBut.pdf) , especially equation 3 is of interest to us. (It should be familiar for the real-time systems course you have taken previously.)
## Presentation
Make a git repo of your solution(s) with documentation (README.md) sufficient to reproduce your results.
Notify me (Telegram or mail) and we decide on time for individual presentation. 30 minutes should be sufficient.
---
## Definitions
A task `t` is defined by:
- `P(t)` the priority of task `t`
- `D(t)` the deadline of taks `t`
- `A(t)` the inter-arrival of task `t`
A resource `r` is defined by:
- `π(r)` the resource ceiling, computed as the highest priority of any task accessing `r`. SRP allows for dynamic priorities, in our case we have static priorities only.
For SRP based analysis we assume a task to perform/execute a finite sequence of operations/instructions (aka. run-to-end or run-to-completion semantics). During execution, a task can claim resources `Rj`... in nested fashion. Sequential re-claim of resources is allowed but NOT re-claiming an already held resource (in a nested fashion, since that would violate the Rust memory aliasing rule).
E.g., a possible trace for a task can look like:
`[t:...[r1:...[r2:...]...]...[r2:...]...]`, where `[r:...]` denotes a critical section of task `t` holding the resource `r`. In this case the task starts, and at some point claims `r1` and inside the critical section claims `r2` (nested claim), at some point it exits `r2`, exits `r1` and continues executing where it executes a critical section on `r2`, and then finally executes until completion.
## Grade 3
Analysis:
### 1. Total CPU utilization
Worst Case Execution Time (WCET) for tasks and critical sections
In general determining WCET is rather tricky. In our case we adopt a measurement based technique, that spans all feasible paths for the task. Tests triggering the execution paths are automatically generated by symbolic execution. To correctly take concurrency into account resource state is treated symbolically. Thus, for a critical section, the resource is given a fresh (new) symbolic value for each critical section. Inside the critical section we are ensured exclusive access (and thus the value can be further constrained inside of the critical section). The resource model can be further extended by contracts (as shown by the `assume_assert.rs` example).
We model hardware (peripherals) as shared resources (shared by the environment) as being *atomic* (with read/write/modify operations only). Rationale, we must assume that the state of the hardware resources may be changed at any time, thus only *atomic* access can be allowed.
For now, we just assume we have complete WCETs information, in terms of `start` and `end` time-stamps (`u32`) for each section `[_: ... ]`. We represent that by the `Task` and `Trace` data structures in `common.rs`.
### Total CPU request (or total load factor)
Each task `t` has a WCET `C(t)` and inter-arrival time `A(t)`. The CPU request (or load) inferred by a task is `L(t)` = `C(t)`/`A(t)`. Ask yourself, what is the consequence of `C(t)` > `A(t)`?
We can compute the total CPU request (or load factor), as `Ltot` = sum(`L(T)`), `T` being the set of tasks.
Ask yourself, what is the consequence of `Ltot` > 1?
Implement a function taking `Vec<Task>` and returning the load factor.
### Response time (simple over-approximation)
Under SRP response time can be computed by equation 7.22 in [Hard Real-Time Computing Systems](
https://doc.lagout.org/science/0_Computer%20Science/2_Algorithms/Hard%20Real-Time%20Computing%20Systems_%20Predictable%20Scheduling%20Algorithms%20and%20Applications%20%283rd%20ed.%29%20%5BButtazzo%202011-09-15%5D.pdf).
In general the response time is computed as.
- `R(t)` = `C(t)` + `B(t)` + `I(t)`, where
- `B(t)` is the blocking time for task `t`, and
- `I(t)` is the interference (preemptions) to task `t`
For a task set to be schedulable under SRP we have two requirements:
- `Ltot` < 1
- `R(t)` < `D(t)`, for all tasks. (`R(t)` > `D(t)` implies a deadline miss.)
#### Blocking
SRP brings the outstanding property of single blocking. In words, a task `t` is blocked by the maximal critical section a task `l` with lower priority (`P(l)`< `P(t)`) holds a resource `l_r`, with a ceiling `π(l_r)` equal or higher than the priority of `t`.
- `B(t)` = max(`C(l_r)`), where `P(l)`< `P(t)`, `π(l_r) >= P(t)`
Implement a function that takes a `Task` and returns the corresponding blocking time.
#### Preemptions
A task is exposed to interference (preemptions) by higher priority tasks. Intuitively, during the execution of a task `t` (`Bp(t)`) each higher priority task `h` (`P(h)`>`P(t)`) may preempt us (`Bp(t)`/`A(h)` rounded upwards) times.
- `I(t)` = sum(`C(h)` * ceiling(`Bp(t)`/`A(h)`)), forall tasks `h`, `P(h)` > `P(t)`, where
- `Bp(t)` is the *busy-period*
We can over approximate the *busy period* `Bp(i)` = `D(i)` (assuming the worst allowed *busy-period*).
As a technical detail. For the scheduling of tasks of the same priority, the original work on SRP adopted a FIFO model (first arrived, first served). Under Rust RTFM, tasks are bound to hardware interrupts. Thus we can exploit the underlying hardware to do the actual scheduling for us (with zero-overhead). However the interrupt hardware, schedules interrupts of the same priority by the index in the vector table. For our case here we can make a safe over approximation by considering preemptions from tasks with SAME or higher priority (`P(h)` >= `P(t)`).
Implement a function that takes a `Task` and returns the corresponding preemption time.
Now make a function that computes the response time for a `Task`, by combing `C(t)`, `B(t)` and `I(t)`.
Finally, make a function that iterates over the task set and returns a vector with containing:
`Vec<Task, R(t), C(t), B(t), I(t)>`. Just a simple `println!` of that vector gives the essential information on the analysis.
#### Preemptions revisited
The *busy-period* is in `7.22` computed by a recurrence equation.
Implement the recurrence relation (equation) starting from the base case `C(t) + B(t)`. The recurrence might diverge in case the `Bp(t) > D(t)`, this is a pathological case, where the task becomes non-schedulable, in that case terminate the recurrence (with an error). You might want to indicate that a non feasible response time have been reached by using the `Result<u32, ())>` type or some other means e.g., (`Option<u32>`).
You can let your `preemption` function take a parameter indicating if the exact solution or approximation should be used.
## Grade 4
Here you can go wild, and use your creativity to present task set and results of analysis in the best informative manner. We will discuss some possible visualizations during class.
## Grade 5
If you aim for the highest grade, let me know and I will hook you up with the current state of the development. The goal is to derive the task set characterization by means of the automated test-bed, (test case generation + test runner based on the `probe.rs` library.) All the primitives are there, and re-implementing (back-porting) previous work based on `RTFM3` is mostly an engineering effort.
---
## Resources
`common.rs` gives the basic data structures, and some helper functions.
`generate.rs` gives an example on how `Tasks` can be manually constructed. This is vastly helpful for your development, when getting started.
## Tips
When working with Rust, the standard library documentation [std](https://doc.rust-lang.org/std/) is excellent and easy to search (just press S). For most cases, you will find examples on intended use and cross referencing to related data types is just a click away.
Use the `generate` example to get started. Initially you may simplify it further by reducing the number of tasks/and or resources. Make sure you understand the helper functions given in `common.rs`, (your code will likely look quite similar). You might want to add further `common` types and helper functions to streamline your development, along the way.
Generate your own task sets to make sure your code works in the general case not only for the `Tasks` provided. Heads up, I will expose your code to some other more complex task sets.
---
## Robust and Energy Efficient Real-Time Systems
In this part of the course, we have covered.
- Software robustness. We have adopted Rust and Symbolic Execution to achieve guaranteed memory safety and defined behavior (panic free execution). With this at hand, we have a strong (and theoretically underpinned) foundation for improved robustness and reliability proven at compile time.
- Real-Time Scheduling and Analysis. SRP provides an execution model and resource management policy with outstanding properties of race-and deadlock free execution, single blocking and stack sharing. Our Rust RTFM framework provides a correct by construction implementation of SRP, exploiting zero-cost (software) abstractions. Using Rust RTFM resource management and scheduling, is done by directly by the hardware, which allows for efficiency (zero OH) and predictability.
The SRP model is amenable to static analysis, which you have now internalized through an actual implementation of the theoretical foundations. We have also covered methods for Worst Case Execution Time (WCET) analysis by cycle accurate measurements, which in combination with Symbolic Execution for test-case generation allows for high degree of automation.
- Energy Consumption is roughly proportional to the supply voltage (static leakage/dissipation), and exponential to the frequency (dynamic/switching activity dissipation). In the case of embedded systems, low-power modes allow parts of the system to be powered down while retaining sufficient functionality to wake on external (and/or internal) events. In sleep mode, both static and dynamic power dissipation is minimized typically to the order of uAmp (in comparison to mAmp in run mode).
Rust RTFM adopts an event driven approach allowing the system to automatically sleep in case no further tasks are eligible for scheduling. Moreover, leveraging on the zero-cost abstractions in Rust and the guarantees provided by the analysis framework, we do not need to sacrifice correctness/robustness and reliability in order to obtain highly efficient executables.
Robust and Energy Efficient Real-Time Systems for real, This is the Way!
README.md
View file @ 132b7de7
......@@ -2,14 +2,13 @@
This repo contains a set of usage examples for `klee-sys` low-level KLEE bindings. For more information on internal design behind see the [klee-sys](https://gitlab.henriktjader.com/pln/klee-sys) repo.
See section `Cargo.toml` for detaled information on features introduced.
See section `Cargo.toml` for detailed information on features introduced.
### General dependencies
- llvm toolchain tested with (9.0.1)
- rustup tested with 1.40.0 (73528e339 2019-12-16)
- klee tested with KLEE 2.1-pre (https://klee.github.io)
- LLVM toolchain tested with (9.0.1 and 10.0.1)
- rustup tested with rust toolchain 1.47.0 (18bf6b4f0 2020-10-07) and 1.49.0-nightly (ffa2e7ae8 2020-10-24)
- klee tested with KLEE 2.1 (https://klee.github.io)
- cargo-klee (installed from git)
---
......@@ -18,11 +17,11 @@ See section `Cargo.toml` for detaled information on features introduced.
- `paths.rs`
This example showcase the different path termintaiton conditions possible and their effect to KLEE test case generation.
This example showcase the different path termination conditions possible and their effect to KLEE test case generation.
- `assume_assert.rs`
This example showcase contract based verification, and the possibilies to extract proofs.
This example showcase contract based verification, and the possibilities to extract proofs.
- `struct.rs`
......@@ -40,7 +39,12 @@ See section `Cargo.toml` for detaled information on features introduced.
- `register_test.rs`
Simple test to showcase the use of the `volatile-register` abstraction. `volitile-register` builds on `vcell` and is used by both hand written and machine generated hardware accesses in the Rust embedded ecosystem.
Simple test to showcase the use of the `volatile-register` abstraction. `volitile-register` builds on `vcell` and is used by both hand written and machine generated hardware accesses in the Rust embedded ecosystem.
This example also showcase the `gdb` replay functionality.
TODO: perhaps better to put the `gdb` replay in the Basic test examples,
as replay is not tied to `volatile-register`.
- `cortex-m-test1.rs`
......@@ -68,14 +72,29 @@ See section `Cargo.toml` for detaled information on features introduced.
- llvm target `thumbv7em-none-eabihf`
- `> rustup show`, to show current Rust tool-chain and installed targets.
- `> rustup target add <target>`, to add target, e.g., `thumbv7em-none-eab¡hf`.
- [cargo bin-utils](https://github.com/rust-embedded/cargo-binutils) (tested with version 0.1.7)
### Examples
- `f401_minimal.rs`
This example showcase the execution of code on the stm32f401 (and similar targets from the f4).
This example showcase the execution of a minimal "Hello World!" application on the stm32f401 (and similar targets from the f4).
- `f401_minimal2.rs`
This example showcase cycle accurate and non-intrusive execution time measurements. It also covers, debug vs. release mode optimization and the effect of the `inline-asm` feauture.
- `f401_probe.rs`
--
A continuation of `f401_minimal2.rs`, showcasing the ultimate degree of automation possible, in an all Rust profiling setting. Further information is found in the `runner` crate.
---
### Disclaimer
This project is in early development, thus expect bugs and shortcomings, no API stability offered or guaranteed. It is however well suited for experimentation and all implemented features have been successfully tested.
---
## Licencse
......
compile.txt deleted 100644 → 0
View file @ aad74fbe
examples/README.md 0 → 100644
View file @ 132b7de7
# Examples
## assume_assert
Exercises the ability to introduce assumptions in order to prove assertions.
This leads into possibilities for contracts.
## register_test
Exercises the ability to automatically treat hardware read accesses as streams of unknown values,
and hardware write accesses as no operations. In this way, we can *pessimistically* analyse low-level
code such as drivers. More detailed information (assumptions) on the behavior of the hardware can be
modelled as mocks for the corresponding register blocks.
\ No newline at end of file
examples/assume_assert.rs
View file @ 132b7de7
......@@ -50,7 +50,7 @@ fn f1(a: u32) -> u32 {
// #100000193 in _ZN4core9panicking9panic_fmt17hdeb7979ab6591473E (=94422569870368, =94422566526016) at src/libcore/panicking.rs:139
// #200000227 in _ZN4core9panicking5panic17hb5daa85c7c72fc62E (=94422566525664, =28, =94422566526016) at src/libcore/panicking.rs:70
// #300000130 in _ZN13assume_assert2f117h371b5439de984e07E () at examples/assume_assert.rs:19
// #400000088 in main () at examples/assume_assert.rs:13
// #400000088 in main () at examples/assume_assert.rs:13
//
// So its line 19, (a + 1)
//
......@@ -74,7 +74,7 @@ fn f1(a: u32) -> u32 {
// So KLEE tracks the "path condition", i.e., at line 18 it knows (assumes) that that
// a < u32::MAX, and finds that the assumption a == u32::MAX cannot be satisfied.
//
// This is extremely powerful as KLEE tracks all known "constraints" and all their raliaitons
// This is extremely powerful as KLEE tracks all known "constraints" and all their relations
// and mathematically checks for the satisfiability of each "assume" and "assert".
// So what we get here is not a mere test, but an actual proof!!!!
// This is the way!
......@@ -102,7 +102,7 @@ fn f1(a: u32) -> u32 {
// a + 1
// }
//
// It might even be possible to derive post condtitions from pre conditions,
// It might even be possible to derive post conditions from pre-conditions,
// and report them to the user. Problem is that the conditions are
// represented as "first order logic" (FOL) constraints, which need to be
// converted into readable form (preferably Rust expressions.)
......
examples/f401_ktest.rs 0 → 100644
View file @ 132b7de7
// minimal example for the stm32-f401 (and the f4 series)
//! Prints "Hello, world!" on the host console using semihosting
#![feature(asm)]
#![no_main]
#![no_std]
extern crate panic_halt;
use stm32f4::stm32f401 as stm32;
use cortex_m::{asm, bkpt};
use cortex_m_rt::entry;
// // use klee_sys::klee_make_symbolic2;
// // Mimic RTFM resources
// static mut X: u32 = 54;
#[entry]
#[inline(never)]
fn main() -> ! {
let mut x = 54;
klee_make_symbolic(&mut x);
if x == 0 {
bkpt!();
}
loop {
asm::nop();
}
}
#[inline(never)]
pub fn klee_make_symbolic<T>(data: &mut T) {
// force llvm to consider data to be mutaded
unsafe {
asm!("bkpt #0" : /* output */: /* input */ "r"(data): /* clobber */ : "volatile")
}
}
// pub fn taint() {
// unsafe {
// X = 73;
// }
// }
// #[no_mangle]
// pub extern "C" fn klee_bkpt(data: *mut core::ffi::c_void) {
// bkpt!();
// }
// extern "C" {
// pub fn klee_bkpt(ptr: *mut core::ffi::c_void, // pointer to the data
// );
// }
// cargo objdump --bin app --release -- -disassemble -no-show-raw-insn
// unsafe { asm!("mov $0,R15" : "=r"(r) ::: "volatile") }
// cargo objdump --example f401_ktest --release --features f4,inline-asm --target thumbv7em-none-eabihf -- -d
examples/f401_minimal.rs
View file @ 132b7de7
......@@ -8,6 +8,7 @@ extern crate panic_halt;
use stm32f4::stm32f401 as stm32;
use cortex_m::asm;
use cortex_m_rt::entry;
use cortex_m_semihosting::hprintln;
......@@ -15,7 +16,9 @@ use cortex_m_semihosting::hprintln;
fn main() -> ! {
hprintln!("Hello, world!").unwrap();
loop {}
loop {
asm::nop();
}
}
// See RM0368 Reference Manual for details
......@@ -29,4 +32,84 @@ fn main() -> ! {
// openocd -f openocd.cfg
//
// cargo run --example f401_minimal --features f4 --target thumbv7em-none-eabihf
//
// ...
// DefaultPreInit () at /home/pln/.cargo/git/checkouts/cortex-m-rt-073d0396a6df513c/8d26860/src/lib_thumb_rt.rs:571
// 571 pub unsafe extern "C" fn DefaultPreInit() {}
// (gdb)
//
// At this point, the progrom has been flashed onto the target (stm32f401/f411).
//
// (gdb) c
// Continuing.
//
// Breakpoint 1, main () at examples/f401_minimal.rs:14
// 14 #[entry]
//
// `main` is our "entry" point for the user application.
// It can be named anything by needs to annotated by #[entry].
// At this point global variables have been initiated.
//
// The `openocd.gdb` script defines the startup procedure, where we have set
// a breakpoint at the `main` symbol.
//
// Let's continue.
//
// (gdb) c
// Continuing.
// halted: PC: 0x08001206
//
// In the `openocd` terminal the `Hello world!` text should appear.
// The program is stuck in the infinite `loop {}`.
//
// If you press Ctrl-C, you will force the target (stm32fxx) to break.
//
// (gdb) c
// Continuing.
// halted: PC: 0x08001206
// ^C
// Program received signal SIGINT, Interrupt.
// f401_minimal::__cortex_m_rt_main () at examples/f401_minimal.rs:19
// 19 loop {
//
// (gdb) disassemble
// Dump of assembler code for function f401_minimal::__cortex_m_rt_main:
// 0x0800019a <+0>: movw r0, #5104 ; 0x13f0
// 0x0800019e <+4>: movt r0, #2048 ; 0x800
// 0x080001a2 <+8>: movs r1, #14
// 0x080001a4 <+10>: bl 0x8000f86 <cortex_m_semihosting::export::hstdout_str>
// 0x080001a8 <+14>: movw r1, #5144 ; 0x1418
// 0x080001ac <+18>: movt r1, #2048 ; 0x800
// 0x080001b0 <+22>: bl 0x80011fa <core::result::Result<T,E>::unwrap>
// 0x080001b4 <+26>: b.n 0x80001b6 <f401_minimal::__cortex_m_rt_main+28>
// 0x080001b6 <+28>: bl 0x80012b4 <__nop>
// => 0x080001ba <+32>: b.n 0x80001b6 <f401_minimal::__cortex_m_rt_main+28>
//
// (In gdb you may use tab, for command completion, up arrow for previous command and
// shortcuts for just about anything, `c` for `continue` e.g.)
//
// 0x080001b6 <+28>: bl 0x80012b4 <__nop>
// is a "branch and link call" to a function `__nop`, that simply does nothing (no operation).
// 0x080001ba <+32>: b.n 0x80001b6 <f401_minimal::__cortex_m_rt_main+28>
// in a branch to the previous instruction, indeed an infinite loop right.
//
// Some basic Rust.
// Use https://www.rust-lang.org/learn and in particular https://doc.rust-lang.org/book/.
// There is even a book on embedded Rust available:
// https://rust-embedded.github.io/book/, it covers much more than we need here.
//
// Figure out a way to print the numbers 0..10 using a for loop.
//
// Figure out a way to store the numbers in 0..10 in a static (global) array using a loop.
//
// Print the resulting array (using a single println invocation, not a loop).
//
// (You may prototype the code directly on https://play.rust-lang.org/, and when it works
// back-port that into the minimal example, and check that it works the same)
//
// These two small exercises should get you warmed up.
//
// Some reflections:
// Why is does dealing with static variables require `unsafe`?
//
// This is the way!
examples/f401_minimal2.rs 0 → 100644
View file @ 132b7de7
// minimal example for the stm32-f401 (and the f4 series)
//! Prints "Hello, world!" on the host console using semihosting
#![no_main]
#![no_std]
extern crate panic_halt;
use stm32f4::stm32f401 as stm32;
use cortex_m::asm;
use cortex_m_rt::entry;
#[entry]
#[inline(never)] // to keep the symbol
fn main() -> ! {
asm::nop();
asm::nop();
asm::bkpt();
do_some_work();
asm::bkpt();
loop {
asm::nop();
}
}
fn do_some_work() {
for _ in 0..100 {
asm::nop();
}
}
// cargo run --example f401_minimal2 --features f4 --target thumbv7em-none-eabihf
// ...
// halted: PC: 0x08000322
// DefaultPreInit () at /home/pln/.cargo/git/checkouts/cortex-m-rt-073d0396a6df513c/8d26860/src/lib_thumb_rt.rs:571
// 571 pub unsafe extern "C" fn DefaultPreInit() {}
// (gdb) disassemble
// Dump of assembler code for function DefaultPreInit:
// => 0x08000322 <+0>: bx lr
// End of assembler dump.
// (gdb) c
// Continuing.
// Breakpoint 1, main () at examples/f401_minimal2.rs:14
// 14 #[entry]
// (gdb) c
// Continuing.
// halted: PC: 0x0800019a
// Program received signal SIGTRAP, Trace/breakpoint trap.
// 0x08000420 in __bkpt ()
// (gdb) backtrace
// #0 0x08000420 in __bkpt ()
// #1 0x080001a6 in cortex_m::asm::bkpt () at /home/pln/.cargo/git/checkouts/cortex-m-514878a7410beb63/d8f2851/src/asm.rs:19
// #2 f401_minimal2::__cortex_m_rt_main () at examples/f401_minimal2.rs:18
// inline-frame.c:156: internal-error: void inline_frame_this_id(frame_info*, void**, frame_id*): Assertion `frame_id_p (*this_id)' failed.
// A problem internal to GDB has been detected,
// further debugging may prove unreliable.
// Quit this debugging session? (y or n) n
//
// This is a bug, please report it. For instructions, see:
// <http://www.gnu.org/software/gdb/bugs/>.
//
// inline-frame.c:156: internal-error: void inline_frame_this_id(frame_info*, void**, frame_id*): Assertion `frame_id_p (*this_id)' failed.
// A problem internal to GDB has been detected,
// further debugging may prove unreliable.
// Create a core file of GDB? (y or n) n
// Command aborted.
// .... eeeehhh no worries, GDB is written in C and still kind of works
// (gdb) frame 2
// #2 f401_minimal2::__cortex_m_rt_main () at examples/f401_minimal2.rs:18
// 18 asm::bkpt();
// So we can get back to the "caller" (that called the `__bkpt()` function).
// At this point we can disassassemble the program.
//
// (gdb) disassemble
// Dump of assembler code for function f401_minimal2::__cortex_m_rt_main:
// 0x08000584 <+0>: bl 0x800077c <__nop>
// 0x08000588 <+4>: bl 0x800077c <__nop>
// 0x0800058c <+8>: bl 0x8000778 <__bkpt>
// => 0x08000590 <+12>: bl 0x800059c <f401_minimal2::do_some_work>
// 0x08000594 <+16>: b.n 0x8000596 <f401_minimal2::__cortex_m_rt_main+18>
// 0x08000596 <+18>: bl 0x800077c <__nop>
// 0x0800059a <+22>: b.n 0x8000596 <f401_minimal2::__cortex_m_rt_main+18>
//
// We see the two calls to the nop function, the bkpt call, the call to do_some_work_
// followed by the infinite loop.
// Great!
//
// Now lets try to find out how long it takes to `do_some_work`.
//
// One way would be by stepping the code and counting the number of steps.
// That is tedious and boring, and prone to errors.
//
// The ARM M4 core has some nice features allowing making our life easier.
//
// The DWT (Debug and Watchpoint and Trace Unit)
// http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.100166_0001_00_en/ric1417175910926.html
// And in particular, the DWT programmers model.
// What we want to do is
// (gdb) mon mww 0xe0001000 1
// (gdb) mon mww 0xe0001004 0
// (gdb) mon mdw 0xe0001004
// Which
// - enables the DWT
// - sets the cyclecounter to 0
// - reads the cyclcounter
//
// Now let the program run (from the first bkpt to the next bkpt.
// (gdb) c
// Continuing.
// Program received signal SIGTRAP, Trace/breakpoint trap.
// 0x0800077c in __bkpt ()
//
// (gdb) mon mdw 0xe0001004
// 0xe0001004: 0000b92f
//
// Alternativle you may use the `x` (examine memory command)
// (gdb) x 0xe0001004
// 0xe0001004: 0x0000b92f
//
// Or in decimal
// (gdb) x/d 0xe0001004
// 0xe0001004: 47407
//
// So some 47k clock cycles... Hmm quite a lot for a loop 0..100 doing ... nothing
//
// Let's repeat the experiment in --release (optimized mode)
//
// cargo run --example f401_minimal2 --features f4 --target thumbv7em-none-eabihf --release
// ...
// run to first breakpoint, setup the DWT cyclecounter, run to breakpoint
// I got 505, cycles. Good but not great... still 5 cycles per nop, right?
//
// Well let's look at the code.
// (gdb) disassemble
// Dump of assembler code for function f401_minimal2::__cortex_m_rt_main:
// => 0x0800019a <+0>: bl 0x80003f4 <__nop>
// 0x0800019e <+4>: bl 0x80003f4 <__nop>
// 0x080001a2 <+8>: bl 0x80003f0 <__bkpt>
// 0x080001a6 <+12>: bl 0x80003f4 <__nop>
// 0x080001aa <+16>: bl 0x80003f4 <__nop>
// 0x080001ae <+20>: bl 0x80003f4 <__nop>
// 0x080001b2 <+24>: bl 0x80003f4 <__nop>
// 0x080001b6 <+28>: bl 0x80003f4 <__nop>
// 0x080001ba <+32>: bl 0x80003f4 <__nop>
// 0x080001be <+36>: bl 0x80003f4 <__nop>
// 0x080001c2 <+40>: bl 0x80003f4 <__nop>
// 0x080001c6 <+44>: bl 0x80003f4 <__nop>
// 0x080001ca <+48>: bl 0x80003f4 <__nop>
// 0x080001ce <+52>: bl 0x80003f4 <__nop>
// 0x080001d2 <+56>: bl 0x80003f4 <__nop>
// ... a 100 in a row, that's some heavy inlining right!
//
// Well at this point, Rust + LLVM is not ALLOWED to do better.
// The assembly (nop) instruction is marked "volatile", meaning it implies
// a side effect, so Rust + LLVM is not allowed to optimize it out.
// That is indeed excellent, as we will discuss later.
//
// But why is the `__nop` a function call and not a native assebly nop?
// Well, Rust has yet to decide on a "stable" format for inline assembly.
// It's merely a syntactical thing, and the RFC has not yet been accepted
// (in due time we will have it.)
//
// In the meantime we can use inline assembly as an "unstable" feature
// by enabled in the nightly toolchain.
//
// > rustup override set nightly
//
// Now we have enabled the nightly toolchain for the current directory (a bit Nix like)
//
// cargo run --example f401_minimal2 --features f4 --target thumbv7em-none-eabihf --release --features inline-asm
//
// run until the first bkpt instruction...
//
// Program received signal SIGTRAP, Trace/breakpoint trap.
// f401_minimal2::__cortex_m_rt_main () at examples/f401_minimal2.rs:19
// 19 asm::bkpt();
// (gdb) disassemble
// Dump of assembler code for function f401_minimal2::__cortex_m_rt_main:
// 0x0800019a <+0>: nop
// 0x0800019c <+2>: nop
// => 0x0800019e <+4>: bkpt 0x0000
// 0x080001a0 <+6>: nop
// 0x080001a2 <+8>: nop
// 0x080001a4 <+10>: nop
// 0x080001a6 <+12>: nop
// 0x080001a8 <+14>: nop
// 0x080001aa <+16>: nop
// 0x080001ac <+18>: nop
// 0x080001ae <+20>: nop
// 0x080001b0 <+22>: nop
// 0x080001b2 <+24>: nop
// 0x080001b4 <+26>: nop
//
// (gdb) mon mww 0xe0001000 1
// (gdb) mon mww 0xe0001004 0
// (gdb) c
// Continuing.
//
// Program received signal SIGTRAP, Trace/breakpoint trap.
// f401_minimal2::__cortex_m_rt_main () at examples/f401_minimal2.rs:21
// 21 asm::bkpt();
// (gdb) mon mdw 0xe0001004
// 0xe0001004: 00000064
//
// (gdb) x/d 0xe0001004
// 0xe0001004: 100
//
// So what have we learned?
// - how we can do NON INTRUSIVE cycle accurate execution time measuremnts
// - how we can speed up a program 470 times without altering its semantics
//
// So back to the question on "volatile" (assembly) instructions.
// "volatile" in this context implies a number of things.
// - it may note be optimized out
// - the order of volatile instructions along an execution path must be preserved
//
// This allows us to
// - write inline assembler for parts of our code that is extremely timing critical
// - introduce precise delays
// - fiddle with CPU registers
// - stack pointer
// - link register
// - special purpose core registers (interrupt enable/disable etc.)
// Essentially using inline assembly we can ALL in Rust. We do not NEED to link
// to external assembly code or external C code (still we can if we want)...
//
// All in Rust, That is the Way!
examples/f401_probe.rs 0 → 100644
View file @ 132b7de7
// minimal example for the stm32-f401 (and the f4 series)
//! Prints "Hello, world!" on the host console using semihosting
#![no_main]
#![no_std]
extern crate panic_halt;
use stm32f4::stm32f401 as stm32;
use cortex_m::asm;
use cortex_m_rt::entry;
#[entry]
#[inline(never)] // to keep the symbol
fn main() -> ! {
asm::nop();
asm::nop();
asm::bkpt();
do_some_work();
asm::bkpt();
loop {
asm::nop();
}
}
fn do_some_work() {
for _ in 0..100 {
asm::nop();
}
}
// cargo run --example f401_probe --features f4 --target thumbv7em-none-eabihf
// ...
//
// The ARM M4 core provides the DWT register for cycle accurate measurements (CYCCNT).
// There is a lot more possibilities to tracing etc. that we will not cover in this course
//
// The real power however comes from automation.
// gdb (designed in the mid 80s) offers automation through python (natively)
// and bindings to sereverals high level languages have been developed.
//
// However, internally gdb has a lot of technical dept, and high internal complexity
// partly due to C and the ad-hoc threading model (threading was introduced along the way
// and not part of the "design".)
//
// More recently the llvm project has released debugger with largely compatible
// interface and automation capabalities. lldb is however not yet supporting
// embedded systems (so we stick to gdb atm)
//
// In both cases their code base is huge, and they are vary capable as designed for
// general purpose debugging.
//
// What we need in order to profile embedded code is however just a small but very
// precise subset of the functionality, defined by the ARM coresight API (for core access)
// and probing functionality (providid by e.g. stlink or DAP link).
//
// Using the latter you can e.g.:
// - read and write bytes/words and blocks thereof
// - read and write flash (writing is section based, first eraze then program)
//
// This type of low-level debug access is sufficent to automate profiling,
// tracing, etc.
//
// The recent Rust `probe-rs` team aims at supporting probing and coresight APIs.
// While the code base is young and immature, it already provides what we need to:
// - program (flash code), this was implemented for the M4 this weekend
// - stepping to and from breakpoint instructions
// - managing the DWT
// The latter two I implemented yesterday, so be aware there might be bugs out there...
//
// So here we go:
// 1. confirm that the above program compiles and runs as expected.
// 2. go to the `runner` folder and run `cargo run --bin f401_probe`
//
// You should get something like:
// device STLink V2-1 (VID: 1155, PID: 14155, STLink)
// probe connected
// strategy ChipInfo(ChipInfo { manufacturer: JEP106Code({ cc: 0x00, id: 0x20 } => Some("STMicroelectronics")), part: 1041 })
// target Target { identifier: TargetIdentifier { chip_name: "STM32F411VETx", ...
// Continue running
// Hit breakpoint :Core stopped at address 0x0800019e
// Continue from breakpoint.
// running
// Hit breakpoint :Core stopped at address 0x08000268
// cycles 100
//
// Have a close look at the small program, and the `runner` library.
//
// Hints:
// cargo doc --open
// Documenst the API, and lets you browse the documentation and source code behind.
//
// cargo objdump --example f401_probe --release --features f4,inline-asm --target thumbv7em-none-eabihf -- -d
// Part of the `cargo bin-utils` package that lets you inspect the generated binary.
//
// Later you will build a small analysis framework combining symbolic execution
// with the measurement based testing, to derive WCET estimates for embedded applications.
//
// This is the Way!
examples/register_test.rs
View file @ 132b7de7
......@@ -27,7 +27,7 @@ fn main() {
// embedded Rust ecosystem.
//
// When analyzed by KLEE, we make the return value symbolic, thus each access
// givs a new unique symbol. Even if we write a value to it, the next read
// gives a new unique symbol. Even if we write a value to it, the next read
// will still be treated as a new symbol. That might be overly pessimistic
// but is a safe approximation for the worst case behavior of the hardware.
//
......@@ -104,7 +104,7 @@ fn main() {
// object 1: uint: 2
// object 1: text: ....
//
// The first read gives 1, the second 2, and we hit unreacable.
// The first read gives 1, the second 2, and we hit unreachable.
//
// We can replay the last test to gather more information:
// $ cargo klee --example register_test -r -k -g -v
......@@ -136,7 +136,9 @@ fn main() {
// (gdb) print read_2
// $2 = 2
//
// If this does not work its a gdb problem, try lldb the LLVM debugger
// If this does not work its a gdb problem, try `lldb` (or `rust-lldb`) the LLVM debugger
// (debug info may not be completely compatible)
//
// https://lldb.llvm.org/use/map.html
//
// This is the way!
ktest/Cargo.lock 0 → 100644
View file @ 132b7de7
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
[[package]]
name = "ktest"
version = "0.1.0"
ktest/Cargo.toml 0 → 100644
View file @ 132b7de7
[package]
name = "ktest"
version = "0.1.0"
authors = ["Per Lindgren <per.lindgren@ltu.se>"]
edition = "2018"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[lib]
name = "ktest"
path = "src/lib.rs"
[[bin]]
name = "ktest"
path = "src/main.rs"
\ No newline at end of file
ktest/src/README.md 0 → 100644
View file @ 132b7de7
# ktest
Tool to read ktest files
ktest/src/lib.rs 0 → 100644
View file @ 132b7de7
use std::fs::File;
use std::io::prelude::*; // provide io traits
use std::io::{Error, ErrorKind};
#[derive(Debug)]
pub struct KTEST {
pub version: i32,
pub args: Vec<String>,
pub objects: Vec<(String, Vec<u8>)>,
}
pub fn read_ktest(file_name: &str) -> std::io::Result<KTEST> {
let mut file: File = File::open(file_name)?;
let mut hdr = [0u8; 5];
file.read_exact(&mut hdr)?;
if &hdr != b"KTEST" {
return Err(Error::new(ErrorKind::Other, "not a KTEST file"));
}
let version = read_i32(&mut file)?;
println!("version : {}", version);
if version > 3 {
return Err(Error::new(ErrorKind::Other, "non support KTEST version"));
}
let num_args = read_i32(&mut file)?;
// info regarding the KTEST file
let mut args = vec![];
for _ in 0..num_args {
let arg = read_sized(&mut file)?;
let str = String::from_utf8(arg).unwrap();
args.push(str);
}
// metadata not used here
let _sym_argvs = read_i32(&mut file)?;
let _sym_argv_len = read_i32(&mut file)?;
// read the objects
let num_objects = read_i32(&mut file)?;
let mut objects = vec![];
for _ in 0..num_objects {
let name = read_string(&mut file)?;
let data = read_sized(&mut file)?;
objects.push((name, data))
}
Ok(KTEST {
version,
args,
objects,
})
}
fn read_i32(file: &mut File) -> std::io::Result<i32> {
let mut str = [0u8; 4];
file.read_exact(&mut str)?;
Ok(i32::from_be_bytes(str)) // big endian
}
fn read_string(file: &mut File) -> std::io::Result<String> {
let str = read_sized(file)?;
Ok(String::from_utf8(str).unwrap())
}
fn read_sized(file: &mut File) -> std::io::Result<Vec<u8>> {
let size = read_i32(file)?;
let mut buf = vec![0u8; size as usize];
file.read_exact(&mut buf)?;
Ok(buf)
}
ktest/src/main.rs 0 → 100644
View file @ 132b7de7
use ktest::{read_ktest, KTEST};
fn main() -> std::io::Result<()> {
let ktest = read_ktest("test000001.ktest");
println!("{:?}", ktest);
Ok(())
}
ktest/test000001.ktest 0 → 100644
View file @ 132b7de7
File added