search

seL4 / microkit

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

Remove taking the address of local variables #92

Closed isubasinghe closed 23 hours ago

isubasinghe commented 5 months ago

This is a change needed to verify the code (see this page on C parser restrictions), instead of taking the address of local variables we should take the address of a global variable and then copy it over to a local variable. This copy itself isn't really needed, but makes the proof somewhat nicer to express.

axel-h commented 5 months ago

This seem to be a general issue then that other code might also run into. Thus, I wonder if we should provide a version of seL4_ReplyRecv() that returns all both tag an badge then. This might apply for other API then also.

lsf37 commented 5 months ago

This seem to be a general issue then that other code might also run into. Thus, I wonder if we should provide a version of seL4_ReplyRecv() that returns all both tag an badge then. This might apply for other API then also.

It would actually be nice to survey libsel4 for those kinds of things. I wonder if returning a tuple (struct) here would also work nicer with the Rust interface. @nspin do you have any input on that? It doesn't seem to me like there'd be any real performance impact since this is just a word.

Ivan-Velickovic commented 5 months ago

I wonder if returning a tuple (struct) here would also work nicer with the Rust interface. @nspin do you have any input on that?

The Rust bindings already do, e.g https://sel4.github.io/rust-sel4/views/aarch64-microkit/aarch64-sel4-microkit/doc/sel4/struct.LocalCPtr.html#method.reply_recv.

isubasinghe commented 5 months ago

This seem to be a general issue then that other code might also run into. Thus, I wonder if we should provide a version of seL4_ReplyRecv() that returns all both tag an badge then. This might apply for other API then also.

It would actually be nice to survey libsel4 for those kinds of things. I wonder if returning a tuple (struct) here would also work nicer with the Rust interface. @nspin do you have any input on that? It doesn't seem to me like there'd be any real performance impact since this is just a word.

It would be nice if we can get the code in libsel4 itself in a position where we can pass it off to the C parser. I believe it's really CallWithMRs that is problematic.

This is one thing that somewhat impacts the ability to get verification as a part of the CI pipeline. We can talk more about this tomorrow.

wom-bat commented 4 months ago

These changes make the code no longer thread-safe. Is it meant to be?

Ivan-Velickovic commented 4 months ago

These changes make the code no longer thread-safe. Is it meant to be?

All PDs are single-threaded (and I don’t think the code was thread safe to begin with actually)

axel-h commented 4 months ago

Given this is all internal static functions, it seems fine. But I wonder if the variables should be made static at least? What is the state about the approach suggested in https://github.com/seL4/microkit/pull/92#issuecomment-1895669349, to solve this for a wider usage, is there a plan to try this?

Ivan-Velickovic commented 4 months ago

The new globals introduced in this PR can probably be static sure.

Yes, to my knowledge we'd still like to try change libsel4 to return a struct instead. Main focus regarding verification is automating it so that it can be put into CI. Once that is finished I assume @isubasinghe will have more time to return to this.

isubasinghe commented 4 months ago

Just an update to what I've done regarding verification is that I've kept these changes and changed libsel4 and the python gen tool to emit /* DONT_TRANSLATE */ comments before every libsel4 function.

This was the quickest way to automate the verification process. I have a slight preference to doing what I've done here because it requires little change to libsel4, but happy to make the changes to return structs if there is consensus that that approach is better.

axel-h commented 4 months ago

make the changes to return structs

It would break the API, so that might be a tough step. If we add a new set of functions with the new interface it might allow a transition for users that care.

Ivan-Velickovic commented 23 hours ago

Closing because @isubasinghe won't be pursuing this anymore and we are likely looking at a change to verification tooling that would not need this patch.

If we do need it we can always re-open.