Skip to content

Concern about soundness of placement of stack memory #6

Open
@RalfJung

Description

@RalfJung

@japaric I read your post at https://blog.japaric.io/microamp/ with great interest. Most of that embedded stuff is very foreign to me, and I continue to be amazed by your ways to provide safe abstractions in this world. :)

That said, I have a concern about some of the things you describe there. Specifically:

The stack will be placed at the end of aliased BTCM1 (0x3_0000). Note that the stack grows downwards, towards smaller addresses.

References to stack variables can not be sent to a different core because they have non-static lifetimes and to place a value in a static variable it must only contain static lifetimes ( there’s an implicit T: 'static bound on all static variables).

I am not convinced that the latter is true -- that you will never see references to stack variables if you restrict yourself to T: 'static.

The first, maybe silly example is the following function:

pub fn make_static<T>(x: &T, f: impl FnOnce(&'static T)) -> ! {
    // Casting away the lifetime is okay because we know there is
    // a loop there that makes sure the reference remains valid forever.
    f(unsafe { &*(x as *const T)});
    loop {}
}

I think this function is safe in the sense that it doesn't break the type system and could conceivably be provided by a library. I even have a formal proof that this is compatible with our formal model of the type system.

But of course if a μAMP program uses this function, it could communicate a stack reference to another core, and suddenly the pointer is using the wrong address space.

Now this may sound somewhat artificial, but that doesn't make it less of a problem, at least in principle. We have two unsafely implemented abstractions (make_static and μAMP) which seem fine in isolation, but go bad when used together, and it is not clear "who is right". (Also from a formal perspective, I have no clear idea what is wrong with the function above that would make a correctness proof not go through -- you are using 'static in a way that means much more than just "a lifetime that goes on forever".)

I also am not sure if this example is the only problem: with intrusive collections, we can have elements in a collection that live shorter than the collection. This is certainly challenging to get right with concurrency in mind, but I see no fundamental reason why we couldn't have an intrusive concurrent collection where thread A can add elements (that will automatically remove themselves when the stack gets popped) and thread B can access them while they are in there.

So, generally, the rule you are postulating that T: 'static cannot refer to any thread's stack, is not something that necessarily has to be true, it would be a new piece in Rust's safety contract and I think it is in conflict with some legitimate uses (intrusive collections in particular, where the entire point is that you can add elements to a collection without showing that the elements outlive the collection).

I am curious about your thoughts on this. :)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions