Interesting, didn't hear from this system so far. Seems to be funded by the EU. Apparently it is written in pure Rust since 2020, and Andrew "bunnie" Huang seems to be involved.

Is there a PDF version of the book (https://betrusted.io/xous-book/)?

▲ romac 8 hours ago | parent [-]

There is a single-page version of the book that you can save as a PDF: https://betrusted.io/xous-book/print.html

▲ Rochus 8 hours ago | parent [-]

Great, thanks.

I assume the "kernel" makes heavy use of "unsafe", because all the infrastructure assumed by Rust is not available. Or how was this solved?

▲ ajb 6 hours ago | parent | next [-]

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.

	▲	quotemstr 4 hours ago \| parent [-]
		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.

▲ jandrewrogers 7 hours ago | parent | prev | next [-]

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.

▲ maxbond 7 hours ago | parent | prev | next [-]

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.

▲ Rochus 7 hours ago | parent [-]

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.

	▲	wmf 2 hours ago \| parent \| next [-]
		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.
	▲	maxbond 7 hours ago \| parent \| prev \| next [-]
		I have no affiliation, I'm just a commenter. The standard library requires a heap and such, but you can enable the no_std attribute to work in environments where they don't exist. https://docs.rust-embedded.org/book/intro/no-std.html 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.
	▲	inferiorhuman 6 hours ago \| parent \| prev [-]
		`Rust assumes a runtime, the standard library assumes a stack exists, a heap exists, and that main() is called by an OS;` Wrong. Source: I'm writing Rust without a runtime without a heap and without a main function. You can too.

▲ junon 7 hours ago | parent | prev [-]

You can't write a kernel without `unsafe` appearing somewhere.

▲

quotemstr 4 hours ago | parent [-]

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?

▲

tadfisher 3 hours ago | parent [-]

I guess then you aren't writing a kernel anymore, you're writing a driver suite for seL4.

	▲	quotemstr 3 hours ago \| parent [-]
		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.