At 2019-11-08T14:09:14+0800, 李庚 wrote:
Dear Sir or Madam,
Very Sorry to brother you.
It's no bother--the mailing list is here to help people.
We have get into trouble after compiling sel4
following the https://docs.sel4.systems/Docker.html,may
I seek some advice from you?
First,I attmpt to follow the
"Failed to allocate object
of size xxxx" ara discovered in serial_output.txt .
I don't have any experience with VMWare but I suspect what you're seeing
is not related to VMWare.
The Docker page you mentioned first guides the reader through the build
and execution of an seL4 project using the "sel4test" userspace. It is
difficult to evaluate an operating system kernel, especially a
microkernel, without giving it some tasks to run. sel4test is a
userspace task whose job is to exercise the system and check whether it
is operating successfully.
sel4test produces a lot of output, and many diagnostic measures are
emitted as the userspace code attempts to do many impossible things,
like attempt to gain a capability to more memory than physically exists
on the system, or prohibited things, like invoking a capability that
does not exist. Many of these tests are present to (informally) verify
the security properties of the system.
The bottom line is that you will see many error messages; not all of
them are failures per se. Similarly, you would not expect at a Unix
shell session for an unpriviled user to be able to run superuser
commands or inspect the memory of processes that belong to other users.
The literal bottom line is that when sel4test is done running, you
should see some output like this:
Starting test 120: Test all tests ran
Test suite passed. 120 tests passed. 48 tests disabled.
All is well in the universe
If you see "All is well in the universe" (as I just now confirmed on a
build for the sabre platform with simulation enabled, so I could test
the platform using QEMU instead of real hardware), then there is no
reason to be alarmed by the error messages you are seeing--the system is
Second,we wanna to make a sel4 startup disk
there any useful Document ?
I haven't deployed seL4 on a physical x86_64 machine myself, but seL4
supports that target and I've run sel4test and sel4bench (a benchmarking
userspace) on QEMU-simulated x86_64 hardware many times. seL4 supports
Try having a look at https://docs.sel4.systems/GettingStarted.html
That page will take through an x86_64 build and run of sel4test.
Sorry again for this sudden interruption and I
would be very
grateful if receive your reply.