Is there a plan to add UEFI support in seL4 for x86 hardware in the near
future? Newer x86 boards are frequently UEFI only. It is possible to
get around the lack of UEFI support, as I have done with the UP board:
https://up-community.org/wiki/Hardware_Specification
but I am hitting problems which I will detail below.
When I compile using ia32_debug_xml_defconfig and boot using the
resulting images the board fails to find the RSDP location. To fix this
I had to modify the source code a bit:
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h
+ #define UPBOARD_RSDP 0x5B161000
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c
- acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP,
strlen(ACPI_SIG_RSDP),
- (void *) BIOS_PADDR_START, (void *)
BIOS_PADDR_END);
+ acpi->rsdp = (void *)UPBOARD_RSDP;
* seL4test/kernel/src/plat/pc99/machine/acpi.c
- for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END;
addr += 16) {
+ for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) {
It would be handy to have this as a kernel parameter to cover cases
where it is not successfully discovered automatically. With these
changes I can boot the board and several tests pass but then I get stuck
on INTERRUPT0001 (Test interrupts with timer). I don't get a test
failure or an error the board just sits and makes no more progress.
Someone had that test fail in this post:
https://sel4.systems/pipermail/devel/2017-February/001328.html
and the first recommendation was to check if the irq of the timer was
correctly found. I booted the board into linux to find the correct irq
which was listed as 0 in /proc/interupts. I added a printf to
handleInterrupt in the kernel source, recompiled and when I booted seL4
I found that the irq reported to handleInterrupt is 125 (which sel4
reports as the max interrupt value) every time that function is called.
Adding this printf also showed me that when the test hangs the board
hasn't crashed or locked up as calls to handleInterrupt are made
continuously.
At this point I noticed that before any tests started to run several
ACPI tables are not recognized:
Parsing ACPI tables
Skipping table FPDTD, unknown
Skipping table FIDT<9c>, unknown
Skipping table UEFIB, unknown
Skipping table TPM24, unknown
Skipping table LPIT^D^A, unknown
Skipping table BCFG9^A, unknown
Skipping table PRAM0, unknown
Skipping table CSRTL^A, unknown
Skipping table BCFG9^A, unknown
Skipping table OEM0<84>, unknown
Skipping table OEM1@, unknown
Skipping table PIDVÜ, unknown
Skipping table RSCI,, unknown
Skipping table WDAT^D^A, unknown
Warning: skipping table ACPI XSDT
Maybe one or more of those tables needs to be loaded to handle
interrupts properly. The LPIT table is conspicuous in the case of the
timer test but I think other tests are likely to depend on the other tables.
Any suggestions about porting this type of hardware?
--
Edward Sandberg
Adventium Labs
111 3rd Avenue S. Suite #100
Minneapolis, MN 55401
ed.sandberg(a)adventiumlabs.com
Hello,
I realize that the only officially supported SMP platform is the i.mx6 but I did see some code on 6.0 to master for SMP and the zynq7000 so I am trying to test out some SMP functionality on my zc702 board.
I am wondering if anyone has this working because my system is failing when compiling from master and the 6.0 and compatible tags.
My second core seems to be coming up but the system ultimately fails and prints out:
Bo
ot
nKgE RaNlEl L fDinAiTsAh eAdBO, RdT!r
ppFaeud lttio nugs eirn stspraucctei o
n: 0xe001d1b0 o
FAR: 0xfffffff8 DFSR: 0x807
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 1, Invocation tag: 37
Which seems to be "Booting all finished, dropped to user space" from core0 and "KERNEL DATA ABORT!" from core1.
The "0xe001d1b0" seems to be the label of the "idle_thread" function.
While stepping through via JTAG, I have verified that core1 gets through "init_kernel" and then enters "restore_user_context" at some point in "restore_user_context" the fault registers as shown in the printed output are set. I think it is either in the c_exit_hook in restore_user_context or after the program branches to "0xFFF0010" which is "ldr pc,0xFFFF0030". This branches to the "arm_data_abort_exception" label, which goes to "kernel_data_fault" label and then to "kernel data abort".
I'm having trouble exactly pin pointing where the fault occurs but it seems to be close to there.
Has anyone had similar issues with SMP? It seems to get fairly far without setting the fault registers.
I have tried to step through the execution over JTAG and here are some of my (verbose) notes
| CORE0 Address | Core0 Function | Core0 Instruction | CORE1 Address | Core1 Function | Core1 Instruction | DFSR | DFAR | Note |
|---------------+-----------------------------+------------------------+---------------+------------------------------------+----------------------+------------+------------+------|
| 0x10000000 | label: start | =cpsid aif= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | |
| 0x10003A2C | call: platform_init | =bl -x10003DD8= | 0xFFFFFF30 | | =wfe= | 0x00000000 | 0x00005000 | |
| 0x10003ACC | call: smp_boot | =bl 0x100039FC= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | |
| 0x10003ADO | ret: smp_boot | =bl 0x10005C54= | 0x10000020 | in: non_boot_core | =orr r0,r0,#0x40= | 0x00000000 | 0x00005000 | 2 |
| 0x10003ADC | =if(is_hyp_mode())= | =beq 0x10003AF0= | 0x10002200 | label: arm_disable_dcaches | =push {r14}= | 0x00000000 | 0x00005000 | |
| 0x10003AFC | call: arm_enable_mmu | =bl 0x10002174= | 0xE0006190 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001D70 | label: init_kernel | =push {r11,r14}= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001814 | label: try_init_kernel | =push {r11,r14}= | 0xE0001690 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001B80 | call: create_initial_thread | =str r0, [r11,#-0x14]= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001C48 | call: SMP_COND_STATEMENT | =bl 0xE0003C20= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 3 |
| 0xE0001C4C | call: SMP_COND_STATEMENT | =bl 0xE00017D8= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 4 |
| 0xE0001C50 | NODE_LOCK_SYS | =bl 0xE0019280= | 0xE0019288 | in: getCurrentCPUIndex | =sub r13,r13,#0x8= | 0x00000000 | 0x00005000 | 5 |
| 0xE0001D1C | call: arch_pause | =bl 0xE0019DB0= | 0xE0019290 | in: getCurrentCPUIndex | =str r0,[r11,#-0x8]= | 0x00000000 | 0x00005000 | 6 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00037F4 | in: init_core_state | =pop {r4,r11,pc}= | 0x00000000 | 0x00005000 | |
| 0xE0001D20 | in: clh_lock_acquire | =mov r2,#0xE800= | 0xE0003754 | in: init_core_state | =movw r2,#0xE8E0= | 0x00000000 | 0x00005000 | 7 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00017C4 | in: try_init_kernel_secondary | =mov r3,#0x1= | 0x00000000 | 0x00005000 | 8 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002A06C | in: schedule | =push {r11,r14}= | 0x00000000 | 0x00005000 | 9 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002979C | in: activateThread | =push {r11, r14}= | 0x00000000 | 0x00005000 | 10 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE001D24C | label: Arch_activateIdleThread | =push {r11}= | 0x00000000 | 0x00005000 | 11 |
| 0xE0001D38 | in: clh_lock_acquire | =ldr r3,[r3,#0x4]= | 0xE0000054 | in: start | =b 0xE001CEC8= | 0x00000000 | 0x00005000 | 12 |
Notes
1. Core1 is in a =while (!node_boot_lock)= loop
2. In =smp_boot=, CORE1 changes after =init_cpus= (branch location: ZSR:10003A08)
- In =smp_boot=, =boot_cpus= is called
- This sets the =CPU_JUMP_PTR= =*((volatile uint32_t*)CPU_JUMP_PTR) = (uint32_t)entry;=
- calls =dsb= (data synchronization barrier)
- After this call, CPU1 goes to =FFFFFF2C: dsb sy=
- And then =sev=
- After this call, CPU1 goes to the =non_boot_core= label
- SEV
- SEV causes an event to be signaled to all cores within a multiprocessor system. If SEV is implemented, WFE must also be implemented.
- WFE
- If the Event Register is not set, WFE suspends execution until one of the following events occurs:
- an IRQ interrupt, unless masked by the CPSR I-bit
- an FIQ interrupt, unless masked by the CPSR F-bit
- an Imprecise Data abort, unless masked by the CPSR A-bit
- a Debug Entry request, if Debug is enabled
- an Event signaled by another processor using the SEV instruction.
- If the Event Register is set, WFE clears it and returns immediately.
- If WFE is implemented, SEV must also be implemented.
- After CPU0 executes =arm_enable_mmu()= from the =main= function
- by the end of =smp_boot= core1 is just starting =non_boot_main=
3. The =SMP_COND_STATEMENT= is calling =clh_lock_init=
4. The =SMP_COND_STATEMENT= is calling =release_secondary_cpus=
5. right after Core0 returned from releasing secondary cpus
- First time Core1 has exited the loop
- Core1's stack is
- =getCurrentCPUINdex=
- =init_core_state=
- =try_init_kernel_secondary_core=
- =init_kernel=
6. Core0 is in a =while(big_kernel_lock.node_owners[cpu].next->value ! = CLHState_Granted)=
- Core0 is in a static inline function =clh_lock_acquire= in =try_init_kernel=
- Core1 is in =getCurrentCPUIndex= but being called from =tcbDebugAppend=
- =tcbDebugAppend= is being called from a =for= loop in =init_core_state=
7. Core0 is still in the previously mentioned while loop
- Core1 is in "init_core_state" and has exited the for loop that called =tcbDebugAppend(NODE_STATE_ON_CORE(ksIdleThread, i))=
8. Core0 is still in the previously mentioned while loop
- Core1 has returned to =try_init_kernel_secondary_core= from =init_core_state= and is at the end of the function
9. Core0 is still in the previously mentioned while loop
- Core1 has entered the =init_kernel= call and then the =schedule= function.
10. Core0 is still in the previously mentioned while loop
- Core1 has entered the =activateThread= call after =schedule= in =init_kernel=
11. Core0 is still in the previously mentioned while loop
- Core1 seems to have dropped into the =case ThreadState_IdleThreadState:= case when switching on =switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState))=
- This was in =activateThread=
12. Core0 is still in the previously mentioned while loop
- Core1 has exited =init_kernel= and is now branching to =restore_user_context=
To test everything out I am using the "camkes-sols-master" manifest and building the "CAmkES Hello World application with events and dataports".
The changes I made are
* I edited the top level CAmkES file to set the affinity for two separate cores.
* Upped the Max Number of CPU nodes to 2
The rest of the config is pretty standard. I have it attached to this message.
The FSBL and ps7_init script I use are the standard ones created for the zc702 from the 2017.2 version of the Xilinx XSDK.
I am booting from jtag and first run the ps7_init script and then flash the fsbl and then the "capdl-loader-experimental-image-arm-zynq7000" that was built.
I am wondering if anyone is using a modified fsbl or ps7_init that does something else, if there is config value that I missed, or if it is still in development? If it is still in development I'd like to work with whoever is
Thanks,
Jesse Millwood
Hello,
I have a question about standard output. I have a camkes component than can
write into text-mode VGA buffer (basically it follows this simple example
http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like
to be able to redirect the kernel messages during startup to be printed on
screen using VGA buffer.
Once another component (either Linux in a VM, or some other camkes app)
will initialize, it will be able to take control over the screen output
(and for example show login window etc).
My questions is - is this possible with seL4? And if so, what would it
entail?
I guess in the minimal version, I would have to provide a different
implementation of seL4_DebugPutChar, is that correct?
The VGA standard seems to define the buffer to be at 0xB8000, so it should
be consistent between x86 platforms.
Regards
Michal
Hello,
we use the seL4 benchmark interface to feed Genode's trace
infrastructure with information about the CPU utilization of threads and
of idle times.
In general the integration was reasonable straightforward.
One minor point we had. It seems that the idle time of a CPU can only be
requested by a thread running on the vary same CPU. Requesting the CPU
idle times of a remote CPU (the calling thread is on another CPU) is not
supported, right ?
In principle we may start on each CPU a thread just for the sake of
requesting the idle utilization time, which however looks a bit of overkill.
We "kind of" circumvent the issue for us by changing the syscall
handling in the kernel in that regard, that the CPU number of the
requested target thread is taken instead that of the caller thread, e.g.
like this:
--- a/src/benchmark/benchmark_utilisation.c
+++ b/src/benchmark/benchmark_utilisation.c
@@ -36,6 +36,11 @@ void benchmark_track_utilisation_dump(void)
tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(lu_ret.cap));
buffer[BENCHMARK_TCB_UTILISATION] = tcb->benchmark.utilisation; /*
Requested thread utilisation */
+#if CONFIG_MAX_NUM_NODES > 1
+ if (tcb->tcbAffinity < ksNumCPUs)
+ buffer[BENCHMARK_IDLE_UTILISATION] =
NODE_STATE_ON_CORE(ksIdleThread,
tcb->tcbAffinity)->benchmark.utilisation; /* Idle thread utilisation */
+ else
+#endif
buffer[BENCHMARK_IDLE_UTILISATION] =
NODE_STATE(ksIdleThread)->benchmark.utilisation; /* Idle thread
utilisation */
#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
With this change, we still have to create a thread on every CPU (since
we need a capability for the syscall), but at least the threads must not
be running actively.
Does this change (the patch) make sense to you and is it worthwhile to
adjust in general on your side - or would you advise/envision another
approach/direction ?
(like specifying the cpu number for the idle times directly via the
syscall or having a explicit syscall just for cpu idle times [but there
are no specific thread idle capabilities as syscall parameter] etc.)
Another question:
Currently it seems that no idle CPU times are provided, as long as no
user thread is actively running on that specific CPU. We can handle it,
no problem in general - however we would have to adjust generic code
(which runs on 8 different kernels) specifically for seL4 to handle this
minor case.
Could this possibly be changed (easily) ?
Thanks,
Alex.
--
Alexander Boettcher
Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Hi,
I am trying to compile seL4 for the BBB. I am getting the following errors
when it gets to timer_service. I am following the instructions at
https://github.com/seL4/refos-manifest. I got past another compile error
by adding a typedef to device_timer.h for pstimer_t. Any help is
appreciated.
// tfp, added to avoid compiler error
typedef uint32_t pstimer_t;
[apps/timer_server] building...
[HEADERS]
[STAGE] autoconf.h
[CC] src/state.o
In file included from
/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:22:0,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24:
/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:
In function 'data_open_map':
/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:95:69:
warning: passing argument 6 o f 'data_open' from incompatible pointer
type [-Wincompatible-pointer-types]
d.dataspace = data_open(session, name, flags, mode, dspaceSize,
&errnoRetVal);
^
In file included from
/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:21:0,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27,
from
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24:
/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client.h:72:11:
note: expected 'int ** (*)()' but ar gument is of type 'int *'
seL4_CPtr data_open(seL4_CPtr session, char* name, int flags, int mode,
int size, int* errno);
^
[CC] src/device_timer.o
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:
In function 'device_timer_handle_irq':
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:146:5:
warning: implicit declaration of function 'timer _handle_irq'
[-Wimplicit-function-declaration]
timer_handle_irq(s->timerDev, irq);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:
In function 'device_timer_init':
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:239:5:
error: unknown type name 'timer_config_t'
timer_config_t config;
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:11:
error: request for member 'vaddr' in something not a structure or union
config.vaddr = ps_io_map(&io->opsIO.io_mapper,
dm_timer_paddrs[TIMER_ID],
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52:
error: 'dm_timer_paddrs' undeclared (first use in this function)
config.vaddr = ps_io_map(&io->opsIO.io_mapper,
dm_timer_paddrs[TIMER_ID],
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52:
note: each undeclared identifier is reported on ly once for each
function it appears in
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:11:
error: request for member 'irq' in something no t a structure or union
config.irq = dm_timer_irqs[TIMER_ID];
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:18:
error: 'dm_timer_irqs' undeclared (first use in this function)
config.irq = dm_timer_irqs[TIMER_ID];
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:243:16:
error: request for member 'vaddr' in something not a structure or union
if (!config.vaddr) {
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:19:
warning: implicit declaration of function 'ps_g et_timer'
[-Wimplicit-function-declaration]
s->timerDev = ps_get_timer(TIMER_ID, &config);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:17:
warning: assignment makes pointer from integer without a cast
[-Wint-conversion]
s->timerDev = ps_get_timer(TIMER_ID, &config);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:250:11:
error: request for member 'vaddr' in something not a structure or union
config.vaddr = ps_io_map(&io->opsIO.io_mapper,
dm_timer_paddrs[TICK_ID],
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:252:11:
error: request for member 'irq' in something no t a structure or union
config.irq = dm_timer_irqs[TICK_ID];
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:253:16:
error: request for member 'vaddr' in something not a structure or union
if (!config.vaddr) {
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:258:16:
warning: assignment makes pointer from integer without a cast
[-Wint-conversion]
s->tickDev = ps_get_timer(TICK_ID, &config);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:273:41:
error: request for member 'properties' in somet hing not a structure or
union
for (uint32_t i = 0; i < s->timerDev->properties.irqs; i++) {
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:274:19:
warning: implicit declaration of function 'time r_get_nth_irq'
[-Wimplicit-function-declaration]
int irq = timer_get_nth_irq(s->timerDev, i);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:282:44:
error: request for member 'properties' in somet hing not a structure or
union
for (uint32_t i = 0; i < s->tickDev->properties.irqs; i++) {
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:289:21:
warning: implicit declaration of function 'time r_start'
[-Wimplicit-function-declaration]
int error = timer_start(s->tickDev);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:310:13:
warning: implicit declaration of function 'time r_periodic'
[-Wimplicit-function-declaration]
error = timer_periodic(s->timerDev, TIMER_PERIODIC_MAX);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:
In function 'device_timer_get_time':
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:344:21:
warning: implicit declaration of function 'time r_get_time'
[-Wimplicit-function-declaration]
uint64_t time = timer_get_time(s->timerDev);
^
/home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:345:21:
error: request for member 'properties' in somet hing not a structure or
union
if (!s->timerDev->properties.upcounter) {
^
make[1]: ***
[/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/common/common.mk:265:
src/device_timer.o] Error 1
make: *** [tools/common/project.mk:331: timer_server] Error 2
Todd Peterson
Chief Embedded Systems Engineer
Management Sciences, Inc.
6022 Constitution Ave NE
Albuquerque, NM 87144
505-255-8611 (office)
505-205-7057 (cell)
This email message and any attachments are for the sole use of the
intended recipient(s) and may contain proprietary and/or confidential
information which may be privileged or otherwise protected from
disclosure. Any unauthorized review, use, disclosure or distribution is
prohibited. If you are not the intended recipient(s), please contact the
sender by reply email and destroy the original message and any copies of
the message as well as any attachments to the original message.
Hello,
we're happy to announce the version 17.08 of the Genode OS Framework.
Within the last release cycle (3-months) we upgraded our Genode/seL4
support from kernel version 3.2.0 to 6.0.0, enabled x86_64 and ARM
support, added UEFI support to the seL4 kernel and enabled SMP for x86.
A summary of changes and features are:
- Hardware-accelerated graphics for Intel Gen-8 GPUs
- The seL4 6.0 kernel on ARM and 64-bit x86 hardware
- Genode as Xen DomU
- Preliminary UEFI support for NOVA, base-hw, and seL4
- New server for capturing reports to files
- New runtime for the sequential execution of components
- Support for boot-time initialized frame buffer
- FatFS-based VFS plugin
- Extended non-blocking operation of the VFS
- Refined time handling
- Updated Muen separation kernel
The long version of the official release documentation:
https://genode.org/documentation/release-notes/17.08
All the best,
--
Alexander Boettcher
Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Hello,
we're are in progress of extending our Genode/seL4 support, namely
adding x86_64 and ARM support.
During this work I encountered on x86_64 some sporadically crashes of
the seL4 kernel. It happened during the debugging of our roottask on
seL4 in form of a page fault in the kernel ("KERNEL EXCEPTION") or a
static assertion in the kernel (see below).
>From my understanding, this shouldn't be possible based on your
verification work. Nevertheless, it happens reliable.
(To be fair, the roottask was in this scenario already a bit confused
and did things wrong - which however should never be enough to force the
kernel in an exception or assertion - I presume.)
I saved and stripped down the scenario which causes the kernel exception
with high reliably and hope you can re-produce it and find the root
cause. I stripped down the scenario to just the Genode image binary and
the steps we did to create the seL4 kernel from the vanilla sources.
Steps to reproduce:
qemu-system-x86_64 -no-kvm -serial stdio -m 512 -kernel sel4 -initrd
bomb_image.elf
The binaries of "bomb_image.elf" can be found at [1] and the kernel
"sel4" at [2].
The kernel is based on seL4 6.0 and a patch to pc99/autoconf.h (see
[0]). Beside that it is the vanilla 6.0 kernel:
https://github.com/seL4/seL4.git
git commit 8564ace4dfb622ec69e0f7d762ebfbc8552ec918
"update VERSION file to 6.0.0"
patch -p1 <~autoconfig.patch
BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 make
objcopy -O elf32-i386 kernel.elf.strip sel4
(Qemu complains otherwise about 64bit elf for boot)
The final "sel4" binary can be used with the "bomb_image.elf" and qemu
as pointed out above.
I tried Qemu 2.5.0 as shipped with Ubuntu 16.04 LTS and Qemu 2.8.0
(self-compiled). On real hardware the scenario typically leads after a
while (kernel booted, roottask booted, scenario starts to run) to a
reboot (without the messages or assertion as in the Qemu case, see below).
The tool-chain for Genode is based on GNU GCC 6.3.0 (see [3] and [4]).
The kernel was either compiled with Genode's toolchain (6.3.0) or with
the standard GCC as provided by Ubuntu 16.04 LTS (GCC 5.4.0).
On x86_32 I could not reproduce the issue. (On ARM I did not try.)
I hope the information are helpful - if you need more just ask.
Cheers,
Alex.
========== KERNEL EXCEPTION ==========
Vector: 0xe
ErrCode: 0x0
IP: 0xffffffff80720e60
SP: 0xffffffff80740e08
FLAGS: 0x6
CR0: 0x8000003b
CR2: 0x3007065 (page-fault address)
CR3: 0x1ffb000 (page-directory physical address)
CR4: 0x220
Stack Dump:
*0xffffffff80740e08 == 0xffffff8001a99b00
*0xffffffff80740e10 == 0xffffffff80729b1f
*0xffffffff80740e18 == 0x1
*0xffffffff80740e20 == 0xffffffff80721c59
*0xffffffff80740e28 == 0xffffffff
*0xffffffff80740e30 == 0x0
*0xffffffff80740e38 == 0xffffff801f02b740
*0xffffffff80740e40 == 0xffffff801f02b740
*0xffffffff80740e48 == 0x1
*0xffffffff80740e50 == 0xffffff8001a99000
*0xffffffff80740e58 == 0x7
*0xffffffff80740e60 == 0x59
*0xffffffff80740e68 == 0xffffff8001a99b00
*0xffffffff80740e70 == 0xffffffff80729cf3
*0xffffffff80740e78 == 0x9000000000000007
*0xffffffff80740e80 == 0xffffff8001a99059
*0xffffffff80740e88 == 0xffffff80ffffffff
*0xffffffff80740e90 == 0xffffffff80740f18
*0xffffffff80740e98 == 0xffffff800013c200
*0xffffffff80740ea0 == 0x10000
Halting...
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 10, Invocation tag: 16
or
seL4 failed assertion
'(cte_t*)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL &&
(cte_t*)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at
src/object/cnode.c:457 in function cteInsert
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 10, Invocation tag: 18
or a fault by the roottask (and not in the kernel). So - this is no
issue for the kernel:
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x18 with status 0x4
in thread 0xffffff800013c200 "child of: 'rootserver'" at address 0x20419cf
[0]
https://github.com/alex-ab/genode/blob/crash_sel4_kernel_vanilla/autoconfig…
[1]
https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.…
[2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4
[3] https://genode.org/download/tool-chain
[4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.05/
--
Alexander Boettcher
Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Hello to All,
I am trying to do some message passing between a vm component and a camkes
component.
I have tried by enabling the Vchan option on the build system and compiling
the helloworld linux user level program on a tk1. I received an error about
the /dev/vmm_manager not being able to open. What is the proper method of
setting up the Vchan communication for camkes-arm-vmm on a tk1?
Thank You
Dear,
I used "qemu-system-i386 -m 1024 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99"
It showed "Booting from ROM"
Thanks, Sincerely
------------------ Original ------------------
From: "devel-request";<devel-request(a)sel4.systems>;
Date: Thu, Aug 24, 2017 10:00 AM
To: "devel"<devel(a)sel4.systems>;
Subject: Devel Digest, Vol 39, Issue 26
Send Devel mailing list submissions to
devel(a)sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit
https://sel4.systems/lists/listinfo/devel
or, via email, send a message with subject or body 'help' to
devel-request(a)sel4.systems
You can reach the person managing the list at
devel-owner(a)sel4.systems
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Devel digest..."
Today's Topics:
1. Re: about camkesvm (Kofidoku.Atuah(a)data61.csiro.au)
----------------------------------------------------------------------
Message: 1
Date: Thu, 24 Aug 2017 00:00:19 +0000
From: <Kofidoku.Atuah(a)data61.csiro.au>
To: <devel(a)sel4.systems>
Subject: Re: [seL4] about camkesvm
Message-ID: <1503532819201.94096(a)data61.csiro.au>
Content-Type: text/plain; charset="iso-8859-1"
Hey Talos,
Sorry we didn't make this clearer on that page: those defconfigs build an x86-pc image; not an ARM image. Could you try running Qemu again, but with something similar to,
qemu-system-i386 -m <WHATEVER_RAM_SIZE_YOU_WANT> -kernel <SEL4_KERNEL_IMAGE> -initrd <CAPDL_INITRD_IMAGE>
And tell me what happens? Sorry for the inconvenience.
--
Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO
________________________________
From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com>
Sent: 22 August 2017 15:39
To: devel
Subject: [seL4] about camkesvm
Hi
I started the tutorial following the link:
https://wiki.sel4.systems/CAmkESVM
I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig
then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99
but the error is
Segmentation fault (core dumped)
what's wrong? Thanks
Sincerely
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://sel4.systems/pipermail/devel/attachments/20170824/cd4992b3/attachmen…>
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 39, Issue 26
*************************************
