Comments (7)
Looking closer at the implementation. The "resource_proxy" could be created for each task invocation, meaning that the OH of an extra field would be only a stack allocation, never stored on the (static heap), so its not really an issue (at least not as much as a static allocation).
from rfcs.
Another positive implication is that this approach can be seen as a limited soundness run-time verification. I.e., if the borrow checker somehow would be broken, at least the we would catch this by a panic. This is not a very strong guarantee though, since it only checks the case of nested re-locking, not other soundness issues that would be caused by a broken borrow checker. However, if we store the locked
with the actual resource (stored statically), then we would actually have a run-time verification of soundness cross tasks. This however brings OH as the checks would be done for each resource lock (but that might be a price worth to pay for safety/security critical applications).
Notably, the big difference in between FreeRTOS and SafeRTOS, is that the latter is certified to standards, automotive etc., by run-time checking/verification (and crippling API functionality/surface). In our case the OH would be very small and predictable (and we do not need to cripple API functionality/surface), since the API is sound by design. The only potentially unsound operations in RTIC reside in the small and well defined blocks of unsafe code.
from rfcs.
There is now a testing branch for the aforementioned approach.
cortex-m-rtic/immutable_resource_proxies
, and corresponding
rtic-core/immutable_resource_proxies
.
The Mutex trait no longer takes an &mut self, but the more relaxed &self.
Previously, Exclusive implemented the Mutex trait, I removed this for the time being, unclear how and if we want this at all. Exlusive is already an &mut, we would temporarily need to downgrade mutability to fit the Mutex trait, and restore it for the closure application. Not sure if a transmute could be used to restore the mutability, or if we could do it in a cleaner way. (RefCell hands out &mut T, so maybe looking there could give some hint, or maybe I'm missing the obvious...).
In any case, the Boolean locked
is handled by a Cell, initialized for each sequential context (task invocation) to false
. The auto generated code implementing lock, now looks like this.
impl<'a> rtic::Mutex for resources::shared<'a> {
type T = u32;
#[inline(always)]
fn lock<R>(&self, f: impl FnOnce(&mut u32) -> R) -> R {
#[doc = r" Priority ceiling"]
const CEILING: u8 = 2u8;
if unsafe { self.get_locked() } {
::core::panicking::panic("Resource locked in sequential context");
};
unsafe {
self.set_locked(true);
}
let r = unsafe {
rtic::export::lock(
&mut shared,
self.priority(),
CEILING,
lm3s6965::NVIC_PRIO_BITS,
f,
)
};
unsafe {
self.set_locked(false);
}
r
}
}
self
here is the resource proxy. We check if the lock is taken, if so we panic. Else we claim the lock (set_locked(true)
) do the real hw lock (here we execute f
), and restore the locked state to false after returning.
The lock3
example ( cargo run --example lock3 --target thumbv7m-none-eabi
), all is well. Behaves line the original lock
example, as there are no re-locking of resources.
The lock4
example ( cargo run --example lock4 --target thumbv7m-none-eabi
), blows up at run-time as expected.
A
B - shared = 1
panicked at 'Resource locked in sequential context', examples/lock4.rs:12:1
Source:
c.resources.shared.lock(|shared| {
// data can only be modified within this critical section (closure)
*shared += 1;
// GPIOB will *not* run right now due to the critical section
rtic::pend(Interrupt::GPIOB);
hprintln!("B - shared = {}", *shared).unwrap();
c.resources.shared.lock(|_shared| {}); // here we try to re-lock
I tested this both in dev and release mode.
It will be interesting to see how well LLVM copes with the added complexity regarding optimization, and if not what a realistic overhead would be.
The gpioa
code of lock2.rs
compiles to:
000000f0 GPIOA:
f0: push {r7, lr}
f2: mov r7, sp
f4: movs r0, #192
f6: bl #336
fa: movw r0, #0
fe: movt r0, #8192
102: ldr r1, [r0]
104: adds r1, #1
106: str r1, [r0]
108: movw r0, #57856
10c: movs r1, #2
10e: movt r0, #57344
112: str r1, [r0]
114: movs r0, #224
116: bl #304
11a: movs r1, #38
11c: movs r0, #24
11e: movt r1, #2
122: bl #270
126: movs r0, #0
128: pop.w {r7, lr}
12c: b.w #282 <__basepri_w>
This code includes pending a task and exiting the simulator. A more realistic example would be lock2_miniamal.rs
.
Here we get:
000000f0 GPIOA:
f0: push {r7, lr}
f2: mov r7, sp
f4: movs r0, #192
f6: bl #324
fa: movw r0, #0
fe: movt r0, #8192
102: ldr r1, [r0]
104: adds r1, #1
106: str r1, [r0]
108: movs r0, #224
10a: bl #304
10e: movs r0, #0
110: pop.w {r7, lr}
114: b.w #294 <__basepri_w>
As a comparison. The same example under vanilla RTIC, gives:
000000f0 GPIOA:
f0: push {r7, lr}
f2: mov r7, sp
f4: movs r0, #192
f6: bl #324
fa: movw r0, #0
fe: movt r0, #8192
102: ldr r1, [r0]
104: adds r1, #1
106: str r1, [r0]
108: movs r0, #224
10a: bl #304
10e: movs r0, #0
110: pop.w {r7, lr}
114: b.w #294 <__basepri_w>
At least for simple examples, there is Zero OH inferred by the immutable_resource_proxies, LLVM was able to remove all reference counting, setting, clearing the locked
Cell.
As its passed 2AM, I will rest at this.
Feel free to experiment with the relaxed resource proxies, I look forward to further discussions, evaluations etc. I hope it will play nicely with other developments, like goodby exclusive, lock-optimisation, etc.
from rfcs.
Closed by mistake ...
from rfcs.
By the way, the bl, is calling the read/write of BASEPRI, the cargo obdump lost the named symbols to external code somehow in the dissasembly. (Should have run with the inline asm instead on nightly, then you see exactly what's going on.) We should have a closer look at the fences, not entirely sure they are correct/sufficient.
from rfcs.
Update.
The immutable_resource_proxies
branches of rtic-core
and cortex-m-rtic
now includes Exclusive
following the same patterns as Mutex
(i.e., panic on re-lock).
Currently, RTIC hands out &mut T, for resources exclusively owned. These can now be wrapped into an Exclusive<&'a mut T>
data structure, supporting both Deref, DerefMut and Mutex lock. Thus possible to pass on to external code (e.g., HAL implementations) that internally lock the resources where needed.
In this way, we can support a symmetric API. In the future we might choose to hand out Exclusive
instead of `&mut T. This should also work well with #30, allowing do explicitly state the set Exclusive resources (and hence direct Deref/DerefMut, will never break).
The examples, lock5..lock9 demonstrates various safety features.
No OH measurements have been done, but as being less complex than general Mutex resource proxies, LLVM will have an easier task to optimize away the underlying Cell and its counterparts.
The panics could be be implemented as a linked library (non present) thus any such calls could be spotted at compile time.
A re-locking, would cause an linking error.
❯ cargo run --example lock8 --target thumbv7m-none-eabi --release
Compiling rtic-core v0.3.0 (/home/pln/rust/grepit/rtic-core)
Compiling cortex-m-rtic v0.5.3 (/home/pln/rust/grepit/cortex-m-rtic)
error: linking with `rust-lld` failed: exit code: 1
|
= ...88J/libcortex_m-19f1dd21ecd80693.rlib" "--end-group" "/home/pln/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/thumbv7m-none-eabi/lib/libcompiler_builtins-fa0816b847f38cf8.rlib" "-Tlink.x" "-Bdynamic"
= note: rust-lld: error: undefined symbol: re_lock
>>> referenced by lock8.cmw4tywi-cgu.0
>>>
Notice, this is a poor man's solution, but gives a static guarantee that the program will never reference the external re-lock
functions (here LLVM has proven the program free of re-locks). Of course this works only in realease builds, and can also show false positives (i.e., LLVM is note able to prove re-lock freedom, but the program would never run into the re-locks at run-time. (So a correct program could be rejected). So it can be seen as an opt-in (or maybe opt-out) functionality, and provided behind a feature. This is currently not implemented though.
from rfcs.
Update.
As a proof of concept, there is now a feature link_fail.
Compiling cortex-m-rtic v0.5.3 (/home/pln/rust/grepit/cortex-m-rtic)
error: linking with `rust-lld` failed: exit code: 1
|
= note: "rust-lld" "-flavor" "gnu" "-L" "/home/pln/.rustup/toolchains...fa0816b847f38cf8.rlib" "-Tlink.x" "-Bdynamic"
= note: rust-lld: error: undefined symbol: re_lock
>>> referenced by lock8.9vno1x9n-cgu.0
>>> /home/pln/rust/grepit/cortex-m-rtic/target/thumbv7m-none-eabi/release/examples/lock8-6bf696e4b09f1abf.lock8.9vno1x9n-cgu.0.rcgu.o:(GPIOC)
While
cargo run --example lock8 --target thumbv7m-none-eabi --release
Finished release [optimized] target(s) in 0.02s
Running `qemu-system-arm -cpu cortex-m3 -machine lm3s6965evb -nographic -semihosting-config enable=on,target=native -kernel target/thumbv7m-none-eabi/release/examples/lock8`
A
B - shared = 1
panicked at 'Re-lock of Exclusive resource', /home/pln/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/macros/mod.rs:34:9
I have not implemented link_fail for the Mutex panics, but it could be done in a similar fashion. Not sure the name link_fail
is the best, perhaps link_fail_on_re-lock
would be more descriptive, but I got lazy!
from rfcs.
Related Issues (20)
- Memory Lane - Zero Cost Logging with deferred formatting HOT 4
- #[init()] functions should provide a CriticalSection HOT 5
- [tracking issue] 1.0 (previously 0.6) push HOT 7
- SeqCst around critical sections.
- Spawn and message queues. HOT 1
- Synchroneous task
- Emulation of Monotonic Timers
- Resource handling take 2 HOT 1
- RTIC on RISC-V - roadmap / tasks HOT 1
- Tracing RTIC tasks over ITM HOT 4
- Async idle
- Exporting app description during compliation for tracing purposes? HOT 2
- Lockall API HOT 12
- Add support for the async functions HOT 1
- Soundness of RTIC
- Fine grained concurrency on thumbv6m (no BASEPRI). HOT 1
- Modular RTIC HOT 2
- Type based Layout for Rust RTIC
- rtic-sync: DynSender and DynReceiver HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from rfcs.