From the talk linked above, they went to considerable effort to design a system with a cheap processor which nevertheless contains an mmu, and so most other embedded kernels, which assume the lack of one, are not applicable. So the point of writing in rust is that they can ensure that some of the guarantees of rust are enforced by the hardware. (It's been a while since I watched that talk, so I don't recall exactly which ones). And this is a microkernel, not a monolithic kernel, so they will be using hardware guarantees even between kernel components.
To be fair, 1) Zephyr can take advantage of an MMU if you have one, and 2) Linux itself scales down surprisingly far. Keep in mind that its lineage extends far back in time and that it retains much of its ability to run on low-spec hardware.
Linux required MMU from the start, uCLinux and nommu patches does work. I used it a long time ago it was great, but there are lots of small things like stack size is set compile time, memory mapped io does not work... You do get lots of functionality from Linux from my short three day experience with Zephyr I like uCLinux a lot better at least on STM32.
Xous seemed very nice together with Precursor which is the only platform I have seen it run on
It's not really about infrastructure but yes kernels and firmwares have to do a lot of stuff the compiler can't verify as safe, eg writing to a magic memory address you obtained from the datasheet that enables some feature of the chip. And that will need to happen in unsafe code blocks. I wouldn't call that a problem but it is a reality.
Are you one of the authors? Concerning the "infrastructure": Rust assumes a runtime, the standard library assumes a stack exists, a heap exists, and that main() is called by an OS; in a kernel, none of this is true. And the borrow checker cannot reason about things like e.g. DMA controllers mutating memory the CPU believes it owns, Memory-mapped I/O where a "read" has side effects (violating functional purity), context switches that require saving register state to arbitrary memory locations, or interrupt handlers that violate the call stack model. That's what I mean by "infrastructure". It's essentially the same issue with every programming language to some degree, but for Rust it is relevant to understand that the "safety guarantees" don't apply to all parts of an operating system, even if written in Rust.
I am a maintainer. I think what you're referring to is the problem where `std` is actually a veneer on C - so for example, when Rust allocates memory on an x86-class desktop, it actually invokes a C library (jemalloc, or whatever the OS is using) and that networking is all built on top of libc. Thus a bunch of nice things like threads, time, filesystem, allocators are all actually the same old C libraries that everything else uses underneath a patina of Rust.
In Xous, considerable effort went in to build the entire `std` in Rust as well, so no C compilers are required to build the OS, including `std`. You can see some of the bindings here in the Rust fork that we maintain: https://github.com/betrusted-io/rust/tree/1.92.0-xous/librar...
Thus to boot the OS, a few lines of assembly are required to set up the stack pointer and some default exception handler state, and from there we jump into Rust and stay in Rust. Even the bootloaders are written in Rust using the small assembly shim then jump to Rust trick.
Xous is Tier-3 Rust OS, so we are listed as a stable Rust target. We build and host the binaries for our `std` library, which native rustc knows how to link against.
Thanks, interesting. My concern was less about which language implements std, but rather about the semantic mismatch between Rust's ownership model and hardware behavior (e.g. DMA aliasing, MMIO side effects). So I was curious what work-around you found; do you e.g. use wrapper types with VolatileCell, or just raw pointers?
Hmm, I think I see what you're asking. I'm not sure if this exactly answers your question, but at least for aliasing, because we have virtual memory all pages have to be white-listed to be valid.
Thus "natural" aliases (say due to a decoder that doesn't decode all the address bits) can't be mapped because the OS would not accept the aliases as valid pages. This is handled through a mechanism that goes through the SVD description of the SoC (SVD is basically an XML file that lists every register and memory region) and derives the list of valid pages. The OS loader then marks those as the set of mappable pages; any attempt to map a page outside that list will lead to a page fault. One nice thing about the SoC RTL being open source is that this entire process of extracting these pages is scripted and extracted from the SoC's source code, so while there can be code bugs, at least human error is eliminated from that process.
DMA devices on their own right can have "god mode" access to memory, because they operate on physical memory addresses and lack page translation tables. To that end the preferred DMA mechanism in hardware has an "allow list" of windows that can be enabled as DMA targets; on reset the list is nil and nothing can be DMA'd, the OS has to correctly configure that. So this is not a Rust-level thing, this is just a driver-level hack. Not all the DMA-capable peripherals have this safety mechanism though, some of the IP blocks are just a big gun with no safety and you're free to point it at your toes.
However, if you set up a DMA and then you read from it later on - you're in unsafe territory. Rust can't reason about that. So for structures that are intended as DMA targets, they are coded in a peculiar way such that they are marked as unsafe and you're using the read_volatile() method on the raw pointer type to force the compiler to not try to optimize out the read for any reason. Furthermore, fence instructions are put around these reads, and a cache flush is required to ensure the correct data is pulled in.
This complexity is baked into a wrapper struct we create specifically to handle dangerous interactions like this.
Thanks, that's exactly what I was asking about. So if I understand correctly: for the hardware interface layer (DMA, MMIO), you're essentially writing disciplined C-style code in unsafe blocks with volatile reads and manual memory barriers, then wrapping it to contain the unsafety. That's pragmatic.
I was looking for information about Xous's raw IPC performance to get an impression of how it performs compared to e.g. the L4 family, especially L4re and sel4. Also a comparison to QNX would be very interesting. Are there any "cycles-per-IPC" benchmarks for Xous available somewhere? What are your plans/goals in this regards?
Rust's safety model only applies to code you write in your program, and there's a lot that's unsafe (cannot be verified by the compiler) about writing a kernel or a firmware, agreed. You could have similar problems when doing FFI as well.
standard library assumes a stack exists, a heap exists, and that main() is called
A small assembly stub can set up the stack and heap and call main(); from then on you can run Rust code. The other topics you mention are definitely legitimate concerns that require discipline from the programmer because Rust won't automatically handle them but the result will still be safer than C.
The Rust runtime will, at a minimum, set up the stack pointer, zero out the .bss, and fill in the .data section. You're right in that a heap is optional, but Rust will get very cranky if you don't set up the .data or .bss sections.
Use of "unsafe" is unavoidable. Various pieces of hardware are directly writing into the address space. Concepts of "ownership" and "mutability" go beyond code semantics.
Yeah. That's why my preferred approach isn't to use Rust for the core TCB. It'd be mostly unsafe anyway, so what's the point? You can write in an all-unsafe language if you want. you can still prove it correct out of band, and seL4 has done that work for you.
Sure, you could just use unsafe Rust and prove it correct with Prusti or something, but why duplicate work?
It is true that hardware, by definition, is a big ball of globally mutable state with no guarantees about concurrency, data types, or anything else. However, one could take the view that it's the role of the OS to restrict & refine that raw power into a set of APIs that are safe, through a set of disciplines, such as reasoning through why an unsafe block might actually be sound.
unsafe means that the compiler can't provide any guarantees about what happens inside the unsafe block. However, it is possible to manually ensure those guarantees.
Thus as a matter of discipline every time an unsafe block is used there's a comment next to it recanting the mantra of safety: This `unsafe` is sound because ... all data types are representable, the region is aligned & initialized with valid data, the lifetime is static, we structurally guarantee only one owner at a time (no concurrency issues)...often times in writing that comment, I'll be like, "oh, right. I didn't actually think about concurrency, we're going to need an Atomic somewhere around this to guarantee that" - and that saves me a really hard-to-find concurrency bug down the road.
So while this is a very manual process, I have found the process of documenting safety to be pretty helpful in improving code quality.
Once you've established safety, then you do get some nice things in your life, like Mutexes, Refcells, Arcs, and the whole collections library to build an OS on top of, which saves us a lot of bugs. It is kind of nice to have a situation where if the code compiles, it often just works.
Because not ALL of it is unsafe. The point of using Rust in the kernel is to write abstractions over the unsafe bits and then utilize safe Rust for all the logic you build on top.
Yep. And that's a good place to be. Keep in mind that the "driver suite" in an seL4 system includes a bunch of things that others would put in the kernel: memory management and swap, networking, filesystems, linking and loading, and so on are all userspace. So, if you want, you still get to differentiate based on interesting low-level things.
Calling seL4 system guts a "driver suite" is like calling rustc "just a preprocessor for LLVM IR". True, but only in the most uselessly pedantic sense.
>It'd be mostly unsafe anyway, so what's the point?
The vast majority of the code that will be tagged "unsafe", will be done so because you're doing the equivalent of FFI, but implemented in hardware. If there was a way to automatically generate the binding from a register map, the only purpose of the unsafe keyword would be to warn you that the effect of the ffi call you are doing is unknown. In other words, the unsafe marker isn't some kind of admission of defeat. It marks the potentially unsafe sections of the code where additional care might be required.
This means you're throwing out the baby with the bathwater.
You can also go the other way around and generate traces [1] from the TLA+ or Quint [2] specs using the Apalache model checker [3], map each action in the trace to an action on your system under test, and check that the abstract and concrete states match at each step.
If you are interested in TLA+, you might want to check out Quint (https://quint-lang.org), a modern take on a specification language which shares the same underlying temporal logic of actions, but with a syntax more familiar to programmers.
If you haven't seen those already, you might also want to check out:
- Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
- Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)
I see the game was ported with the legacy CheerpJ 2.3 runtime. Consider upgrading to the new CheerpJ 3.0. Improving boot times has been one of our main goals and upgrading is very easy: https://cheerpj.com/docs/migrating-from-cheerpj2
Fun game! I thought you programmed it wrong till I realized in your version of liars dice 1s are wild. Also never played the way of guessing the total number of dots, and we always have loser go first on the next round. Thanks for sharing!
Vale has a very interesting approach to memory safety, without garbage collection or a borrow checker, using a memory management technique called "generational references" which I had never heard of previously.
reply