Hi,
I am a student fron Nanjing university, a fresh man of microkernel,
specially,
know very little about the seL4.
Recently I accept a chellange about porting the lwip to sel4, on arch
of imx6,
does any one could give me a clue?
I found the source of camkes does have this code, could I do something
to port,
to make the lwip work? What my aim is make a tcp echo server.
Thank you for all of you help.
Best regards
from Xuguo Wang
Hello together,
I was wondering how you do get the execution time in seL4 if you are using
multiple threads.
In the initial thread I can use the timer as it is shown in the tutorial
about timers since I do have the bootinfo, vka, allocman and so on.
But how do I use the timer to measure the execution time of the other
threads without stopping their execution to "pull" the time from the
initial thread? Is it possible to share the timer or create new ones in the
other threads? Or is there another way to measure the execution time?
Some background information:
The threads have different VSpace's and CSpace's.
Used tutorials: seL4-tutorial 4, seL4-tutorial timer.
The other threads do not have a bootinfo in their environment.
Kind regards,
Chris
Hello,
I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode directly using the functions "install_monitor_hook()" and “switch_to_mon_mode()”. Is the sp in monitor mode appropriate? After calling smc in SVC mode, it hangs(do nothing in smc_handle()). What's wrong with it? Do you have any ideas?
Thank you!
Dongxu Ji
Hi, I want to change seL4 benchmark configuration in ninja build tool.
First, I want to change seL4's cache use.
Sencond, I want to change CPU core number.
How can I change these configuration?
When building the x86 demo for both 32 and 64 bit builds, it looks like the
kernel is still a 32 bit elf file regardless of the build and only the
sel4test-driver file is what is either 32 bit or 64 bit depending on which
is selected. Is this normal or should the kernel also be 64 bit on the 64
bit build?
--
Thank You,
Chris Rothrock
Senior System Administrator
(315) 308-1637
Hi Yanyan,
1. It doesn't set the NS bit to 1 in SCR(I just want it to return without
do anything). The arm_monitor_vector and the smc_handler():
arm_monitor_vector:
ldr pc, [pc, #28]
ldr pc, [pc, #24]
ldr pc, =smc_handler
ldr pc, [pc, #16]
ldr pc, [pc, #12]
ldr pc, [pc, #8]
ldr pc, [pc, #4]
ldr pc, [pc, #0]
smc_handler:
movs pc, lr
2. I didn't do any extra work other than the boot log:
..........
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
paddr=[20000000..203fbfff]
ELF-loading image 'kernel'
paddr=[10000000..10026fff]
vaddr=[e0000000..e0026fff]
virt_entry=e0000000
ELF-loading image 'sel4test-driver'
paddr=[10027000..10500fff]
vaddr=[8000..4e1fff]
virt_entry=25a6c
Enabling MMU and paging
Jumping to kernel-image entry point...
3. The initialization operations in platform_init.c:
set sp:
#define MONITOR_MODE (0x16)
#define MON_VECTOR_START (0x11000000)
#define VECTOR_BASE 0x11000000
#define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10)
asm volatile ( "mrs r1, cpsr\n\t"
"cps %0\n\t"
"isb\n"
"mov sp, %1\n\t"
"msr cpsr, r1\n\t"
::"I"(MONITOR_MODE),"r"(STACK_TOP));
copy monitor mode vector to MON_VECTOR_START and write into MVBAR:
uint32_t size = arm_monitor_vector_end - arm_monitor_vector;
printf("Copy monitor mode vector from %x to %x size %x\n",
(arm_monitor_vector), MON_VECTOR_START, size);
memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size);
asm volatile ("dmb\n isb\n");
asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START));
I enter into SVC mode by software interrupt and call the function smc():
asm (".arch_extension sec\n");
asm volatile ("stmfd sp!, {r3-r11, lr}\n\t"
"dsb\n"
"smc #0\n"
"ldmfd sp!, {r3-r11, pc}");
and then the problem arises.
Thank you,
Dongxu Ji
<Yanyan.Shen(a)data61.csiro.au> 于2018年8月28日周二 下午8:30写道：
> Hi,
>
> The smc_handle() in monitor.S, it does nothing but "movs pc, lr".
>
> Does it set the NS bit to 1 in SCR?
>
> Also, what did you do to ensure that 0x11000000 is not used by the kernel?
>
> Could you share the code (if possible) so that I could better understand
> the problem.
>
> Regards,
> Yanyan
>
>
> ------------------------------
> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of 冀东旭 <
> jidongxu1993(a)gmail.com>
> *Sent:* Tuesday, August 28, 2018 1:02 PM
> *To:* devel(a)sel4.systems
> *Subject:* [seL4] SMC in seL4
>
> Hello,
>
> I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode by setting the sp to STACK_TOP and copying arm_monitor_vector to MON_VECTOR_START according to the functions "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c".
>
> #define VECTOR_BASE 0x11000000(addr is not used by the seL4 kernel)
>
> #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10)
>
> #define MON_VECTOR_START 0x11000000(The VECTOR_BASE is the same as MON_VECTOR_START)
>
> The smc_handle() in monitor.S, it does nothing but "movs pc, lr". After calling smc in SVC mode, it hangs without any log. If I comment the "smc #0", it can return the caller successfully in usr mode.
>
> stmfd sp!, {r3-r11, lr}
> dsb
> smc #0
> ldmfd sp!, {r3-r11, pc}
>
> Is the sp in monitor mode appropriate? Or I need to do something else in initialization operations? What's wrong with it? Do you have any ideas?
>
> Thank you!
>
> Dongxu Ji
>
>
Hello,
I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I
initialize the monitor mode by setting the sp to STACK_TOP and
copying arm_monitor_vector to MON_VECTOR_START according to the
functions "install_monitor_hook()" and "switch_to_mon_mode()" in
"platform_init.c".
#define VECTOR_BASE 0x11000000(addr is not used by the seL4 kernel)
#define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10)
#define MON_VECTOR_START 0x11000000(The VECTOR_BASE is the same as
MON_VECTOR_START)
The smc_handle() in monitor.S, it does nothing but "movs pc, lr".
After calling smc in SVC mode, it hangs without any log. If I comment
the "smc #0", it can return the caller successfully in usr mode.
stmfd sp!, {r3-r11, lr}
dsb
smc #0
ldmfd sp!, {r3-r11, pc}
Is the sp in monitor mode appropriate? Or I need to do something else
in initialization operations? What's wrong with it? Do you have any
ideas?
Thank you!
Dongxu Ji
Hello,
I have tried to build sel4test following 'running SEL4' instruction.
It was successful for x86 platform, but when I try to build it for 'zyncmp' I've got an error:
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
gcc: error: unrecognized command line option '-mfloat-abi=soft'
Thank you,
Leonid
-- Build files have been written to: /home/lm/sel4test/build-zynqmp
lm@u-18:~/sel4test/build-zynqmp$ ninja
[2/235] Generating linker.lds_pp
FAILED: elfloader-tool/linker.lds_pp
cd /home/lm/sel4test/build-zynqmp/elfloader-tool && /usr/bin/gcc -march=armv8-a -marm -D__KERNEL_32__ -I/home/lm/sel4test/build-zynqmp/autoconf -I/home/lm/sel4test/build-zynqmp/kernel/gen_config -I/home/lm/sel4test/build-zynqmp/elfloader-tool/gen_config -I/home/lm/sel4test/build-zynqmp/libsel4/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vka/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4utils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4platsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4serialserver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4debug/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4test/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4muslcsys/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vmm/gen_config -I/home/lm/sel4test/build-zynqmp/projects/sel4test/apps/sel4test-driver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libutils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libplatsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libethdrivers/gen_config -P -E -o linker.lds_pp -x c /home/lm/sel4test/tools/seL4/elfloader-tool/src/arch-arm/linker.lds
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
[3/235] Building C object kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj
FAILED: kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj
ccache /usr/bin/gcc --sysroot=/home/lm/sel4test/build-zynqmp -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/arm -I../kernel/include/arch/arm/arch/32 -I../kernel/include/plat/zynqmp -I../kernel/include/plat/zynqmp/plat/32 -I../kernel/include/arch/arm/armv/armv8-a -I../kernel/include/arch/arm/armv/armv8-a/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=armv8-a -marm -D__KERNEL_32__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
gcc: error: unrecognized command line option '-mfloat-abi=soft'
[4/235] Creating C input file for preprocessor
ninja: build stopped: subcommand failed.
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
