From e0c683b6711fc02e388837af0ec0e652c0e1dbcf Mon Sep 17 00:00:00 2001 From: Per Lindgren Date: Mon, 25 Oct 2021 10:02:59 +0200 Subject: [PATCH] soundness and cost --- Cargo.toml | 6 ++- examples/lock_cost.rs | 79 +++++++++++++++++++++++++++++++++ examples/lockall_cost.rs | 81 ++++++++++++++++++++++++++++++++++ examples/lockall_soundness3.rs | 40 +++++++++++++++++ 4 files changed, 205 insertions(+), 1 deletion(-) create mode 100644 examples/lock_cost.rs create mode 100644 examples/lockall_cost.rs create mode 100644 examples/lockall_soundness3.rs diff --git a/Cargo.toml b/Cargo.toml index 3f32a80eee..b2c62d0e07 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,7 +20,7 @@ version = "0.6.0-rc.2" name = "rtic" [dependencies] -cortex-m = "0.7.0" +cortex-m = "0.7.3" cortex-m-rtic-macros = { path = "macros", version = "0.6.0-rc.2" } rtic-monotonic = "0.1.0-rc.1" rtic-core = "0.3.1" @@ -46,6 +46,10 @@ trybuild = "1" codegen-units = 1 lto = true +[features] +inline-asm = ["cortex-m/inline-asm"] +linker-plugin-lto = ["cortex-m/linker-plugin-lto"] + [workspace] members = [ "macros", diff --git a/examples/lock_cost.rs b/examples/lock_cost.rs new file mode 100644 index 0000000000..cbd2f22665 --- /dev/null +++ b/examples/lock_cost.rs @@ -0,0 +1,79 @@ +//! examples/lock_cost.rs + +#![deny(unsafe_code)] +#![deny(warnings)] +#![no_main] +#![no_std] + +use panic_semihosting as _; + +#[rtic::app(device = lm3s6965)] +mod app { + #[shared] + struct Shared { + shared: u32, + } + + #[local] + struct Local {} + + #[init] + fn init(_: init::Context) -> (Shared, Local, init::Monotonics) { + (Shared { shared: 0 }, Local {}, init::Monotonics()) + } + + #[idle(shared = [shared])] + #[inline(never)] + fn idle(mut cx: idle::Context) -> ! { + cx.shared.shared.lock(|shared| *shared += 1); + + loop { + cortex_m::asm::nop(); + } + } + + #[task(binds = UART0, shared = [shared])] + fn uart0(mut cx: uart0::Context) { + cx.shared.shared.lock(|shared| *shared += 1); + } +} + +// cargo objdump --example lock_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lock_cost.objdump + +// 0000016c : +// 16c: 80 b5 push {r7, lr} +// 16e: 6f 46 mov r7, sp +// 170: 01 78 ldrb r1, [r0] +// 172: 39 b1 cbz r1, 0x184 @ imm = #14 +// 174: 40 f2 00 00 movw r0, #0 +// 178: c2 f2 00 00 movt r0, #8192 +// 17c: 01 68 ldr r1, [r0] +// 17e: 01 31 adds r1, #1 +// 180: 01 60 str r1, [r0] +// 182: 0f e0 b 0x1a4 @ imm = #30 +// 184: 01 21 movs r1, #1 +// 186: 01 70 strb r1, [r0] +// 188: e0 21 movs r1, #224 +// 18a: 81 f3 11 88 msr basepri, r1 +// 18e: 40 f2 00 01 movw r1, #0 +// 192: c2 f2 00 01 movt r1, #8192 +// 196: 0a 68 ldr r2, [r1] +// 198: 01 32 adds r2, #1 +// 19a: 0a 60 str r2, [r1] +// 19c: 00 21 movs r1, #0 +// 19e: 81 f3 11 88 msr basepri, r1 +// 1a2: 01 70 strb r1, [r0] +// 1a4: 00 bf nop +// 1a6: fd e7 b 0x1a4 @ imm = #-6 + +// 000001a8 : +// 1a8: 80 b5 push {r7, lr} +// 1aa: 6f 46 mov r7, sp +// 1ac: 40 f2 00 00 movw r0, #0 +// 1b0: c2 f2 00 00 movt r0, #8192 +// 1b4: 01 68 ldr r1, [r0] +// 1b6: 01 31 adds r1, #1 +// 1b8: 01 60 str r1, [r0] +// 1ba: 00 20 movs r0, #0 +// 1bc: 80 f3 11 88 msr basepri, r0 +// 1c0: 80 bd pop {r7, pc} diff --git a/examples/lockall_cost.rs b/examples/lockall_cost.rs new file mode 100644 index 0000000000..48d4c5cb6c --- /dev/null +++ b/examples/lockall_cost.rs @@ -0,0 +1,81 @@ +//! examples/lockall_cost.rs + +#![deny(unsafe_code)] +#![deny(warnings)] +#![no_main] +#![no_std] + +use panic_semihosting as _; + +#[rtic::app(device = lm3s6965)] +mod app { + #[shared] + struct Shared { + shared: u32, + } + + #[local] + struct Local {} + + #[init] + fn init(_: init::Context) -> (Shared, Local, init::Monotonics) { + (Shared { shared: 0 }, Local {}, init::Monotonics()) + } + + #[idle(shared = [shared])] + #[inline(never)] + fn idle(mut cx: idle::Context) -> ! { + cx.shared.lock(|x| *x.shared += 1); + + loop { + cortex_m::asm::nop(); + } + } + + #[task(binds = UART0, shared = [shared])] + fn uart0(mut cx: uart0::Context) { + cx.shared.lock(|x| *x.shared += 1); + } +} + +// cargo objdump --example lockall_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lockall_cost.ojbdump +// +// The priority cell not optimized out? +// 0000016c : +// 16c: 80 b5 push {r7, lr} +// 16e: 6f 46 mov r7, sp +// 170: 01 78 ldrb r1, [r0] +// 172: 39 b1 cbz r1, 0x184 @ imm = #14 +// 174: 40 f2 00 00 movw r0, #0 +// 178: c2 f2 00 00 movt r0, #8192 +// 17c: 01 68 ldr r1, [r0] +// 17e: 01 31 adds r1, #1 +// 180: 01 60 str r1, [r0] +// 182: 0f e0 b 0x1a4 @ imm = #30 +// 184: 01 21 movs r1, #1 +// 186: 01 70 strb r1, [r0] +// 188: e0 21 movs r1, #224 +// 18a: 81 f3 11 88 msr basepri, r1 +// 18e: 40 f2 00 01 movw r1, #0 +// 192: c2 f2 00 01 movt r1, #8192 +// 196: 0a 68 ldr r2, [r1] +// 198: 01 32 adds r2, #1 +// 19a: 0a 60 str r2, [r1] +// 19c: 00 21 movs r1, #0 +// 19e: 81 f3 11 88 msr basepri, r1 +// 1a2: 01 70 strb r1, [r0] +// 1a4: 00 bf nop +// 1a6: fd e7 b 0x1a4 @ imm = #-6 + +// The lock at highest prio is zero cost +// 000001a8 : +// 1a8: 80 b5 push {r7, lr} +// 1aa: 6f 46 mov r7, sp +// 1ac: 40 f2 00 00 movw r0, #0 +// 1b0: c2 f2 00 00 movt r0, #8192 +// 1b4: 01 68 ldr r1, [r0] +// 1b6: 01 31 adds r1, #1 +// 1b8: 01 60 str r1, [r0] +// 1ba: 00 20 movs r0, #0 +// 1bc: 80 f3 11 88 msr basepri, r0 +// 1c0: 80 bd pop {r7, pc} diff --git a/examples/lockall_soundness3.rs b/examples/lockall_soundness3.rs new file mode 100644 index 0000000000..9e3376d2b9 --- /dev/null +++ b/examples/lockall_soundness3.rs @@ -0,0 +1,40 @@ +//! examples/lockall_soundness3.rs + +#![deny(unsafe_code)] +// #![deny(warnings)] +#![no_main] +#![no_std] + +use panic_semihosting as _; + +#[rtic::app(device = lm3s6965, dispatchers = [GPIOA])] +mod app { + use cortex_m_semihosting::{debug, hprintln}; + + #[shared] + struct Shared { + a: u32, + b: i64, + } + + #[local] + struct Local {} + + #[init] + fn init(_: init::Context) -> (Shared, Local, init::Monotonics) { + foo::spawn().unwrap(); + + (Shared { a: 1, b: 2 }, Local {}, init::Monotonics()) + } + + // when omitted priority is assumed to be `1` + #[task(shared = [a, b])] + fn foo(mut c: foo::Context) { + // let s = c.shared.lock(|s| s); // lifetime error + // hprintln!("a {}", s.a).ok(); + + // let a = c.shared.lock(|foo::Shared { a, b: _ }| a); // lifetime error + // hprintln!("a {}", a).ok(); + debug::exit(debug::EXIT_SUCCESS); // Exit QEMU simulator + } +}