The Basic Embedded Abstract Machine (BEAM) and `unsafe` embedded code #111

japaric · 2019-04-14T20:39:45Z

Hello UCG WG. I'm @japaric from the Embedded WG.

In embedded Rust, and specially in Rust code that runs on (single-core)
microcontrollers, we use unsafe code in (rather) unusual ways (spoilers: we
use static mut variables, a lot), which we believe to be safe and sound. I'd
like to discuss the soundness of these patterns (i.e. whether the compiler /
LLVM will mis-optimize them or not) with the UCG WG so I'll create (roughly) one
discussion PR per pattern and list them at the end of this comment. But before
you click on those PRs please read the rest of this comment.

Concurrency on microcontrollers looks quite different from the OS-thread
concurrency model one uses in non-no_std programs and even among
microcontrollers details around how one does concurrency vary a bit between
architectures. So to make sure we are all on the same page when discussing
unsafe embedded Rust code I'm specifying in this PR an abstract
machine that's representative of the microcontrollers one can run Rust
code on. I'll call this abstract machine: the Basic Embedded Abstract Machine
(BEAM).

Rendered specification

Assuming that I do a good job, this specification should be all you need to know
about microcontrollers to discuss the soundness of the unsafe patterns listed
below. All the PRs have code examples that target the BEAM.

[BEAM] Runtime initialization of static variables #112 Runtime initialization of static variables
[BEAM] Unsynchronized access to a shared static mut variable #113 Unsynchronized access to a shared static mut variable
[BEAM] Critical sections #114 Critical sections
[BEAM] &'static mut references to static variables and LLVM noalias #115 &'static mut references to static variables and LLVM noalias
[BEAM] The meaning of Send and Sync in the context of interrupt handlers #116 The meaning of Send and Sync in the context of interrupt handlers

gnzlbg · 2019-04-14T20:47:05Z

At this rate I think we are probably months or years away from being at a point where starting to discuss these issues would make sense.

I don’t think it makes sense to delay a layout / validity MVP with any of this.

comex · 2019-04-15T10:25:13Z

Hmm, the name collides with the BEAM virtual machine that powers Erlang.

RalfJung · 2019-05-05T13:50:02Z

Thanks @japaric for posting this! When you asked about some discussion I expected a few issues with questions, not several books worth of content. oO

I don’t think it makes sense to delay a layout / validity MVP with any of this.

I don't think @japaric proposed that. :)

But I agree that it seems hard to make hard statements about using Rust in a particular environment before we have set in stone anything about the semantics of the language.^^

However, just like I am experimenting with a Stacked Borrows spec here without that expressing even the consent of the UCG yet, and focusing only on a narrow aspect of Rust program execution while ignoring the (not-yet-specified) rest, it seems fine to me to do the same with BEAM. I am just afraid you overwhelmed us thoroughly, @japaric -- we barely have the resources to keep our discussions going and have a hard time finding people to do write-ups, so it will be hard to muster the resources to properly review 6 PRs. Is there a way you could stretch this over time so that we don't feel like we are drowning in content?^^

RalfJung · 2019-05-05T13:53:10Z

wip/beam-spec.md

+as follows: when an interrupt *signal* arrives the processor suspends the
+execution of the current function and jumps to a special subroutine known as the
+interrupt *handler*. When this subroutine returns the processors resumes the
+execution of the function that was preempted by the interrupt handler.)


I think this should not be just a parenthetical. This is important background for people not familiar with the area.

This explains the "signal" and "interrupt handler" concepts. I think it might be worth it to also introduce here "masking" and "priority", since these terms are used below a couple of times before being introduced.

RalfJung · 2019-05-05T13:53:28Z

wip/beam-spec.md

+execution of the function that was preempted by the interrupt handler.)
+
+- BEAM's interrupt handling capabilities can be summarized as: prioritization of
+  interrupts, individual interrupt masking and global interrupt masking.


Could you explain what these capabilities mean?

Oh, I now see you do that later. The way this gets mentioned in an enumeration here made me think you expect the reader to understand what all of this means -- you go on with the next enumeration item, so the previous one is done.

RalfJung · 2019-05-05T13:54:20Z

wip/beam-spec.md

+
+- When the BEAM starts, all interrupts are *disabled*, *unmasked* and are
+  configured with an initial *priority* of `1`; and the *running priority* of
+  the system is set to `0`.


