tool: create IPC buffer in the tool, not the ELF#532
Conversation
midnightveil
force-pushed
the
julia/ipc-buffer-patched
branch
from
ea57cbf to
3555000
Compare
|
OK, figured out the issue: seL4/seL4#1693. Annoyingly this complicates things, but oh well. |
midnightveil
force-pushed
the
julia/ipc-buffer-patched
branch
from
3555000 to
ff31b38
Compare
dreamliner787-9
left a comment
dreamliner787-9
left a comment
There was a problem hiding this comment.
A couple of small things from me but other than that looks good.
| // Workaround: https://github.com/seL4/seL4/issues/1693 | ||
| #if seL4_UserTop == 0x00ffffffffff || seL4_UserTop == 0x0fffffffffff || seL4_UserTop == 0x7fffffffffff | ||
| #define user_top_aligned (seL4_UserTop + 1) | ||
| #elif (seL4_UserTop & ((1ULL << seL4_PageBits) - 1)) != 0 | ||
| #error "Expects seL4_UserTop to be aligned" | ||
| #else | ||
| #define user_top_aligned (seL4_UserTop) | ||
| #endif |
There was a problem hiding this comment.
Suggestion: can we fix this in the kernel first? I dislike having workarounds like this, because then we have to go back and fix it later.
There was a problem hiding this comment.
It depends on proof updates to seL4, as the values are used inside seL4 implementation.
I suppose @lsf37 can comment if it would be possible to fix seL4/seL4#1693 before the next release.
We could do something hacky where we export a different value than what seL4 uses in the code, and so we make userspace consistent whilst leaving the checks the same. I don't suppose the semantics extraction is clever enough to do constant folding, would it?
e.g. if we changed a seL4_UserTop that is 0x800000000 to 0x7fffffffffff and then made the check inside the vspace map functions do (>= (seL4_UserTop + 1)). Whether it's smart enough to constant fold and not affect the proofs?
But I don't know if it's worth doing that as opposed to just fixing it... (it's surely just changing < to <= in a few places?).
There was a problem hiding this comment.
The semantics extraction does not do constant folding as such, but a lot of the times it is done implicitly in the proofs, so it would be possible to be lucky on that one.
I currently don't have it on the list for the release, because I wanted to focus on bugs, but it would not be hard to add once we have decided what to do. The tricky part is social: technically this changes the API and is a breaking change. I don't really want to write an entire RFC for this, but a few more opinions would be good.
There was a problem hiding this comment.
But I don't know if it's worth doing that as opposed to just fixing it... (it's surely just changing < to <= in a few places?).
In the code, yes. In the proofs it's slightly more than that, because one version needs a proof of absence of overflow and the other does not. It's small, but it's not automatic.
midnightveil
force-pushed
the
julia/ipc-buffer-patched
branch
2 times, most recently
from
38d5f9c to
871ee7f
Compare
midnightveil
force-pushed
the
julia/ipc-buffer-patched
branch
from
871ee7f to
af4b74f
Compare
|
This is now just blocked waiting on this update to the microkit-manifest: seL4/microkit-manifest#3 It now uses user_vspace_top everywhere. |
We should probably remove/rework this so it uses the manifest, but for now this is the easiest. Necessary for seL4_UserVSpaceTop. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This removes the need for the linker script to define the IPC buffer. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Turns out the SDF parser does check for overlap with the stack, so we don't need to duplicate this here, only doing ELF. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
midnightveil
force-pushed
the
julia/ipc-buffer-patched
branch
from
af4b74f to
e158afa
Compare
3 participants
This removes the need for the linker script to define the IPC buffer.
Fixes: #451.