From c0e9da864242f6555220fe33ad677dd6ec4f410e Mon Sep 17 00:00:00 2001 From: Per Lindgren Date: Mon, 25 Oct 2021 10:58:58 +0200 Subject: [PATCH] soundness and cost --- examples/lock_cost.rs | 74 ++++++++++++++++------------------------ examples/lockall_cost.rs | 74 ++++++++++++++++------------------------ 2 files changed, 59 insertions(+), 89 deletions(-) diff --git a/examples/lock_cost.rs b/examples/lock_cost.rs index cbd2f22665..fe07c93376 100644 --- a/examples/lock_cost.rs +++ b/examples/lock_cost.rs @@ -22,58 +22,44 @@ mod app { (Shared { shared: 0 }, Local {}, init::Monotonics()) } - #[idle(shared = [shared])] - #[inline(never)] - fn idle(mut cx: idle::Context) -> ! { + #[task(binds = GPIOA, shared = [shared])] + fn low(mut cx: low::Context) { cx.shared.shared.lock(|shared| *shared += 1); - - loop { - cortex_m::asm::nop(); - } } - #[task(binds = UART0, shared = [shared])] - fn uart0(mut cx: uart0::Context) { + #[task(binds = GPIOB, priority = 2, shared = [shared])] + fn high(mut cx: high::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 : +// +// Zero-Cost implementations: +// 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 +// 170: c0 20 movs r0, #192 +// 172: 80 f3 11 88 msr basepri, r0 +// 176: 40 f2 00 00 movw r0, #0 +// 17a: c2 f2 00 00 movt r0, #8192 +// 17e: 01 68 ldr r1, [r0] +// 180: 01 31 adds r1, #1 +// 182: 01 60 str r1, [r0] +// 184: e0 20 movs r0, #224 +// 186: 80 f3 11 88 msr basepri, r0 +// 18a: 00 20 movs r0, #0 +// 18c: 80 f3 11 88 msr basepri, r0 +// 190: 80 bd pop {r7, pc} -// 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} +// 00000192 : +// 192: 80 b5 push {r7, lr} +// 194: 6f 46 mov r7, sp +// 196: 40 f2 00 01 movw r1, #0 +// 19a: ef f3 11 80 mrs r0, basepri +// 19e: c2 f2 00 01 movt r1, #8192 +// 1a2: 0a 68 ldr r2, [r1] +// 1a4: 01 32 adds r2, #1 +// 1a6: 0a 60 str r2, [r1] +// 1a8: 80 f3 11 88 msr basepri, r0 +// 1ac: 80 bd pop {r7, pc} diff --git a/examples/lockall_cost.rs b/examples/lockall_cost.rs index 48d4c5cb6c..d3a5a8179c 100644 --- a/examples/lockall_cost.rs +++ b/examples/lockall_cost.rs @@ -22,60 +22,44 @@ mod app { (Shared { shared: 0 }, Local {}, init::Monotonics()) } - #[idle(shared = [shared])] - #[inline(never)] - fn idle(mut cx: idle::Context) -> ! { + #[task(binds = GPIOA, shared = [shared])] + fn low(mut cx: low::Context) { cx.shared.lock(|x| *x.shared += 1); - - loop { - cortex_m::asm::nop(); - } } - #[task(binds = UART0, shared = [shared])] - fn uart0(mut cx: uart0::Context) { + #[task(binds = GPIOB, priority = 2, shared = [shared])] + fn high(mut cx: high::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 : +// Zero-Cost implementations: +// 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 +// 170: c0 20 movs r0, #192 +// 172: 80 f3 11 88 msr basepri, r0 +// 176: 40 f2 00 00 movw r0, #0 +// 17a: c2 f2 00 00 movt r0, #8192 +// 17e: 01 68 ldr r1, [r0] +// 180: 01 31 adds r1, #1 +// 182: 01 60 str r1, [r0] +// 184: e0 20 movs r0, #224 +// 186: 80 f3 11 88 msr basepri, r0 +// 18a: 00 20 movs r0, #0 +// 18c: 80 f3 11 88 msr basepri, r0 +// 190: 80 bd pop {r7, pc} -// 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} +// 00000192 : +// 192: 80 b5 push {r7, lr} +// 194: 6f 46 mov r7, sp +// 196: 40 f2 00 01 movw r1, #0 +// 19a: ef f3 11 80 mrs r0, basepri +// 19e: c2 f2 00 01 movt r1, #8192 +// 1a2: 0a 68 ldr r2, [r1] +// 1a4: 01 32 adds r2, #1 +// 1a6: 0a 60 str r2, [r1] +// 1a8: 80 f3 11 88 msr basepri, r0 +// 1ac: 80 bd pop {r7, pc}