Redox OS 0.6.0 | Hacker News Reader

Redox OS 0.6.0

redox-os.org

111 pointsjackpot5128 comments

I am Jeremy Soller, the creator of Redox OS, please let me know if you have questions!

Can you share what are the things missing from redoxOS before it can take advantage of the full capabilities of a system76 laptop?

iwlwifi, a more complete USB stack, i2c hid, graphics acceleration.

What does work is pretty cool though. Ethernet, input, non-accelerated graphics, nvme and ahci storage

Related, what is the end goal for Redox in your mind?

Do you plan to ship it on System76 laptops when it's eventually ready? Or do you see this more as a hobby / exploratory project?

What's next for Redox OS? I couldn't find a roadmap, but maybe you have one?

Next up is probably a graphical installer

Any plans for what to do about GPU drivers?

Port DRM drivers to userspace and use mesa, probably

Cool, I figured as much, I guess that means implementing ioctl() or some equivalent.

Hey Jeremy! What sort of support do you have for graphical APIs like windowing, graphics, etc.? I'd be really interested in working with you to port Veloren (https://veloren.net/), also written in Rust, to Redox at some point in the future: if nothing else, as a demonstration of what a pure Rust tech stack can do. If you're interested in this, feel free to message me on Reddit (same username).

Hi Jeremy,

Is there a port of Redox OS which runs under xen as a guest OS (paravirtual or otherwise)?

Lots of tiny OSes, such as Minix, have been ported to this environment and I think this could be a fun way to run Redox while leveraging the broad device support of a traditional Linux Kernel.

Thanks!

> rmm, a complete rewrite of the kernel memory manager. This has eliminated kernel memory leaks, which became quite an issue with the previous memory manager

Hang on, I thought the whole point of writing in Rust was that this didn't happen. Is there something about a memory manager that requires unsafe? (Keeping in mind that I neither know Rust nor kernel design, so there's a very good chance that I'm just missing something here)

Memory managers are intrinsically unsafe. Rust generally passes around already allocated memory, but allocating the memory requires that you start with an undifferentiated bucket of bits, so the memory manager passes around raw pointers.

In Rust, memory leaks are considered "safe"; you don't need unsafe to create a memory leak. There's even a function in the standard library (std::mem::forget) to explicitly leak a value, and it's not marked as unsafe. And even without that function, it's very easy to leak memory in safe code (just create a cycle with reference-counted values).

But yes, memory managers generally require unsafe. Consider what happens when you release memory containing a value of type A, and that memory is later allocated for a value of type B. This is equivalent to a transmute between types A and B, which requires unsafe.

The book[1] (something like bible of Rust) wrotes:

> memory leaks are memory safe in Rust

[1]: https://doc.rust-lang.org/book/ch15-06-reference-cycles.html...

There's probably no way to guarantee that there are no memory leaks in a general purpose language where you can allocate memory dynamically. How can the allocator know if you actually need those 1 MB chunks forever, like you keep requesting?

Couldn't the language demand that, as long as a memory chunk is allocated and not freed, there's a path to use this memory chunk? Meaning it's not a memory leak in the sense of 'we are certain (we could prove) that this memory chunk will never be used again', such as the std::mem::forget mentioned elsewhere in the thread.

In practice that would mean that you need to write some formal proof, but that doesn't seem impossible. Just like some formal languages require that you write a termination proof to define a recursive function. Of course I'm not saying this is a practical solution for a language like Rust to demand this kind of proofs for every program, but since programs written in a subset of C have been formally verified, it should be possible (and sometimes desirable) for Rust too.

This is actually pretty easy to do, and indeed vanilla Rust does sort of guarantee that memory leaks can't happen, at least when using its normal ownership rules.

However, Rust's standard library also includes types (implemented with unsafe code, but only accessible through safe interfaces) that allow shared ownership through reference-counting like `Rc`/`Arc` and also ways to mutate shared memory like `RefCell`/`Mutex`. These two things, in combination, allow the creation of self-referential data (i.e: effectively a leak). For this reason, it's necessary to consider leaking a safe (if generally unintended) behaviour.

