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
DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed).
Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released?
Thanks,
Chris Guikema
Hi all,
I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint?
Best Regards
-Daniel Wang
Hi all
I am new comer to sel4 community. I knew a little bit virtualisation
infrastructe(kvm/qemu), but I know little about sel4/docker.
I am investigating the proper implemenatation for running docker on sel4 on
arm64.
There might several ways I can figure out.Any suggestions are welcome :-)
1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might
be the
easiest way. It might have worked well on X86
2. porting l4linux to sel4. Don't know whether it is feasible?
3. run docker as sel4 service without linux. On this way, golang and its
library should be ported to sel4. Some missed syscalls which are needed by
docker should be implemenated.
Is there any other ways or anything else to make the implatation more
feasible?
---
Cheers,
Justin
I have been following the instructions "Fetching, Configuring and Building
seL4test" on this page https://docs.sel4.systems/GettingStarted.html.
Everything seems to work, but the initrd provided only runs a bunch of
tests and then exits. Is there another project that provides a shell or a
way for me to launch my own programs?
I have tried to follow the instructions on these pages
https://docs.sel4.systems/Hardware/Qemu/ and
https://docs.sel4.systems/CAmkESVM but the repo init command fails (404).
Thanks,
Baptiste.
Hi All,
I have noticed an alignment fault in the seL4 elfloader when running seL4 on an
AArch64 platform with dcache disabled in U-Boot. The alignment fault is caused
by reading the elf files header in the elfloader. The fault can be fixed
(hacked) by modifying the length of the elf file name, located before the elf
file header, to force a proper alignment.
Is the seL4 elfloader intended to be dependent on u-boot enabling the cache?
Hi all. I was having discussion about how secure handwritten asm code
compared to C code in
https://board.flatassembler.net/topic.php?p=206126#206117
and someone mentioned that there are undefined behavior in x86 instruction
set
How is these x86 undefined behavior handled in sel4?
Hello,
during some experimental work on Genode/seL4 and VM extensions, I
encountered the issue to trigger a kernel fault.
The symptom seems, that if a thread invokes seL4_VMEnter, but the actual
thread is not meant/supposed to run a VM, the kernel will (ever?/may?)
page fault with a nullpointer access - which effectively renders the
whole Genode system unusable.
A partial log is attached based on Genode on x86_64 with seL4 kernel
version 9.0.1.
The fault address points to [0], where the variable _expected_vmcs_ is
null and the kernel de-references it. I put a message before this line
and print the value of the variable (as visible in the log below).
The seL4 10.0.0 code looks similar, so I presume the same issue there .
(if the code is not verified - which according to the roadmap is not the
case [1] ?)
Cheers,
Alex B.
[0]
https://github.com/seL4/seL4/blob/0dd40b6c43a290173ea7782b97afbbbddfa23b36/…
[1] https://sel4.systems/Info/Roadmap/home.pml
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
diff --git a/src/arch/x86/object/vcpu.c b/src/arch/x86/object/vcpu.c
index cf74fa4..68a1dca 100644
--- a/src/arch/x86/object/vcpu.c
+++ b/src/arch/x86/object/vcpu.c
@@ -1540,6 +1540,7 @@ restoreVMCS(void)
}
#ifndef CONFIG_KERNEL_SKIM_WINDOW
+ userError("opps expected_vmcs=%p", expected_vmcs);
if (getCurrentCR3().words[0] != expected_vmcs->last_host_cr3) {
expected_vmcs->last_host_cr3 = getCurrentCR3().words[0];
vmwrite(VMX_HOST_CR3, getCurrentCR3().words[0]);
Boot config: parsing cmdline '/boot/sel4 disable_iommu'
Boot config: console_port = 0x1808
Boot config: debug_port = 0x1808
Boot config: disable_iommu = true
Detected 1 boot module(s):
module #0: start=0xfd58000 end=0xffff330 size=0x2a7330
name='/boot/image.elf'
Parsing GRUB physical memory map
Physical Memory Region from 0 size 89400 type 1
Physical Memory Region from 89400 size 16c00 type 2
Physical Memory Region from d2000 size 2000 type 2
Physical Memory Region from dc000 size 24000 type 2
Physical Memory Region from 100000 size bb17c000 type 1
Adding physical memory region 0x100000-0xbb27c000
Physical Memory Region from bb27c000 size 6000 type 2
Physical Memory Region from bb282000 size dd000 type 1
Adding physical memory region 0xbb282000-0xbb35f000
Physical Memory Region from bb35f000 size 12000 type 2
Physical Memory Region from bb371000 size 81000 type 4
Physical Memory Region from bb3f2000 size 1d000 type 2
Physical Memory Region from bb40f000 size 60000 type 1
Adding physical memory region 0xbb40f000-0xbb46f000
Physical Memory Region from bb46f000 size 1f9000 type 2
Physical Memory Region from bb668000 size 80000 type 4
Physical Memory Region from bb6e8000 size 27000 type 2
Physical Memory Region from bb70f000 size 8000 type 1
Adding physical memory region 0xbb70f000-0xbb717000
Physical Memory Region from bb717000 size 8000 type 2
Physical Memory Region from bb71f000 size 4c000 type 1
Adding physical memory region 0xbb71f000-0xbb76b000
Physical Memory Region from bb76b000 size c000 type 4
Physical Memory Region from bb777000 size 3000 type 3
Physical Memory Region from bb77a000 size 7000 type 4
Physical Memory Region from bb781000 size 1000 type 3
Physical Memory Region from bb782000 size 9000 type 4
Physical Memory Region from bb78b000 size 1000 type 3
Physical Memory Region from bb78c000 size 13000 type 4
Physical Memory Region from bb79f000 size 60000 type 3
Physical Memory Region from bb7ff000 size 1000 type 1
Adding physical memory region 0xbb7ff000-0xbb800000
Physical Memory Region from bb800000 size 800000 type 2
Physical Memory Region from bc000000 size 4000000 type 2
Physical Memory Region from e0000000 size 10000000 type 2
Physical Memory Region from feaff000 size 1000 type 2
Physical Memory Region from fec00000 size 10000 type 2
Physical Memory Region from fed00000 size 400 type 2
Physical Memory Region from fed1c000 size 4000 type 2
Physical Memory Region from fed20000 size 70000 type 2
Physical Memory Region from fee00000 size 1000 type 2
Physical Memory Region from ff000000 size 1000000 type 2
Physical Memory Region from 100000000 size 38000000 type 1
Adding physical memory region 0x100000000-0x138000000
Multiboot gave us no video information
ACPI: RSDP paddr=0xf68e0
ACPI: RSDP vaddr=0xf68e0
ACPI: RSDT paddr=0xbb7f07a2
ACPI: RSDT vaddr=0xbb7f07a2
***WARNING*** SKIM window not enabled, this machine is probably
vulernable to Meltdown (https://www.meltdownattack.com), consider enabling
Kernel loaded to: start=0x200000 end=0xaa5000 size=0x8a5000 entry=0x201209
ACPI: RSDT paddr=0xbb7f07a2
ACPI: RSDT vaddr=0xbb7f07a2
ACPI: FADT paddr=0xbb7f0a00
ACPI: FADT vaddr=0xbb7f0a00
ACPI: FADT flags=0xc2ad
ACPI: MADT paddr=0xbb7feb45
ACPI: MADT vaddr=0xbb7feb45
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x1
ACPI: MADT_APIC apic_id=0x4
ACPI: MADT_APIC apic_id=0x5
ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: 4 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x110f000 v_entry=0x2000018 v_start=0x2000000 v_end=0x310f000
p_start=0x10000000 p_end=0x1110f000
Moving loaded userland images to final location: from=0x10000000
to=0xaa5000 size=0x110f000
Starting node #0 with APIC ID 0
Mapping kernel window is done
Starting node #1 with APIC ID 1
Starting node #2 with APIC ID 4
Starting node #3 with APIC ID 5
Booting all finished, dropped to user space
virtual address layout of core:
overall [0000000000002000,00000000c0000000)
core image [0000000002000000,000000000310f000)
ipc buffer [000000000310f000,0000000003110000)
boot_info [0000000003110000,0000000003112000)
stack area [0000000040000000,0000000050000000)
boot module 'timer' (113344 bytes)
boot module 'test-vmm_sel4' (9912 bytes)
boot module 'config' (609 bytes)
boot module 'ld.lib.so' (937616 bytes)
boot module 'init' (352672 bytes)
Genode sculpt_vc-2-ge2fd5e5
2909 MiB RAM and 261141 caps assigned to init
...
<<seL4(CPU 0) [restoreVMCS/1543 T0xffffff80ba295400 "child of: 'child
of: 'rootserver''" @10000c9]: opps _expected_vmcs_=(nil)>>
========== KERNEL EXCEPTION ==========
Vector: 0xe
ErrCode: 0x0
IP: 0xffffffff80835236
SP: 0xffffffff8087ef18
FLAGS: 0x10086
CR0: 0x8001003b
CR2: 0x3298 (page-fault address)
CR3: 0xba043000 (page-directory physical address)
CR4: 0x6620
Stack Dump:
*0xffffffff8087ef18 == 0x10000c9
*0xffffffff8087ef20 == 0xffffffff80a93000
*0xffffffff8087ef28 == 0xffffffff80890040
*0xffffffff8087ef30 == 0x40
*0xffffffff8087ef38 == 0xffffff80ba295400
*0xffffffff8087ef40 == 0xffffffff8087efb8
*0xffffffff8087ef48 == 0xffffffffffffffe7
*0xffffffff8087ef50 == 0xffffffff80a93000
*0xffffffff8087ef58 == 0xffffffff80a93000
*0xffffffff8087ef60 == 0x0
*0xffffffff8087ef68 == 0x0
*0xffffffff8087ef70 == 0xffffffff80890040
*0xffffffff8087ef78 == 0xffffffffffffffff
*0xffffffff8087ef80 == 0xffffffff808357fe
*0xffffffff8087ef88 == 0xffffffff80a93000
*0xffffffff8087ef90 == 0xffffffff80838c93
*0xffffffff8087ef98 == 0x1001d4
*0xffffffff8087efa0 == 0x0
*0xffffffff8087efa8 == 0xffffffffffffffe7
*0xffffffff8087efb0 == 0xffffffff80839982
Halting...
halting...
Kernel entry via Interrupt, irq 157
Hello,
My platform is imx6q sabrelite and I have run sel4-test successfully. Now
I'm trying to create a new thread in the initial thread according to sel4
tutorial2. But it didn't run.
The code is shown below:
struct driver_env env;
allocman_t *allocman;
/* function to run in the new thread */
void thread_2(void) {
printf("thread_2: hallo wereld\n");
while (1);
}
int main(void)
{
int error;
reservation_t virtual_reservation;
seL4_BootInfo *info = platsupport_get_bootinfo();
seL4_DebugNameThread(seL4_CapInitThreadTCB, "sel4test-driver");
/* initialise libsel4simple */
simple_default_init_bootinfo(&env.simple, info);
/* create an allocator */
allocman = bootstrap_use_current_simple(&env.simple,
ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool);
/* create a vka */
allocman_make_vka(&env.vka, allocman);
/* create a vspace */
error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&env.vspace,
&data,
simple_get_pd(&env.simple),
&env.vka,
platsupport_get_bootinfo());
/* fill the allocator with virtual memory */
void *vaddr;
virtual_reservation = vspace_reserve_range(&env.vspace,
ALLOCATOR_VIRTUAL_POOL_SIZE,
seL4_AllRights, 1, &vaddr);
if (virtual_reservation.res == 0) {
ZF_LOGF("Failed to provide virtual memory for allocator");
}
bootstrap_configure_virtual_pool(allocman, vaddr,
ALLOCATOR_VIRTUAL_POOL_SIZE,
simple_get_pd(&env.simple));
/* Allocate slots for, and obtain the caps for, the hardware we will be
* using, in the same function.
*/
sel4platsupport_init_default_serial_caps(&env.vka, &env.vspace,
&env.simple, &env.serial_objects);
vka_t serial_vka = env.vka;
serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(&env);
/* Construct a simple wrapper for returning the I/O ports. */
simple_t serial_simple = env.simple;
/* enable serial driver */
platsupport_serial_setup_simple(&env.vspace, &serial_simple,
&serial_vka);
simple_print(&env.simple);
/* get our cspace root cnode */
seL4_CPtr cspace_cap;
cspace_cap = simple_get_cnode(&env.simple);
/* get our vspace root page diretory */
seL4_CPtr pd_cap;
pd_cap = simple_get_pd(&env.simple);
/* create a new TCB */
vka_object_t tcb_object = {0};
error = vka_alloc_tcb(&env.vka, &tcb_object);
/* initialise the new TCB */
error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap,
seL4_NilData, pd_cap, seL4_NilData, 0, 0);
/* give the new thread a name */
name_thread(tcb_object.cptr, "hello-2: thread_2");
UNUSED seL4_UserContext regs = {0};
/* set instruction pointer where the thread shoud start running */
sel4utils_set_instruction_pointer(®s, (seL4_Word)thread_2);
error=sel4utils_get_instruction_pointer(regs);
/* check that stack is aligned correctly */
const int stack_alignment_requirement = sizeof(seL4_Word) * 2;
uintptr_t thread_2_stack_top = (uintptr_t)thread_2_stack +
sizeof(thread_2_stack);
/* set stack pointer for the new thread */
sel4utils_set_stack_pointer(®s, thread_2_stack_top);
error=sel4utils_get_sp(regs);
/* actually write the TCB registers. */
error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, ®s);
/* start the new thread running */
error = seL4_TCB_Resume(tcb_object.cptr);
/* we are done, say hello */
printf("main: hello world \n");
return 0;
}
And I can get some output:
cspace_cap is 2
pd_cap is 3
tcb_object.cptr is 5f7
tcb_object.ut is 10000208
tcb_object.type is 1
tcb_object.size_bits is a
regs.pc is
9640
regs.sp is 3f24f0
Any advice about the issue?
Thank you,
Dongxu Ji
I think I've uncovered an interesting problem involving IPC between rump
kernels and seL4, and I'm curious if anyone has any thoughts on mitigating
it.
My use case is that I want a CAmkES component to be able to notify the rump
component to send a network packet.
However, as far as I can see:
CAmkES connector, mutex, and semaphore threads that run in a rump component
• can wait on their seL4 synchronization primitives
• ... but they can't call rump function calls because they're not rump
threads.
You can try to call, becuase you're running in the same address space as
the rump kernel, but if you call a rumpkernel function, the CAmkES thread
crashes when it reaches curlwp() becuase the calling thread is unknown to
the NetBSD kernel. Therefore you can't call sendto() inside, for example,
a notification callback or an seL4RPCCall handler, unless you can work out
a way to signal to the NetBSD kernel that you're calling into the kernel
from a foreign thread. Is this somehow possible through use of
rump_schedule() and rump_unschedule()?
... and the other possible path I can see also has problems:
rumpkernel created userspace threads (pthreads)
• can wait on seL4 synchronization primitives
• ... but if they do wait, they also unschedule the* entire rest of the
rump kernel and userspace* because every single rump thread (both kernel
and user) all run in one seL4 thread.
Therefore you can't do
while(true) {
semaphore_wait();
sendto(...);
}
without unscheduling the entire rump component when you hit the wait().
For this to work, there would need to be a way to have multiple seL4
threads for rump kernel execution so that one could block while the others
continue. That *is* done for interrupt and timer handling, but there's no
way I can see to set it up from a rump userspace program.
The only other possible path appears to be busy-wait polling which is
obviously very inefficient.
Any thoughts?
--Jason C. Wenger
