Hi,
After hours of debugging I have discovered a quite nasty issue where
seL4_Wait() crash if I build the kernel without optimization (gcc option
-O0) on a pc99 tested with qemu.
How to reproduce: Just create an endpoint (from a vka) and call
seL4_Wait(). The simplest reproducer can be obtained from the hello-2
tutorial:
- Copy the main.c from the solution directory in the apps/hello-2/src/main.c
- Add the following codes right after the creation of vka (TASK 5, approx
line 150):
{
printf("WAITING----------------------------------------------\n");
seL4_Word myBadge;
vka_object_t ep_object = {0};
error = vka_alloc_endpoint(&vka, &ep_object);
ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n");
seL4_Wait(ep_object.cptr, &myBadge);
printf("---------------------------------------------- DONE!!\n");
}
Essentially the added code, creates an endpoint using vka and calls
seL4_Wait() on it... I expect the code to block forever since there are no
other threads that can unblock it...
- Build it and run it with:
make pc99_hello-2_defconfig
make
make simulate
Expected output:
Booting all finished, dropped to user space
4 untypeds of size 12
4 untypeds of size 13
[...]
6 untypeds of size 29
WAITING----------------------------------------------
- Now change the configuration using 'make menuconfig' and select:
seL4 Kernel -> Build Options -> Compiler optimisation flag (-O2)
and change it to -O0, save the new configuration.
- Rebuild and run:
make simulate
Now you get a kernel exception:
[...]
6 untypeds of size 29
WAITING----------------------------------------------
========== KERNEL EXCEPTION ==========
Vector: 0xd
ErrCode: 0xa658
IP: 0xe0118ce5
SP: 0xffaf7e28
FLAGS: 0x86
CR0: 0x8001003b
CR2: 0x0 (page-fault address)
CR3: 0x142000 (page-directory physical address)
CR4: 0x100290
Stack Dump:
*0xffaf7e28 == 0xe011a658
*0xffaf7e2c == 0x0
*0xffaf7e30 == 0x0
*0xffaf7e34 == 0xe011a658
*0xffaf7e38 == 0x8
*0xffaf7e3c == 0x202
*0xffaf7e40 == 0x0
*0xffaf7e44 == 0x0
*0xffaf7e48 == 0x10
*0xffaf7e4c == 0x7
*0xffaf7e50 == 0x0
*0xffaf7e54 == 0x0
*0xffaf7e58 == 0x0
*0xffaf7e5c == 0x0
*0xffaf7e60 == 0x0
*0xffaf7e64 == 0x0
*0xffaf7e68 == 0x0
*0xffaf7e6c == 0x0
*0xffaf7e70 == 0x0
*0xffaf7e74 == 0x0
Halting...
halting...
Kernel entry via Interrupt, irq 157
Version info:
- gcc: gcc (GCC) 4.8.5 20150623 (Red Hat 4.8.5-11)
- qemu: QEMU emulator version 2.0.0, Copyright (c) 2003-2008 Fabrice
Bellard
- Build environment: CentOS Linux release 7.3.1611 (Core)
Other info:
- gcc 4.8.5 doesn't seem to support the 'Nehalem' x86 microarchitecture,
so I am selecting the 'Generic' microarchitecture (Toolchain Options -> X86
microarchitecture)
- Even the tutorial 'hello-timer' fails exactly with the same exception
without any modifications if you build the kernel with -O0.
- Tested on a Beaglebone black: no problems compiling kernel with -O0
Regards,
Fabrizio Bertocci
Real-Time Innovations, Inc.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
