August 2014 - l4-hackers - example.com Site

strange response time question
by Yuxin Ren 06 Aug '14

06 Aug '14

Hi All, Now I am testing the response time in Fiasco, especially for the worse case. The results are strange. The worse case result are always around 2us. I have filtered out the timer interrupt, so I cannot understand what happened. I am using intel IA32 multi core cpu. Do you have any idea about what can cause the 2us delay? Thank you so much. Yuxin

5 8

response time in Fiasco
by Yuxin Ren 06 Aug '14

06 Aug '14

Hi All, Are there any papers or documentation talking about response time in Fiasco? I think this is an important aspect in Fiasco as it is designed for real time. Thank you. Yuxin

3 2

DDE-Kit
by Korbinian Ederer 05 Aug '14

05 Aug '14

Hello, I'm searching for some Informations about using the dde-kit. My goal is to use the SocketCan driver from Linux eith the l4re on an ARM BeagleBone Black (Omap3x). The Manual at http://os.inf.tu-dresden.de/ddekit/ did not work because of missing l4/sys/cache.h After some searching I discovered a copy of dde also in the fiasco snapshot in l4/pkg/dde/ but have no idea of how to use it. I would be very helpfull to get some advice about usefull documentation or some hints about the usage of dde Thanks a lot Korbinian Ederer

2 1

Do L4 Linux lack source code about Freescale i.MX6 Quad ?
by Taeung 04 Aug '14

04 Aug '14

Hello , L4 hackers I always appreciate L4 hackers. I've succeed boot "helloworld + L4/Fiasco" on Freescale i.MX6q_sabre_sd. So, I've try to build L4 linux (|Repository : svn co http://svn.tudos.org/repos/oc/l4linux/trunk l4linux|). I've configured for build L4 Linux such as.. ====================================================== System type ---> ARM system type (Allow multiple platforms to be selected) Multiple platform selection ---> ARMv7 based platforms (Cortex-A, PJ4, Scorpion, Krait) Build type Freescale i.MX family Freescale i.MX support ---> i.MX6 Quad/DualLite support ====================================================== But I've meet errors even so often. such as .. 1. ERROR: CONFIG_ARM_PATCH_PHYS_VIRT must not be enabled. => So, I've force to change CONFIG_ARM_PATCH_PHYS_VIRT=y to =n . 2. irq.c:16:26: error: 'L4X_NR_IRQS_V_DYN' undeclared here irq.c:46:14: error: 'L4X_IRQS_V_DYN_BASE' undeclared and irq.c:48:14: error: 'NR_IRQS_HW' undeclared => So, I've included "#include <asm/generic/irq-vectors.h>" and "#include <asm/mach-arm/generic/mach/irqs.h>". 3. l4.c:57:13: error: 'L4X_IRQS_V_STATIC_BASE' undeclared ...etc. => So, I've included "#include <asm/generic/irq-vectors.h>" and "#include <asm/mach-arm/generic/mach/irqs.h>". 4. drivers/built-in.o: In function `clk_disable': clk.c:867: multiple definition of `clk_disable' arch/l4/built-in.o:/home/taeung/workspace/l4linux/arch/l4/kernel/arch-arm/l4.c:73: first defined here drivers/built-in.o: In function `clk_enable': clk.c:919: multiple definition of `clk_enable' arch/l4/built-in.o:/home/taeung/workspace/l4linux/arch/l4/kernel/arch-arm/l4.c:65: first defined here make[1]: *** [vmlinux] Error 1 make: *** [sub-make] Error 2 => So, I delete this lines in l4linux/drivers/clk/clk.c. 7. undefined reference to `__pv_phys_offset' from signal.c , init.c, mm.h ....etc. My question is.... Is it's problem that my config is wrong or l4 linux lack source code about Freescale i.MX6 Quad ? * Refer to > /home/taeung/workspace/l4linux/arch/l4/kernel/*irq.c* /home/taeung/workspace/l4linux/arch/l4/include/asm/generic/*irq-vectors.h* /home/taeung/workspace/l4linux/arch/l4/kernel/*pm.c */home/taeung/workspace/l4linux/arch/l4/kernel/arch-arm/*l4.c** */home/taeung/workspace/l4linux/arch/l4/l4lxlib/generic/*irq_gen.c* /home/taeung/workspace/l4linux/drivers/clk/*clk.c */home/taeung/workspace/l4linux/arch/l4/kernel/arch-arm/*signal.c */home/taeung/workspace/l4linux/arch/l4/mm/arch-arm/*init.c */home/taeung/workspace/l4linux/include/linux/*mm.h *

3 2

seL4 boot issue
by Jorge Ventura 04 Aug '14

04 Aug '14

I am trying to boot seL4 on beaglebone white. I have an initial code just to configure the DDR2 memory at range 0x80000000-0xbfffffff. As we can see below, the start address is the virtual address 0xf0000000 but at this point I have no MMU configured. I was thinking that the segment .boot should be the code to prepare all details about MMU/D-CACHE/I-CACHE but it's not what gdb is understanding based in the elf header. Someone could explain to me how to boot this kernel; what do I have to consider. I guess that beaglebone is not supported but this is exactly my goal, to make seL4 boot on beaglebone. Any help or suggestion is very welcome. Sincerely, Jorge Ventura (gdb) load kernel.elf > Loading section .boot, size 0x10000 lma 0x80000000 > Loading section .text, size 0xf1ec lma 0x80010000 > Loading section .text.unlikely, size 0xd98 lma 0x8001f1ec > Loading section .rodata, size 0x4170 lma 0x8001ff84 > Loading section .data, size 0x8 lma 0x800240f4 > Start address 0xf0000000, load size 147708 > Transfer rate: 319 KB/sec, 3787 bytes/write. > (gdb) monitor poll > background polling: on > TAP: am335x.dap (enabled) > target state: halted > target halted in ARM state due to debug-request, current mode: System > cpsr: 0x6000019f pc: 0xf0000000 > MMU: disabled, D-Cache: disabled, I-Cache: disabled >

1 0