From 9afe9a47c011e40112ee6e8cd6b362a9a86016c0 Mon Sep 17 00:00:00 2001 From: Jorge Aparicio Date: Sun, 14 Apr 2019 22:27:46 +0200 Subject: [PATCH] [BEAM] Unsynchronized access to a shared `static mut` variable --- .../embedded/static-unsynchronized.md | 82 +++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 active_discussion/embedded/static-unsynchronized.md diff --git a/active_discussion/embedded/static-unsynchronized.md b/active_discussion/embedded/static-unsynchronized.md new file mode 100644 index 00000000..8fda01ac --- /dev/null +++ b/active_discussion/embedded/static-unsynchronized.md @@ -0,0 +1,82 @@ +# Unsynchronized access to a shared `static mut` variable + +Sometimes interrupt handlers need to share state. This is done using a static +variable. We claim that *no* synchronization is needed to access the shared +static variable if the interrupt handlers run at the same priority. + +Note that: + +- The programs in this document target the [Basic Embedded Abstract Machine + (BEAM)][beam]. Please become familiar with the linked specification before you + read the rest of this document. + +[beam]: https://github.com/rust-lang/unsafe-code-guidelines/pull/111 + +- In these programs we assume that [rust-lang/rfcs#2585][rfc2585] has been + accepted and implemented. + +[rfc2585]: https://github.com/rust-lang/rfcs/pull/2585 + +## Example program + +Consider this program + +``` rust +#![no_std] + +#[no_mangle] +unsafe fn main() -> ! { + unsafe { + asm!("ENABLE_INTERRUPTS" : : : : "volatile"); + } + + loop { + // .. any safe code .. + } +} + +static mut X: u128 = 0; + +#[no_mangle] +unsafe fn INTERRUPT0() { + let x: &mut u128 = unsafe { &mut X }; + + // .. any safe code .. +} + +#[no_mangle] +unsafe fn INTERRUPT1() { + let x: &mut u128 = unsafe { &mut X }; + + // .. any safe code .. +} +``` + +Note that "any safe code" can *not* call `main`, `INTERRUPT0` or `INTERRUPT1` +(because they are `unsafe` functions), use `asm!` or access registers. + +**Claim**: this program is well-defined / sound. Rust aliasing rules are +preserved because no preemption is possible between `INTERRUPT0` and +`INTERRUPT1`. + +In fact, I would say that this program (ignoring `main`) is equivalent to this +code, which is sound (and reminds me of cooperative scheduling): + +``` rust +let mut X: u128 = 0; + +loop { + sleep(random()); + + if random() { + INTERRUPT0(&mut X); + } else if random() { + INTERRUPT1(&mut X); + } +} +``` + +## Questions + +- Can this program be misoptimized given that the compiler has *no* information + about `INTERRUPT0` and `INTERRUPT1` executing "cooperatively"?