"Extra Sections" example is potentially unsound

[jamesmunns]

In the cortex-m-rt docs, the extra sections example shows the definition of a zero-initialized static mut array in a section outside of RAM.

I believe this to be unsound, and difficult, if not impossible, to use totally soundly.

The CRT is required to initialize all statics, either to their default value (in .data), or to zero (in .bss). cortex-m-rt explicitly only performs initialization for data and bss sections in the RAM region, meaning the CCRAM must be considered to be uninitialized in the example as currently written.

At the very least if we include an example like this, we should discuss this deficiency, and state that pre_init must be used to guarantee that the static is initialized at the start of the program.

I personally am of the opionion that we cannot soundly perform this initialization in a pre_init in Rust, as that means that Rust code is running without all statics initialized, which violates the agreement the language makes with the platform environment.

This argument is part of why we switched to an assembly CRT, rather than the previously Rust-based init sequence.

[jamesmunns]

@Dirbaio noted (and I agree) that changing it to:

#[link_section=".ccmram.BUFFERS"]
static mut BUF: MaybeUninit<[u8; 1024]> = MaybeUninit::uninit();

alleviates the majority of the UB (though, still recommends static mut which is still hard to use right IMO, but is not "plainly always UB" anymore)

[thejpster]

Can you soundly perform the initialisation in pre_init in assembly?

[jamesmunns]

Can you soundly perform the initialisation in pre_init in assembly?

In my opinion, yes.

__pre_init is the actual ABI symbol for the function called BEFORE init AND BEFORE control transfer to Rust code. See here.

Assembly has no "abstract machine" requirements - so there isn't any soundness requirement here.

I'm not certain we could use inline assembly within a rust pre_init function, e.g. using the #[pre_init] macro, I believe it must be a global asm definition (or externally assembled file that defines the underlying __pre_init symbol).

edit: I was incorrect that __pre_init occured AFTER regular data/bss init, it actually takes place before either of those.

[adamgreig]

I've updated the documentation in #525 to specify that you have to use MaybeUninit or pre_init, though I'd be open to adding a more useful/complete example too.