Hi All,
Here are a few minor details/questions about the kernel code & documentation.
(I've confirmed that these are present in the new seL4-12.1.0 release.)
1) kernel/include/arch/x86/arch/32/mode/machine.h has the following definition
(some code elided):
static inline word_t FORCE_INLINE x86_read_fs_base_impl(void)
{
word_t base = 0;
base &= ...;
base &= ...;
base &= ...;
return base;
}
I'm pretty sure that the three &= operators here should be |= or else the
result is always going to be zero. The same issue occurs in
x86_read_gs_base_impl in the same file.
Some follow-up questions:
Can anyone say if this would have been detected if the PC99 (32-bit) platform
had been verified?
More generally, where can I find information about how ia32 segment registers
are handled by the kernel? Why aren't they just stored/restored like other
user-level registers on kernel entry/exit? Is there something that prevents
user-level changes in the ES register, for example, from being observed in
other threads?
2) A CNodeRotate will generate a FailedLookup error if the pivot slot either
doesn't exist or contains a null capability. But, in the first case the
"lookup failed for a source capability" field in the error message is 1, while
in the second it is 0. Hardly a serious problem, but this does seem
inconsistent. Is this intentional, or a mistake in the specification that has
been carried over to the implementation?
3) Section "3.4 Lookup Failure Description" of the manual describes how
capability lookup errors are represented in an IPC buffer. But it seems the
layout information is incorrect. For example, Section 3.4.2 says that "Offset
+ 0" will contain seL4_MissingCapability while the number of bits left will be
at "Offset + seL4_CapFault_BitsLeft", which is probably supposed to be
equivalent to "Offset + 1". But, based on
kernel/libsel4/include/sel4/shared_types.h, it would seem that this gives
"Offset + 4". Sections 3.4.3 and 3.4.4 have similar problems.
4) On https://docs.sel4.systems/GettingStarted, in the section labeled
"Fetching, Configuring and Building seL4test", there are missing line breaks
between the commands in the text boxes for Steps 1 and 2, and there are some
tags in the text box for Step 4 that probably should not be displayed.
Best wishes, and thanks for any feedback!
Mark
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