After all, leaking isn't "undefined behaviour" and it generally isn't intrinsically harmful to the program, except at the limit when the computer runs out of memory in which case you get a safe, well-defined OOM panic. Heck, there are even a plethora of useful techniques that use leaking. Leaking a data structure proves to the compiler that it will stay around indefinitely (i.e: it has a "static" lifetime), for example, which allows you to do things with it that Rust would normally forbid.

That is not to say that Rust doesn't provide any protection from leaking, however. Its ownership model generally makes leaking extremely difficult to do accidentally, particularly when designing programs idiomatically, and its standard library contains a variety of abstractions that aid in managing shared memory correctly without leaks (Weak RC references, reference swapping, etc.).

I don't think I've personally ever experienced a leak-related problem that wasn't a result of badly-considered unsafe code despite the fact that I've been writing Rust every day for about 5 years and as my day job for the last 2 of those.

> Leaking a data structure proves to the compiler that it will stay around indefinitely (i.e: it has a "static" lifetime), for example, which allows you to do things with it that Rust would normally forbid.

Asking as a Rust neophyte: are you saying that one thus declares a static lifetime without using the static lifetime name (https://doc.rust-lang.org/stable/rust-by-example/scope/lifet...)? In which case would you do one way over the other then?

The type signature of the leak function is

  pub fn leak<'a>(b: Box<T>) -> &'a mut T
  where
      T: 'a,

If T is owned, or only contains ‘static references itself, then ‘a must also be ‘static. Does that help at all?

Most of my programming has been in various garbage collected languages, where indeed the language ensures that there's a path to use allocated memory, and if not, it gets rid of it.

It doesn't stop you leaking memory though. You can store stuff in a map and then never get it out again, and depending on what you're doing, that sort of thing can be surprisingly common.

Allocate memory and assign to a global that’s never actually used. Boom. Memory leak. Make that global a vector to leak larger amounts of memory more easily.

Rust doesn’t have a GC which would be needed to make the guarantee you’re looking for at runtime (and even still, GC’d languages can be made to leak memory as well as far as I’m aware).

In addition to what others have already said: "unsafe" just means that the compiler does not understand your data structure well enough to enforce its invariants. And that's okay! The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical. The zen of Rust is to reduce unsafe code to the minimum, to have only 1% or 0.1% of your code that is unsafe and needs to be reviewed extra-super-duper-rigorously.

> The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical

I'm not sure what you mean by ‘borderline magical’. There are formal verification tools for e.g. c and a subset of ada. The sel4 microkernel has been completely formally verified; i.e. it has no unsafe code.

There is no one definition of 'formal verification'. Sel4's verification required developers to specifically demarcate the behaviour they desire and generally requires the use of abstractions with very predictable safe semantics. In addition, Sel4 is less than 9k lines of code.

That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code. That's not the goal of Rust and I doubt that it would be a particularly useful one for 99% of developers anyway. The goal of Rust's safety promise is that the verification and review of an entire codebase (as would be the case in C) shrinks down to just a very small corner of that codebase (that which is demarcated as 'unsafe').

In practice, I think that unsafe uses are substantially rarer than that even. Veloren (https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand.

> Sel4 is less than 9k lines of code

By my count, it's approximately 86k loc.

> That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code

Even a language like ATS (which is ‘general-purpose’) can verify a substantial majority of code which would need to be marked ‘unsafe’ under rust. (It also proves a number of other interesting and desirable features, like bounding recursion.)

> I doubt that [complete formal verification, as a goal] would be a particularly useful one for 99% of developers anyway

Why? I find that a pretty attractive proposition.

Safety isn't an end to itself; it's means that enables a broader desire to produce more reliable, correct software. One of the great things that rust (and, to a lesser extent, typescript) have done is to bring more expressive, powerful type systems into vogue. Ones that can more effectively model real-world systems and verify program behaviour. Why choose to stop, arbitrarily, with however much power rust's type system happens to have at the moment?

> Veloren (https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand

Veloren is a video game and arguably has no excuse for having any unsafe code. Redox, which is probably a better case study, uses the keyword 8k times.

Memory leaks have nothing to do with "safe programming". Rust simply guarantees that if something is not freed, there is a reference to it. That doesn't mean that circular references or self-referential references can't be created that indeed don't violate what I stated above.

Love seeing the progress on this! Thank you for sharing!

Reply on news.ycombinator.com