What is the difference between "disabled" and "masked"? I'd have thought these are the same thing...

It seems like you have some kind of per-interrupt state machine in mind here, with states like disabled, pending, masked, ...? If yes, then please write down that state machine explicitly.

RalfJung · 2019-05-05T13:57:15Z

wip/beam-spec.md

+            }
+        }
+    }
+}


This would have been really useful further up when I tried to figure out what all that English text means.

RalfJung · 2019-05-05T14:00:27Z

wip/beam-spec.md

+meant to improve your understanding of the above specification but they are not
+part of the specification itself.
+
+In all these examples the BEAM goes from state A, to B, to C, etc.


This sentence makes no sense unless one has already read an example. Maybe announce in advance there will be comments detailing the states the machine can be in?

RalfJung · 2019-06-13T16:15:06Z

@japaric how do we proceed with this? We'd like to get our PR list cleaned up a bit here. ;)

My proposal is to merge this PR here, ideally after applying some of the feedback we gave above. The other PRs are, as you stated, more discussions than resolutions. so I think they should be turned into issues referenced the WIP document here. We can have a label collecting those issues. This is similar to what we do for Stacked Borrows, which also has a WIP document and several open issues/discussions.

gnzlbg · 2019-06-13T16:36:22Z

wip/beam-spec.md

+    }
+}
+```
+


From the text, it is obvious that preemption can occur in the middle of a function, but I was wondering, at which precise granularity can preemption occur ? Or maybe in different words, what are the "atomic" operations of the abstract machine, during which preemption does not occur ?

For example. consider a single instruction like add in an architecture in which it returns a result in one register, and sets a flag in another register indicating whether the add overflowed. Now consider two arguments for which the add overflows. Could the execution of this instruction be preempted after setting the flag register but before writing the result value? That would allow an interrupt handler to remove the overflow flag, and would prevent the interrupted code from knowing that an overflow happened.

This should not be able to happen, that is, such an add operation that modifies multiple registers would be non-preemptable in the middle of its execution. Or in other words, preemption can only happen across these non-preemptable operations.

I don't really know what's the best way to declare / specify at which granularity can pre-emption happen, but this should be specified somewhere.

For example, in a different less-useful abstract machine, preemption could only be allowed across, for example, function calls (e.g. in BEAM, this would be like setting the priority to 255 when entering every function, and setting it to 0 right before calling a function, such that the only window in which this can happen, is right before entering the next function).

consider a single instruction like add in an architecture in which it returns a result in one register, and sets a flag in another register indicating whether the add overflowed. Now consider two arguments for which the add overflows. Could the execution of this instruction be preempted after setting the flag register but before writing the result value?

I'm not sure about specifics of embedded hardware, but this seems to be pretty unlikely behavior.

CPU ISAs are normally specified in terms of instructions following each other in-order and changing observable architectural state like registers atomically (unless explicitly said otherwise).

Even if CPU works in out-of-order fashion internally, instructions as defined by ISA are still retired in-order and maintain architectural state at retirement.

That's why taking of interrupts/exceptions is also tied to instruction retirement, and the first instruction of exception handler will see consistent state left by the previous retired instruction (this is called "precise interrupts").

TLDR: the granularity is macro instructions as defined by respective CPU's ISA.

@petrochenkov Yeah, I guess something like MIR or LLVM-IR, where add_with_overflow and similar are actual intrinsics, would be more interesting to consider than an actual ISA. MIR intrinsics are going to get lowered into multiple CPU instruction, and preemption can happen within them.

This is getting into the interaction of hardware-level interrupts and language abstract machines... that's a hard problem.^^ This is why C says that in an interrupt, the content of all memory is unspecified except for volatile and atomic stuff. We likely need something similar.

gnzlbg · 2019-06-13T16:42:37Z

wip/beam-spec.md

+unsafe fn INTERRUPT1() {
+    // State D (RUNNING_PRIORITY = 1, PEND_INTERRUPT = 0b0000_0000)
+}
+```


From reading the examples, it might be clearer to use VolatileCell instead of UnsafeCell for the registers.

gnzlbg · 2019-06-13T16:53:02Z

wip/beam-spec.md

