soundness and cost

This commit is contained in:
Per Lindgren 2021-10-25 10:58:58 +02:00 committed by Henrik Tjäder
parent a6aa28b277
commit c0e9da8642
2 changed files with 59 additions and 89 deletions

View file

@ -22,58 +22,44 @@ mod app {
(Shared { shared: 0 }, Local {}, init::Monotonics()) (Shared { shared: 0 }, Local {}, init::Monotonics())
} }
#[idle(shared = [shared])] #[task(binds = GPIOA, shared = [shared])]
#[inline(never)] fn low(mut cx: low::Context) {
fn idle(mut cx: idle::Context) -> ! {
cx.shared.shared.lock(|shared| *shared += 1); cx.shared.shared.lock(|shared| *shared += 1);
loop {
cortex_m::asm::nop();
}
} }
#[task(binds = UART0, shared = [shared])] #[task(binds = GPIOB, priority = 2, shared = [shared])]
fn uart0(mut cx: uart0::Context) { fn high(mut cx: high::Context) {
cx.shared.shared.lock(|shared| *shared += 1); cx.shared.shared.lock(|shared| *shared += 1);
} }
} }
// cargo objdump --example lock_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lock_cost.objdump // cargo objdump --example lock_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lock_cost.objdump
//
// 0000016c <lock_cost::app::idle::he8e6b27e7333515d>: // Zero-Cost implementations:
// 0000016c <GPIOA>:
// 16c: 80 b5 push {r7, lr} // 16c: 80 b5 push {r7, lr}
// 16e: 6f 46 mov r7, sp // 16e: 6f 46 mov r7, sp
// 170: 01 78 ldrb r1, [r0] // 170: c0 20 movs r0, #192
// 172: 39 b1 cbz r1, 0x184 <lock_cost::app::idle::he8e6b27e7333515d+0x18> @ imm = #14 // 172: 80 f3 11 88 msr basepri, r0
// 174: 40 f2 00 00 movw r0, #0 // 176: 40 f2 00 00 movw r0, #0
// 178: c2 f2 00 00 movt r0, #8192 // 17a: c2 f2 00 00 movt r0, #8192
// 17c: 01 68 ldr r1, [r0] // 17e: 01 68 ldr r1, [r0]
// 17e: 01 31 adds r1, #1 // 180: 01 31 adds r1, #1
// 180: 01 60 str r1, [r0] // 182: 01 60 str r1, [r0]
// 182: 0f e0 b 0x1a4 <lock_cost::app::idle::he8e6b27e7333515d+0x38> @ imm = #30 // 184: e0 20 movs r0, #224
// 184: 01 21 movs r1, #1 // 186: 80 f3 11 88 msr basepri, r0
// 186: 01 70 strb r1, [r0] // 18a: 00 20 movs r0, #0
// 188: e0 21 movs r1, #224 // 18c: 80 f3 11 88 msr basepri, r0
// 18a: 81 f3 11 88 msr basepri, r1 // 190: 80 bd pop {r7, pc}
// 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 <lock_cost::app::idle::he8e6b27e7333515d+0x38> @ imm = #-6
// 000001a8 <UART0>: // 00000192 <GPIOB>:
// 1a8: 80 b5 push {r7, lr} // 192: 80 b5 push {r7, lr}
// 1aa: 6f 46 mov r7, sp // 194: 6f 46 mov r7, sp
// 1ac: 40 f2 00 00 movw r0, #0 // 196: 40 f2 00 01 movw r1, #0
// 1b0: c2 f2 00 00 movt r0, #8192 // 19a: ef f3 11 80 mrs r0, basepri
// 1b4: 01 68 ldr r1, [r0] // 19e: c2 f2 00 01 movt r1, #8192
// 1b6: 01 31 adds r1, #1 // 1a2: 0a 68 ldr r2, [r1]
// 1b8: 01 60 str r1, [r0] // 1a4: 01 32 adds r2, #1
// 1ba: 00 20 movs r0, #0 // 1a6: 0a 60 str r2, [r1]
// 1bc: 80 f3 11 88 msr basepri, r0 // 1a8: 80 f3 11 88 msr basepri, r0
// 1c0: 80 bd pop {r7, pc} // 1ac: 80 bd pop {r7, pc}

View file

@ -22,60 +22,44 @@ mod app {
(Shared { shared: 0 }, Local {}, init::Monotonics()) (Shared { shared: 0 }, Local {}, init::Monotonics())
} }
#[idle(shared = [shared])] #[task(binds = GPIOA, shared = [shared])]
#[inline(never)] fn low(mut cx: low::Context) {
fn idle(mut cx: idle::Context) -> ! {
cx.shared.lock(|x| *x.shared += 1); cx.shared.lock(|x| *x.shared += 1);
loop {
cortex_m::asm::nop();
}
} }
#[task(binds = UART0, shared = [shared])] #[task(binds = GPIOB, priority = 2, shared = [shared])]
fn uart0(mut cx: uart0::Context) { fn high(mut cx: high::Context) {
cx.shared.lock(|x| *x.shared += 1); cx.shared.lock(|x| *x.shared += 1);
} }
} }
// cargo objdump --example lockall_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lockall_cost.ojbdump // cargo objdump --example lockall_cost --target thumbv7m-none-eabi --release --features inline-asm -- --disassemble > lockall_cost.ojbdump
// //
// The priority cell not optimized out? // Zero-Cost implementations:
// 0000016c <lockall_cost::app::idle::he14f20fbca3d3928>: // 0000016c <GPIOA>:
// 16c: 80 b5 push {r7, lr} // 16c: 80 b5 push {r7, lr}
// 16e: 6f 46 mov r7, sp // 16e: 6f 46 mov r7, sp
// 170: 01 78 ldrb r1, [r0] // 170: c0 20 movs r0, #192
// 172: 39 b1 cbz r1, 0x184 <lockall_cost::app::idle::he14f20fbca3d3928+0x18> @ imm = #14 // 172: 80 f3 11 88 msr basepri, r0
// 174: 40 f2 00 00 movw r0, #0 // 176: 40 f2 00 00 movw r0, #0
// 178: c2 f2 00 00 movt r0, #8192 // 17a: c2 f2 00 00 movt r0, #8192
// 17c: 01 68 ldr r1, [r0] // 17e: 01 68 ldr r1, [r0]
// 17e: 01 31 adds r1, #1 // 180: 01 31 adds r1, #1
// 180: 01 60 str r1, [r0] // 182: 01 60 str r1, [r0]
// 182: 0f e0 b 0x1a4 <lockall_cost::app::idle::he14f20fbca3d3928+0x38> @ imm = #30 // 184: e0 20 movs r0, #224
// 184: 01 21 movs r1, #1 // 186: 80 f3 11 88 msr basepri, r0
// 186: 01 70 strb r1, [r0] // 18a: 00 20 movs r0, #0
// 188: e0 21 movs r1, #224 // 18c: 80 f3 11 88 msr basepri, r0
// 18a: 81 f3 11 88 msr basepri, r1 // 190: 80 bd pop {r7, pc}
// 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 <lockall_cost::app::idle::he14f20fbca3d3928+0x38> @ imm = #-6
// The lock at highest prio is zero cost // 00000192 <GPIOB>:
// 000001a8 <UART0>: // 192: 80 b5 push {r7, lr}
// 1a8: 80 b5 push {r7, lr} // 194: 6f 46 mov r7, sp
// 1aa: 6f 46 mov r7, sp // 196: 40 f2 00 01 movw r1, #0
// 1ac: 40 f2 00 00 movw r0, #0 // 19a: ef f3 11 80 mrs r0, basepri
// 1b0: c2 f2 00 00 movt r0, #8192 // 19e: c2 f2 00 01 movt r1, #8192
// 1b4: 01 68 ldr r1, [r0] // 1a2: 0a 68 ldr r2, [r1]
// 1b6: 01 31 adds r1, #1 // 1a4: 01 32 adds r2, #1
// 1b8: 01 60 str r1, [r0] // 1a6: 0a 60 str r2, [r1]
// 1ba: 00 20 movs r0, #0 // 1a8: 80 f3 11 88 msr basepri, r0
// 1bc: 80 f3 11 88 msr basepri, r0 // 1ac: 80 bd pop {r7, pc}
// 1c0: 80 bd pop {r7, pc}