search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
68 stars 37 forks source link

tool: Not failing if symbols aren't present for patching #86

Open nspin opened 5 months ago

nspin commented 5 months ago

Currently, the MicroKit tool fails if symbols it plans to patch (e.g. microkit_name or those referred to by setvar_vaddr) aren't present. One example of a case where this is inconvenient is when a PD never actually uses microkit_name , and so the linker might exclude microkit_name from the final binary. This happens in Rust PDs for which the compiler can prove that they never panic.

In Rust, there is no way to instruct the linker to include certain unused symbols in the final binary without using unstable features.

I think the best solution is for the tool to permit such symbols to be absent in the binary.

Ivan-Velickovic commented 5 months ago

setvar_vaddr is optional, so is the only problematic variable microkit_name?

Ivan-Velickovic commented 5 months ago

Having an option such as --no-elf-patching to the tool may be possible, but I would only want to do this if this is a problem across multiple/all systems programming languages.

Changing Microkit to work around a limitation in Rust seems weird.

nspin commented 5 months ago

This Rust scenario is just the specific reason why I've found myself wishing the tool had this slightly more general behavior.

I see the change I'm proposing as a slight generalization of the current behavior. From:

Patch each variable

To:

Patch each variable that actually exists in the binary

Making the tool more permissive in this way would simplify PD constructions by reducing the assumptions made about their structure.

Ivan-Velickovic commented 5 months ago

But it seems there is only one assumption we are talking about here, and that is the existence of microkit_name, right?

Ivan-Velickovic commented 5 months ago

I would find the behaviour of the tool weird if you had in your system description setvar_vaddr and then it didn't actually do that because of some control flow that is hidden from the user.

nspin commented 5 months ago

The tool derives, from the system description, a set of variables that it would patch for each PD. The assumption that I'm talking about is the assumption that all of these variables are present in the corresponding PD binaries.

nspin commented 5 months ago

I would find the behaviour of the tool weird if you had in your system description setvar_vaddr and then it didn't actually do that because of some control flow that is hidden from the user.

A case where I think that behavior would be nice is during development, before a PD developer has built out the PD to the point where the relevant variable is actually used.

Ivan-Velickovic commented 5 months ago

A case where I think that behavior would be nice is during development, before a PD developer has built out the PD to the point where the relevant variable is actually used.

Then during development just omit setvar_vaddr?

The behaviour of the variable patching is I think very clear right now. You ask the tool to patch a variable, and it does it. If it can't patch the variable you get a clear error message.

This approach would remove that clear behaviour, and I am not convinced right now that it is beneficial to do that just because a compiler invalidates the assumption. It seems that you are working around the behaviour of a compiler. I do not think it is unreasonable for a compiler for a systems programming language to explicitly leave in a symbol at the request of its user.

I will continue thinking about the issue, I haven't reached a conclusion.