+  `INTERRUPT1`, all the way to `INTERRUPT7`.
+
+- The signature of all interrupt handlers must be `[unsafe] fn()`. That is these
+  handlers don't take arguments nor can they return values.


To me this document feels like a step towards specifying what are interrupt handlers allowed / not allowed to do.

I think that is worth specifying and we might be able to do that without having to speak about "masking" and many other concepts touched in this document.

From that point-of-view, this single point is one of the most important points of the document to me.

This point mentions that their type must be fn() -> (), yet if they are not defined, they are implemented as fn interrupt() { loop {} }, so I wonder, can their type also be fn() -> ! ?

Also, if they return, they either have no effects (e.g. fn interrupt() {}) or they have a side-effect. Which side-effects are they allowed to have ? For example, suppose we have:

static PTR: UnsafeCell<*mut i32>; unsafe fn interrupt() { PTR.get().write_volatile(42); } fn foo() { let mut x = 0; PTR.set(&mut x); // preempted to `interrupt` here dbg!(x); // Does this print `0` or `42` ? PTR.set(ptr::null_mut()); }

foo's execution can be preemtpted to an unsafe fn call, which can modify foo stack. Can dbg!(x) be optimized by the compiler to dbg!(0) ?

I suppose we want to allow the compiler to optimize dbg!(x) to dbg!(0) in this case, and if a user want's to be able to read the 42 modification, they'd have to write dbg!((&x as *const _).read_volatile()); or similar.

In a sense, interrupts always run in a different thread of execution, so even thought the application is single threaded, they should move into them any types that are not Send, should not read / write through references to types that are not Sync, etc.

Ideally, we would have an #[interrupt] annotation in the language that would enforce these invariants at the type level and produce proper errors. EDIT: maybe we can write #[interrupt] as a procedural macro today? E.g. by wrapping the body of the interrupt in a closure, and passing it to a thread::spawn like function that executes it, enforcing type bounds.

In a sense, interrupts always run in a different thread of execution,

I agree that this is the best way to think about them.
In user space, the same happens with signal handlers.

RalfJung · 2019-06-29T09:05:01Z

@japaric final reminder that we are going to close the BEAM PRs soon and replace them by an issue. I'd really like to land this general description of the BEAM, and not lose all the reviewing time we put into it, but we can't do it alone.

RalfJung · 2019-07-18T14:46:35Z

Closing due to inactivity, see #169 for tracking.

add BEAM specification

3cc2eef

RalfJung reviewed May 5, 2019

View reviewed changes

wip/beam-spec.md

}

}

}

}

Copy link

Member

RalfJung May 5, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would have been really useful further up when I tried to figure out what all that English text means.

RalfJung reviewed May 5, 2019

View reviewed changes

gnzlbg reviewed Jun 13, 2019

View reviewed changes

RalfJung mentioned this pull request Jul 18, 2019

Specification of interrupts, interrupt handlers, signals, signal handlers (Basic Embedded Abstract Machine: BEAM) #169

Closed

RalfJung closed this Jul 18, 2019

The Basic Embedded Abstract Machine (BEAM) and unsafe embedded code #111

The Basic Embedded Abstract Machine (BEAM) and unsafe embedded code #111

Uh oh!

Conversation

japaric commented Apr 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gnzlbg commented Apr 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

comex commented Apr 15, 2019

Uh oh!

RalfJung commented May 5, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gnzlbg Jun 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RalfJung commented Jun 13, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

petrochenkov Jun 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gnzlbg Jun 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gnzlbg Jun 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gnzlbg Jun 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RalfJung commented Jun 29, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RalfJung commented Jul 18, 2019

Uh oh!

Uh oh!

The Basic Embedded Abstract Machine (BEAM) and `unsafe` embedded code #111

The Basic Embedded Abstract Machine (BEAM) and `unsafe` embedded code #111

japaric commented Apr 14, 2019 •

edited

Loading

gnzlbg commented Apr 14, 2019 •

edited

Loading

gnzlbg Jun 13, 2019 •

edited

Loading

petrochenkov Jun 13, 2019 •

edited

Loading

gnzlbg Jun 13, 2019 •

edited

Loading

gnzlbg Jun 13, 2019 •

edited

Loading

gnzlbg Jun 13, 2019 •

edited

Loading

RalfJung commented Jun 29, 2019 •

edited

Loading