4 ms·

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 seem

by Rochus 9mo ago

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/ https://betrusted.io/xous-book/)?

romac 9mo ago
There is a single-page version of the book that you can save as a PDF: https://betrusted.io/xous-book/print.html https://betrusted.io/xous-book/print.html
- Rochus 9mo ago
  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?
  - maxbond 9mo ago
    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 9mo ago
      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.
      - maxbond 9mo ago
        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 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 9mo ago
        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.
        xobs 9mo ago
        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.
        comex 9mo ago
        As will C.
        oguz-ismail2 9mo ago
        No idea what either of you are talking about. It's the operating system that sets those things up not the language runtime.
        monocasa 9mo ago
        Not for kernels.
      - 9mo ago
  - junon 9mo ago
    You can't write a kernel without `unsafe` appearing somewhere.
    - quotemstr 9mo ago
      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 9mo ago
        I guess then you aren't writing a kernel anymore, you're writing a driver suite for seL4.
        quotemstr 9mo ago
        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.
      - bunnie 9mo ago
        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.
  - jandrewrogers 9mo ago
    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.
  - ajb 9mo ago
    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 9mo ago
      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.
      - pastage 9mo ago
        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 https://precursor.dev/ https://precursor.dev/ https://www.kernel.org/doc/Documentation/nommu-mmap.txt https://www.kernel.org/doc/Documentation/nommu-mmap.txt
utopiah 9mo ago
It's not directly funded by the EU, it's funded by NLNet which is only in part funded by the EU. The goal is to collect money from large sources (e.g. EU) from relatively complex subsidiaries that are too big for small projects then dispatch and evaluate. Source : I have an NLNet funded project, so like Xous https://github.com/betrusted-io/xous-core?tab=readme-ov-file#acknowledgement https://github.com/betrusted-io/xous-core?tab=readme-ov-file... I have such banners at the bottom of my repository.
bunnie 9mo ago
Thanks to a PR from a community member (millette) there's now a PDF: https://betrusted.io/xous-book/pdf/xous-book.pdf https://betrusted.io/xous-book/pdf/xous-book.pdf

by Rochus 9mo ago

romac 9mo ago

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

Rochus 9mo ago
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?
- maxbond 9mo ago
  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 9mo ago
    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.
    - maxbond 9mo ago
      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 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 9mo ago
      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.
      - xobs 9mo ago
        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.
        comex 9mo ago
        As will C.
        oguz-ismail2 9mo ago
        No idea what either of you are talking about. It's the operating system that sets those things up not the language runtime.
        monocasa 9mo ago
        Not for kernels.
    - 9mo ago
- junon 9mo ago
  You can't write a kernel without `unsafe` appearing somewhere.
  - quotemstr 9mo ago
    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 9mo ago
      I guess then you aren't writing a kernel anymore, you're writing a driver suite for seL4.
      - quotemstr 9mo ago
        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.
    - bunnie 9mo ago
      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.
- jandrewrogers 9mo ago
  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.
- ajb 9mo ago
  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 9mo ago
    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.
    - pastage 9mo ago
      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 https://precursor.dev/ https://precursor.dev/ https://www.kernel.org/doc/Documentation/nommu-mmap.txt https://www.kernel.org/doc/Documentation/nommu-mmap.txt

utopiah 9mo ago

It's not directly funded by the EU, it's funded by NLNet which is only in part funded by the EU. The goal is to collect money from large sources (e.g. EU) from relatively complex subsidiaries that are too big for small projects then dispatch and evaluate. Source : I have an NLNet funded project, so like Xous https://github.com/betrusted-io/xous-core?tab=readme-ov-file#acknowledgement https://github.com/betrusted-io/xous-core?tab=readme-ov-file... I have such banners at the bottom of my repository.

bunnie 9mo ago

Thanks to a PR from a community member (millette) there's now a PDF: https://betrusted.io/xous-book/pdf/xous-book.pdf https://betrusted.io/xous-book/pdf/xous-book.pdf