microkit
microkit copied to clipboard
seL4
Remove taking the address of local variables
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.
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.
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.
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.
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.
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)
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?
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.
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.
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.
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.