- Devel - lists.sel4.systems

Questions on CAMKES-ARM-VM Build and Components
by Daniel Wang 04 Oct '18

04 Oct '18

Hi all, It seems CAmkES-arm-vmm has been immigrated to cmake, How can I build it? I tried to build it by invoking: # ../init-build.sh -DCAMKES_VM_APP=tk1_vm -DPLATFORM=tk1 # ninja But it does not work. Also, thank for the detailed CAmkES X86 documents. I’m wondering does the VM Connector and kernel modules work for ARM architecture, TK1 or TK1-SOM specifically? Best Regards -Daniel Wang

3 6

Does seL4 provide an initrd with a shell?
by Baptiste Lepers 03 Oct '18

03 Oct '18

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.

3 4

Problem in Installing Genode OS
by Amit Goyal 02 Oct '18

02 Oct '18

Hi All, I tried to run Genode OS (on x86-64, i5, ubuntu 16.04) via 3 means but could not succeed. Can someone please suggest a possible way out. a) Running iso on virtual box [1] The system complete freezes and the corresponding error is: emR3Debug: rc=VERR_PGM_HANDLER_VIRTUAL_CONFLICT b) Running iso on Qemu [1] The interface appears with following options: Introduction, Web Browser, Seamless Linux, OpenGL, Qt4. but none of the options work on clicking. c) Building the kernel [2] After following all the instructions in [2] and creating the build directory, the last command <<make KERNEL=linux demo>> fails: Error: target 'demo' does not exist Makefile:211: recipe for target 'error_missing_targets' failed make: *** [error_missing_targets] Error 1 [1] https://genode.org/download/live-cds [2] https://genode.org/documentation/developer-resources/getting_started Also, can you please direct us towards any other operating system which is built using the seL4 microkernel. -- Thanks and Regards, Amit Goyal

2 1

Alignment fault without U-Boot Cache Enabled
by Nicholas Pahl 29 Sep '18

29 Sep '18

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?

2 1

How is undefined behavior in x86 ISA handled?
by Wean Irdeh 27 Sep '18

27 Sep '18

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?

2 1

x86 seL4 kernel bug - kernel page faults on seL4_VMEnter
by Alexander Boettcher 26 Sep '18

26 Sep '18

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

2 2

create a new thread in sel4
by Dongxu Ji 25 Sep '18

25 Sep '18

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(&regs, (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(&regs, thread_2_stack_top); error=sel4utils_get_sp(regs); /* actually write the TCB registers. */ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); /* 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

2 2

seL4 and rump kernel synchronization primitives limitations
by Jason Wenger 20 Sep '18

20 Sep '18

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

2 1

genode-sel4-arm -- Genode OS with seL4 on ARM hardware
by Adam Wiethuechter 18 Sep '18

18 Sep '18

Webite -- http://genodl4arm.critical.com/ Github -- https://github.com/CriticalTechnologiesInc/genode-sel4-arm Hello everyone, I have something rather exciting to share with you all today that we here at Critical Technologies Inc (CTI) have been working on for sometime now - the marriage of Genode OS and seL4 on native ARM hardware. We currently are supporting the Wandboard Quad (from Wandboard) and the SabreLite (from Boundary Devices). We are hoping to continue development targeting ARMv8a boards of interest; mainly the Raspberry Pi 3B and/or the Xilinx Zynq UltraScale+ ZCU102. This is obviously a work in progress with only the first step but we wished to share our documentation to the community for others to contribute and see what we are doing. I am happy to answer any questions you may have. -- 73's, Adam Wiethuechter, Jr Software Engineer Critical Technologies Inc. <adam.wiethuechter(a)critical.com>

2 1

Building/Running https://github.com/SEL4PROJ/docs with docker
by Axel Heider 17 Sep '18

17 Sep '18

Hi, I'm trying to build and run https://github.com/SEL4PROJ/docs with docker. Following the instrucitons: git clone https://github.com/SEL4PROJ/docs cd docs git submodule init git submodule update docker run --network=host -v $PWD:/host -w /host -it ruby bash -c 'bundle install && bundle exec jekyll serve' things fails with: ... Bundle complete! 8 Gemfile dependencies, 29 gems now installed. Bundled gems are installed into `/usr/local/bundle` Configuration file: /host/_config.yml Source: /host Destination: /host/_site Incremental build: disabled. Enable with --incremental Generating... Liquid Exception: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md in ApiDoc.md jekyll 3.6.2 | Error: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md Any hint what's failing here? I don't even see a folder "_repo", but I assume the build should create one? Thanks, Axel

2 1

Getting Started
by Dave Richards 13 Sep '18

13 Sep '18

I am in the process of reading the Getting Started documentation and building a development environment on Debian Linux. I thought RefOS would be the best example project to start with. When I execute the command: repo init -u ssh://git@github.com/seL4/refos-manifest -b master I get the response: Please make sure you have the correct access rights and the repository exists. Permission denied (publickey). fatal: Could not read from remote repository. Please make sure you have the correct access rights and the repository exists. fatal: cannot obtain manifest ssh://git@github.com/seL4/refos-manifest Apparently something has changed since the instructions were written. Dave

2 1

Notion of a User in seL4
by Amit Goyal 11 Sep '18

11 Sep '18

Hi All, As far as I understand, in seL4, the notion of a subject is similar to a thread (process). Each process has a different cspace and thus has different capabilities. Correct me, if I am wrong. Currently, we can make different components say server and client which run on the same seL4 kernel. They can interact with each other by creating endpoint and adding capability for that endpoint, in others cspace. Now, I want to extend it and run client and server on different host machines which run seL4. The threads (client and server) thus generated will be different users as per the standard linux convention. a) How does the communication happen in such a scenario in seL4? The problem which I see is how the capabilities for endpoint on one machine will be minted into other machine's process cspace. b) I also want to understand the notion of a user in seL4. -- Thanks and Regards, Amit Goyal

2 1

seL4 - getting the execution time of different threads
by Mr. Peace 10 Sep '18

10 Sep '18

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

4 5

Strange behavior when writing to memory mapped to a custom device in the VMM.
by Dan DaCosta 09 Sep '18

09 Sep '18

To Whom It May Concern: I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very puzzling. Consider the following code: #define idx(i) (i%16) for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){ mem[idx(i)] = *pArray; } where 'pArray' is the array representation of 'buf' and 'mem' is a memory mapped page set that corresponds to a page set of memory that is managed by a fault handler in the VMM (something I have installed myself using a 'DEV_CUSTOM' device). This code runs as I would expect. However, the follow code results in an assertion failure in the VMM: #define idx(i) (i%16) for(i = 0; i < 16; i++, pArray++){ mem[idx(i)] = *pArray; } The error report follows: 32 bit ARM insts not decoded -------- Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 0x2000046 Context: r0: 0xb6d2a050 r1: 0x0 r2: 0xb6ac76b8 r3: 0x4c r4: 0xb6d2a050 r5: 0xb6d2a8ec r6: 0x1 r7: 0xb6d2a050 r8: 0x7fb73000 r9: 0xad13cfff r10: 0xabe31310 r11: 0x19 r12: 0xb6d285d8 pc: 0x7f68f9a8 r14: 0x7f68f99c sp: 0xaf1c3c20 cpsr: 0x80000010 -------- Assertion failed: rt >= 0 (../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357) Some added information that may be helpful; if the strange modulo operation I am performing on the index is removed I receive a similar crash for both code snippets. Any thoughts on where I might look to get to the bottom of this problem would be helpful. Thanks! Dan DaCosta

2 1

CAmkES VMM platform support
by Grant Jurgensen 07 Sep '18

07 Sep '18

Hi all, I was hoping someone could clarify for me a couple of points regarding the CAmkES VMMs. First off, I have a program I want to run under a linux VM within CAmkES. However, it is written in a language which can be compiled to x86-64 but not IA-32. The impression I have gotten from the documentation and the examples is that the x86 CAmkES VMM only supports the 32-bit variant. Is that correct? My attempt to build the project targeting x86_64 has been met with errors (qemu complains "Huge page not supported by the processor"). Alternatively, said program can be compiled to ARMv6. In fact, the ultimate goal is for this project to run on an Odroid XU4, but as that platform is not currently supported by the CAmkES ARM VMM, I was hoping to build up the infrastructure as much as possible by testing it on any platform I could. The two platforms that are supported for the ARM VMM do not seem to have support on the qemu end though, so unfortunately I have no way of testing there either. Is it fair to assume that porting the Odroid implementation to the Odroid XU4 would be a non-trivial undertaking, or are they perhaps more similar than I am imagining? Thanks, Grant Jurgensen

2 4

issues in running sel4test on RISC-V rocket-chip FPGA
by Tuo Li 06 Sep '18

06 Sep '18

Hi guys, I have ported rocket chip (github.com/ucb-bar/fpga-zynq) on a ZCU102 FPGA board and it successfully runs riscv-linux. It's RV64G RISC-V. I am trying to run sel4test on the same hardware system. So far, the system gives no output after "Jumping to kernel-image entry point..." and seems to be stuck there. The same code has been tested on qemu simulator targeting spike 1.10 with the same device tree, following the online guide ( https://docs.sel4.systems/Hardware/RISCV.html) No problem. I have seen this thread ( http://sel4.systems/pipermail/devel/2018-August/002069.html) and used the solution provided for modifying the paddr range. I tried to add a few printf statements and even a fail statement in the boot.c file in kernel/src/arch/riscv/kernel/, which I guess is the first function executed after head.S. Same problem happens. Any suggestions? Thanks. Best regards, Tuo

2 2

Camkes Build Error
by Amit Goyal 05 Sep '18

05 Sep '18

Hi All, My Camkes has been working fine since now. Suddenly, it stopped working and produce the attached error log on running ninja. I am running it on x86 system (i5 processor), ubuntu 16.04 on qemu: I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution ninja Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

2 1

Does seL4 support raspberry pi 3B+
by talos 04 Sep '18

04 Sep '18

Hi I saw that seL4 supported raspberry pi 3B, did it support 3B+ now? If it did not, how can I modify it for 3B+? Thanks! Sincerely

2 1

SMC in seL4
by 冀东旭 31 Aug '18

31 Aug '18

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

2 1

seL4 benchmark configure
by 송대영 31 Aug '18

31 Aug '18

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?

2 1

32 bit vs 64 bit
by Chris Rothrock 30 Aug '18

30 Aug '18

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

2 1

Fwd: SMC in seL4
by Dongxu Ji 29 Aug '18

29 Aug '18

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 > >

2 2

SMC in seL4
by 冀东旭 28 Aug '18

28 Aug '18

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

2 1

building sel4test for zynqmp platform
by Leonid Meyerovich 27 Aug '18

27 Aug '18

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.

2 1

interesting i.MX8 hardware
by Corey Richardson 23 Aug '18

23 Aug '18

https://puri.sm/shop/librem-5/ A seL4 port for that platform might be nice... -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Demo build
by Kent.Mcleod＠data61.csiro.au 23 Aug '18

23 Aug '18

Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Mcleod, Kent (Data61, Kensington NSW) Sent: Thursday, August 23, 2018 11:28 AM To: Chris Rothrock; Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, August 23, 2018 10:22 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build I am using a newly initialized build directory for ia32. I can get a good, successful build for v 9.0.0 but not 10.0.0. As for x86_64, I was able to get a good build of x86_64 on 10.0.0 before but now I can't. It seems that there is a switch for cpio that is being set in the build that is invalid for that command. Possibly the latest version of cpio no longer support --reproducable switch since this is where it errors. On Wed, Aug 22, 2018 at 7:33 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, For the first issue - just making sure you initialised a new build directory for building ia32? The second issue - our HPET driver is very bare and doesn't support the full gamut of features. If you want to continue with this platform you'll need to improve the driver. Thanks, Anna. From: Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 23 August 2018 3:56 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build So my initial problem is actually resolved - it turns out I had the package 'ninja' installed, not 'ninja-build' which threw everything into a fit when I tried to actually use ninja. That being resolved, I was able to get a clean build of the 64 bit kernel (for x86) and made a simulated run. All looked well during the simulation. I do have 2 problems following up from this, however. When trying to use this build for a hardware boot (not simulated boot) I get an error (listed below). Also, for lengthy reasons, I also need to build a 32 bit version but when I do, this build fails. This is the build output from the ia32 build: Desktop:~/sel4test/build-ia32$ ninja [5/32] Linking CXX executable projects/sel4test/apps/sel4test-tests/sel4test-tests FAILED: : && ccache /usr/bin/g++ --sysroot=/home/jennifer/sel4test/build-ia32 -m32 -march=nehalem -D__KERNEL_32__ -nostdinc++ -g -march=nehalem -D__KERNEL_32__ -Wl,-m -Wl,elf_i386 -static -nostdlib -z max-page-size=0x1000 -u __vsyscall_ptr /home/jennifer/sel4test/build-ia32/lib/crt1.o /home/jennifer/sel4test/build-ia32/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/5/crtbegin.o projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/arch.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment_asm.S.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/helpers.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/main.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/benchmark_api.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/binding.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cache.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cnodeops.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cspace.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/domains.cxx.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/endpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ept.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/faults.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/fpu.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/frames.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/inc_untyped.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/interrupt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ioports.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/iopt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ipc.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/multicore.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/nbwait.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/pagetables.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/preempt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/regressions.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/schedcontext.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/scheduler.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/serial_server.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/sync.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/threads.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/trivial.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/vspace.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a /usr/lib/gcc/x86_64-linux-gnu/5/crtend.o /home/jennifer/sel4test/build-ia32/lib/crtn.o -o projects/sel4test/apps/sel4test-tests/sel4test-tests && : /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh collect2: error: ld returned 1 exit status [5/32] Generating from generated/plat_mode/machine/hardware.bf.pbf ninja: build stopped: subcommand failed. Here is the serial output of the x86_64 build boot: Boot config: parsing cmdline '' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa11000 end=0xd054f0 size=0x2f44f0 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e800 type 1 Physical Memory Region from 9e800 size 1800 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size ac722000 type 1 Adding physical memory region 0x100000-0xac822000 Physical Memory Region from ac822000 size a23000 type 2 Physical Memory Region from ad245000 size 69000 type 3 Physical Memory Region from ad2ae000 size 4b5000 type 4 Physical Memory Region from ad763000 size 430000 type 2 Physical Memory Region from adb93000 size 1000 type 1 Adding physical memory region 0xadb93000-0xadb94000 Physical Memory Region from adb94000 size 206000 type 4 Physical Memory Region from add9a000 size 156000 type 1 Adding physical memory region 0xadd9a000-0xadef0000 Physical Memory Region from adef0000 size 935000 type 2 Physical Memory Region from ae825000 size 4b000 type 1 Adding physical memory region 0xae825000-0xae870000 Physical Memory Region from ae870000 size 781000 type 2 Physical Memory Region from aeff1000 size f000 type 1 Adding physical memory region 0xaeff1000-0xaf000000 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feb80000 size 82000 type 2 Physical Memory Region from fec10000 size 1000 type 2 Physical Memory Region from fed00000 size 1000 type 2 Physical Memory Region from fed40000 size 5000 type 2 Physical Memory Region from fed80000 size 10000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 100000000 size 40000000 type 1 Adding physical memory region 0x100000000-0x140000000 Got VBE info in multiboot. Current video mode is 3 ACPI: RSDP paddr=0xf0490 ACPI: RSDP vaddr=0xf0490 ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 Warning: Your kernel was not compiled for the current microarchitecture. SKIM window for mitigating Meltdown (https://www.meltdownattack.com) not necessary for AMD and performance is being needlessly affected, consider disabling Kernel loaded to: start=0x100000 end=0xa11000 size=0x911000 entry=0x10123e ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 ACPI: FADT paddr=0xad269148 ACPI: FADT vaddr=0xad269148 ACPI: FADT flags=0x385a5 ACPI: MADT paddr=0xad2764a8 ACPI: MADT vaddr=0xad2764a8 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x10 ACPI: MADT_APIC apic_id=0x11 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x12 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x13 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec01000 gsib=24 ACPI: Not recording this IOAPIC, only support 1 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xf ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x35b000 v_entry=0x436000 v_start=0x400000 v_end=0x75b000 p_start=0xd06000 p_end=0x1061000 Moving loaded userland images to final location: from=0xd06000 to=0xa11000 size=0x35b000 Starting node #0 with APIC ID 16 Mapping kernel window is done Booting all finished, dropped to user space Received reserved IRQ: 7Skipping table FPDTD, unknown Skipping table FIDT▒, unknown Skipping table TCPA2, unknown Skipping table MSDMU, unknown Skipping table UEFIB, unknown Skipping table IVRSx, unknown Skipping table BGRT8, unknown Skipping table CRAT(, unknown Skipping table LUFT▒), unknown Warning: skipping table ACPI XSDT hpet_init@hpet.c:223 This driver expects hpet timer0 to be 64bit init_timer@main.c:192 [Cond failed: error] Failed to initialise default timer seL4 root server abort()ed Debug halt syscall from user thread 0xffffff80aeff5400 "sel4test-driver" halting... Kernel entry via Unknown syscall, word: 52 On Wed, Aug 15, 2018 at 8:30 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, That's strange, the build system definitely should not hang. However I need more information to help at all. Which OS version are you using (host and seL4)? Which gcc version and cmake version? Is there any output from the init-build script at all? Also, have you used a clean build directory after the initial failure? Cheers, Anna. From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 16 August 2018 3:16 AM To: devel(a)sel4.systems Subject: [seL4] Demo build Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 2

Demo build
by Chris Rothrock 23 Aug '18

23 Aug '18

Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 4

formal guarantee about preserving user behaviour
by Abhishek Anand 18 Aug '18

18 Aug '18

I have been reading the following paper for some time: Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. “Comprehensive Formal Verification of an OS Microkernel.” *Trustworthy Sytems*, 2014. https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abst… This is fantastic work and provides powerful guarantees about kernel behavior. However, I am confused about the guarantees about the behavior of user programs. The paper seems to suggest that in the abstract model of sel4, the user transitions are nondeterministic. page 21 bottom: "User transitions are specified as nondeterministically changing arbitrary user-accessible parts of the state space" Does this mean that the refinement theorem of sel4 (Theorem 3 in the above paper: the C implementation refines the abstract model) provides no guarantee about what the user program does, except that the user program does not mess up with the kernel state? Is it fair to say that the refinement theorem does not preclude the sel4 implementation from incorrectly changing the behavior of the user programs, e.g. by messing up the user state? I was expecting the abstract model in Isabelle to concretely specify how the user programs behave, perhaps according to x86/arm/riscv semantics extended with syscalls. Sorry if I misunderstood the paper. Thanks in advance for any clarification, Abhishek -- -- Abhishek http://www.cs.cornell.edu/~aa755/

3 5

Cap fault in send phase while spawning processes
by Noah Kennedy 17 Aug '18

17 Aug '18

Hi folks, I'm currently porting over a project from the Kbuild/Kconfig build system to the new CMake based build system and am having some issues. I'm trying trying to spawn additional processes (2+) and I am encountering an error when I attempt to call 'process_config_default_simple'. The message reads: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x4 in thread 0xffffff801ffb5400 "PRIMARY" at address 0x4252ba I loaded the executables which I am trying to spawn into the new processes into the cpio using a variation of the call MakeCPIO(archive.o $<TARGET_FILE:SECONDARY>;$<TARGET_FILE:TERTIARY>;...) where SECONDARY and TERTIARY are the executables which I am using later to spawn the new processes. The source code in question worked previously when using Kbuild, so I'm wondering if I'm doing something wrong with the CMake. Does anyone have any ideas? I've gone through the tutorials, but I'm still fairly new to seL4, so any help would be very much appreciated.

2 2

sel4test driver can not load big elf file
by Dd Nirvana 17 Aug '18

17 Aug '18

Hi guys, When I try to run some application tests(written by myself) on sel4test (x86-qemu environment), I found the following errors. *Starting test suite sel4test* *Starting test 0: Test that there are tests* *Starting test 1: APPTEST1* *vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1* *new_pages_at_vaddr@vspace.c:330 Failed to allocate page number: 0 out of 1* *load_segment@elf.c:103 ERROR: failed to allocate frame by loadee vka: 10* *sel4utils_elf_load_record_regions@elf.c:519 Failed to load segments* *sel4utils_configure_process_custom@process.c:596 Failed to load elf file* It seems seL4test's driver can not load tests with very large size? I also tried to change the "DRIVER_UNTYPED_MEMORY" size from "(1 << 25)" to "(1 << 27)", but it also failed. Any advices about the issue? Dong

2 1

create process in seL4
by Leonid Meyerovich 16 Aug '18

16 Aug '18

Hello, Is there any way to define untyped size while creating process using library functions? process_config_default_simple(simple_t *simple, const char *image_name, uint8_t prio) sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *vka, vspace_t *spawner_vspace, sel4utils_process_config_t config) The second question is how to initialize allocator (probably I should use bootstrap_use_current_1level, but how where should I get parameters?) in created process to support memory allocation operations? Thank you, Leonid ________________________________ 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.

2 2

Interrupts in SEL4
by Sathya Narayanan N 16 Aug '18

16 Aug '18

Hi Experts, We are trying to port sel4 to Shakti FPGA. It is similar to Rocket FPGA. The memory footprint is 256 mb [0x80000000 - 0x8fffffff]. Shakti support -march=imafd. A single core 64 bit design. The run in FPGA stops at *"memcpy((char *)dest_vaddr + phys_virt_offset, (char *)elf + data_offset, data_size);*" called in the function " *unpack_elf_to_paddr()".* Earlier it stopped just at the memset (one line above). I manually commented out memset part and made it to run till memcpy. So I doubt it has something to do with wrong memory access. can someone please explain me the above said function (blue color) ? what could be reasons for memcpy to hung ? Can someone please guide me to the area in code where memory related interrupts are coded ? We have the latest upstream of SEL4 (Aug 10). It has the dornerworks upstream changes. We are trying to load at 0x88000000. The image works well in spike simulation. *Commands to build:* ../init-build.sh -DPLATFORM=spike -DKernelPlatformSpikeRocketChip=ON -DSIMULATION=FALSE -DRISCV64=TRUE ninja *Snapshot of the run in FPGA:* DTB { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-dev"; model = "shakti,spike-bare"; cpus { #address-cells = <0x00000001>; #size-cells = <0x00000000>; timebase-frequency = <0x00989680>; cpu@0 { device_type = "cpu"; reg = <0x00000000>; status = "okay"; compatible = "riscv"; riscv,isa = "rv64imafd"; mmu-type = "riscv,sv39"; clock-frequency = <0x3b9aca00>; interrupt-controller { #interrupt-cells = <0x00000001>; interrupt-controller; compatible = "riscv,cpu-intc"; linux,phandle = <0x00000001>; phandle = <0x00000001>; } } } memory@80000000 { device_type = "memory"; reg = <0x00000000 0x80000000 0x00000000 0x10000000>; } soc { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-soc", "simple-bus"; ranges; } uart { compatible = "shakti,uart0"; reg = <0x00000000 0x00011200 0x00000000 0x00001000>; } htif { compatible = "ucb,htif0"; } } ELF-loader started on paddr=[80200000..8060e7d7] elf check file returned 1 elf check file returned 1 ELF-loading image 'kernel' paddr=[88000000..8802bfff] vaddr=[ffffffff80000000..ffffffff8002bfff] virt_entry=ffffffff80000000 configured page table levels = 3...... elf check file returned 1 image size 2b350 *(char *)dest_vaddr + phys_virt_offset = ffffffff88000000 * *phys_virt_offset = 8000000 * *(char *)elf + data_offset, = ffffffff8020f854* *started memcpy* ------------------------------------------------------------> *Hangs* -- regards, Sathya

2 2

seL4 benchmark cache unable.
by 송대영 15 Aug '18

15 Aug '18

Hi, I have question about sel4 benchmark cache unable. I want to benchmark sel4 without cache but I don't know where is the location that configures cache. Would you give advice?

2 1

Questions about sel4bench IPC statistic in the website
by Zihan Yang 14 Aug '18

14 Aug '18

Hi, Your website(https://sel4.systems/About/Performance/home.pml) lists the IPC benchmark result, and I wonder is the x64 result for both fastpath, or both slowpath, or one fastpath and the other slowpath? According to the evaluation of my own on x64 kabylake, the fastpath client->server takes about 600 cycles, and slow path client->serve takes over 1100 cycles. But the website data is 1465 and 780, but it does not show whether it is fastpath or slow path. It looks like that the website data has client->server goes into slowpath(maybe because of lower priority), and the server->client goes into fastpath. Is it so? Thanks, Zihan

2 3

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

Hi, I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader. The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated. Function under review: *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* /* Parse size/length headers. */ dest_vaddr = elf_getProgramHeaderVaddr(elf, i); data_size = elf_getProgramHeaderFileSize(elf, i); data_offset = elf_getProgramHeaderOffset(elf, i); /* Load data into memory. */ * memcpy((char *)dest_vaddr + phys_virt_offset,* * (char *)elf + data_offset, data_size);* * printf("loaded data into memory \n"); -----> Stuck Here !* } } *Can anyone give me a clue on whatsoever to check here ? **It worked perfectly in spike simulation.* *RISCV FPGA configuration* - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million. *Snap shot* ELF-loader started on paddr=[80200000..8060dc17] elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 ELF-loading image 'kernel' paddr=[c0000000..c002dfff] vaddr=[ffffffff80000000..ffffffff8002dfff] virt_entry=ffffffff80000000 elf file is valid image is aligned phy range valiidngetting size of image elfFile->e_phnum = 1 elfFile->e_phnum = 1 memset each segment in the elf file loading each segment in the elf file 2d018 elfFile->e_phnum = 1 loading data into memory char *)dest_vaddr + phys_virt_offset = ffffffffc0000000 (char *)elf + data_offset, = ffffffff8020a694 ----- ? -- regards, Sathya

2 2

Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

Hi, I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader. The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated. Function under review: *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* /* Parse size/length headers. */ dest_vaddr = elf_getProgramHeaderVaddr(elf, i); data_size = elf_getProgramHeaderFileSize(elf, i); data_offset = elf_getProgramHeaderOffset(elf, i); /* Load data into memory. */ * memcpy((char *)dest_vaddr + phys_virt_offset,* * (char *)elf + data_offset, data_size);* * printf("loaded data into memory \n"); -----> Stuck Here !* } } *Can anyone give me a clue on whatsoever to check here ? **It worked perfectly in spike simulation.* *RISCV FPGA configuration* - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million. -- regards, Sathya

2 1

Paging in SEL4
by Sathya Narayanan N 10 Aug '18

10 Aug '18

Hi Experts, Could some one help me in understanding the paging in SEL4 ? the MMU architecture ? Is there any material to understand ? -- regards, Sathya

4 4

compile error aarch64 platform hikey
by Thad Seeberger 10 Aug '18

10 Aug '18

I really want to target zcu102 but i../init-build.sh -DPLATFORM=zynqmp unsupported platform so I decided to target another A53 target I dont know if this is the proper way to get started on this. ../init-build.sh -DPLATFORM=hikey -DAARCH64=1 ninja [maddthad@localhost build-zcu102]$ ccache /usr/lib64/ccache/aarch64-linux-gnu-gcc --sysroot=/home/maddthad/sel4/sel4test/build-zcu102 -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/hikey -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/64 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a/64 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/sel4test/apps/sel4test-driver/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv8-a+crc -D__KERNEL_64__ -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -mgeneral-regs-only -fpic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ‘;’, ‘,’ or ‘)’ before ‘dest’ void *memcpy(void *restrict dest, const void *restrict src, size_t n) gcc ver: COLLECT_GCC=/usr/bin/aarch64-linux-gnu-gcc COLLECT_LTO_WRAPPER=/usr/libexec/gcc/aarch64-linux-gnu/4.8.5/lto-wrapper Target: aarch64-linux-gnu gcc version 4.8.5 20150623 (Red Hat 4.8.5-16) (GCC) thx Thad

3 3

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 09 Aug '18

09 Aug '18

> > Hi, > > I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf > loader. > > The function stuck is memcpy. I have added prints and I am not progressing > after the last memcpy call in unpack_elf_to_paddr(). All kinds of input > appreciated. > > > Function under review: > *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* > > /* Parse size/length headers. */ > dest_vaddr = elf_getProgramHeaderVaddr(elf, i); > data_size = elf_getProgramHeaderFileSize(elf, i); > data_offset = elf_getProgramHeaderOffset(elf, i); > > /* Load data into memory. */ > > * memcpy((char *)dest_vaddr + phys_virt_offset,* > * (char *)elf + data_offset, data_size);* > * printf("loaded data into memory \n"); -----> Stuck Here > !* > } > > } > > *Can anyone give me a clue on whatsoever to check here ? **It worked > perfectly in spike simulation.* > > *RISCV FPGA configuration* - It supports IMAFD. It has already booted > linux. Kernel is loaded at physical address 80 million. > -- regards, Sathya

1 0

sel4 thread creation problem
by Leonid Meyerovich 08 Aug '18

08 Aug '18

Hello, My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial thread: int err; seL4_timer_t timer; vka_object_t ntfn_object; ntfn_object.cptr = 0; err = vka_alloc_notification(&_env.vka, &ntfn_object); assert(err == 0); err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, &_env.simple, ntfn_object.cptr, &timer); err = ltimer_set_timeout(&timer.ltimer, NS_IN_MS * 20, TIMEOUT_PERIODIC); assert(err == 0); int count = 0; int count_s = 0; while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); count++; if ((count / 50) * 50 == count) { count_s++; printf("-----------------timer=%d %d\n", count, count_s); } } It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 sec, but it's not an issue right now) Now I am trying to move all this timer code into a new thread, which I have created in the same vspace // create thread void initSleep(env_t penv) //seL4_BootInfo *info) { _penv = penv; vka_object_t tcb_object = {0}; int error = vka_alloc_tcb(&penv->vka, &tcb_object); seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&penv->simple); seL4_CPtr pd_cap; pd_cap = simple_get_pd(&penv->simple); seL4_CPtr ipc_page; seL4_Word ipc_buffer = (seL4_Word)vspace_new_ipc_buffer(&penv->vspace, &ipc_page); error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page); error = seL4_TCB_SetPriority(tcb_object.cptr, simple_get_tcb(&penv->simple), seL4_MaxPrio); seL4_UserContext regs = { .pc = (seL4_Word)time_thread, .sp = (seL4_Word)thread_time_stack }; error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); error = seL4_TCB_Resume(tcb_object.cptr); } And this is thread function static void time_thread(void) { _tick_number = 0; int count_s = 0; init_timer(); while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(timer_ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); _tick_number++; if ((_tick_number / 50) * 50 == _tick_number) { count_s++; printf("-----------------timer=%lu %d\n", _tick_number, count_s); } } The system crashed: setup_irq@timer.c:81 Setting up IRQ 8000000000000000 <<seL4(CPU 0) [handleInvocation/281 T0xff8000001200 "child of: 'rootserver'" @42195c]: Invocation of invalid cap #48762580.>> Here is dump: /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23 421938: d53bd066 mrs x6, tpidrro_el0 setup_irq(): /home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85 error = seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, irq->badged_ntfn_path.capPtr); 42193c: f85c8340 ldur x0, [x26,#-56] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165 register seL4_Word msg1 asm("x3") = *in_out_mr1; 421940: d2800003 mov x3, #0x0 // #0 seL4_SetCap(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59 421944: f901e8c1 str x1, [x6,#976] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166 register seL4_Word msg2 asm("x4") = *in_out_mr2; 421948: d2800004 mov x4, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167 register seL4_Word msg3 asm("x5") = *in_out_mr3; 42194c: d2800005 mov x5, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170 register seL4_Word scno asm("x7") = sys; 421950: 92800007 mov x7, #0xffffffffffffffff // #-1 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161 register seL4_Word info asm("x1") = info_arg; 421954: d2941001 mov x1, #0xa080 // #41088 421958: f2a00021 movk x1, #0x1, lsl #16 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171 asm volatile ( 42195c: d4000002 hvc #0x0 seL4_MessageInfo_get_label(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/shared_types_gen.h:49 I suspect that my thread initialization is not right, can somebody see any problem? Thank you, Leonid ________________________________ 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.

2 3

Re: [seL4] camkes-project error
by talos 08 Aug '18

08 Aug '18

Hi I changed it to: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DCAMKES_APP=adder -DSIMULATE=1 -Dc_std=gnu99 and it worked for ninja build. But when started simulation by ./simulate the error is: qemu-system-arm: -kernel images/capdl-loader-image-arm-imx6: unsupported machine type Use -machine help to list supported machines How could I choose the machine type? Thanks! Sincerely

3 2

Combined Ada and C project with Kbuild
by Noah Kennedy 08 Aug '18

08 Aug '18

I'm currently working on a project that is using the old Kbuild system. The project has been primarily implemented in C, however we would like to integrate some Ada code into the project. I am familiar with how to use gcc and makefiles to build polyglot projects on linux, however, I have no idea how to do so with the Kbuild system, as I cannot find out how to build anything other than .c or .h files with the makefile. How would I go about adding ada code to the project? Is there any way for me to build .ads and .adb, or .a files with the makefile?

2 1

camkes-project error
by talos 07 Aug '18

07 Aug '18

Hi, When I followed this tutorial: https://sel4.systems/Info/CAmkES/GettingStarted.pml The error is: /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.o: In function `post_main': /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.c:601: undefined reference to `component_control_main' collect2: error: ld returned 1 exit status /home/talos/camkes-project/build/arm/imx31/simple/camkes-gen.mk:630: recipe for target 'echo.instance.bin' failed make[1]: *** [echo.instance.bin] Error 1 tools/common/project.mk:333: recipe for target 'simple' failed make: *** [simple] Error 2 But when I followed this tutorial: https://docs.sel4.systems/CAmkES/ the error is: [230/232] Building C object elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj FAILED: /usr/bin/arm-none-eabi-gcc --sysroot=/home/talos/camkes-project/build -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/imx6 -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/32 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a/32 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv7-a -marm -D__KERNEL_32__ -g -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -fno-pic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ';', ',' or ')' before 'dest' void *memcpy(void *restrict dest, const void *restrict src, size_t n) ^ ninja: build stopped: subcommand failed. I used Ubuntu 16.04 x86_64 Thanks

3 2

How to write safe C code for free?
by Wean Irdeh 04 Aug '18

04 Aug '18

Hello. I'm a poor person looking for an advice. I know this is the right place since all of you have huge expertise in formal verification. I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?

3 2

using libmuslc library question
by Leonid Meyerovich 03 Aug '18

03 Aug '18

Hello, I have tried to call usleep() function from seL4 'main' thread and it crashes the system with error: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x200 with status 0x82000006 in thread 0xff807bfe2200 "rootserver" at address 0x200 With stack: How to use this library? Thank you, Leonid

1 0

about compile error
by wong xuguo 03 Aug '18

03 Aug '18

Dear Sir/Lady, This is a student from china, I am very interested in the sel4, works on the camkes, When I first compile the project camkes, I met a problem: camkes.c:502: undefined reference to `component_control_main' I know this means it not implemented this function, but this function seems produced by a auto method, so could you tell how to solve this problem? I follow the command: https://docs.sel4.systems/CAmkES/ to compile the : repo init -u https://github.com/seL4/camkes-manifest.git

2 1

Question on multi-partition seL4 image/load for x86
by Jim Marek 02 Aug '18

02 Aug '18

seL4 Developers/SMEs: Does anyone have a seL4 load/configuration that includes more than 2 partitions with at least 2 of the partitions each having a dedicated Ethernet interface assigned to it? I am focused on an x86 host platform. Currently I have a Dell 7910 19" rack unit I am wanting to host on and it has 4 Ethernet ports. Thanks, Jim Marek Enterprise Architect Rockwell Collins

2 3

Question about wrapper files
by Holm, Elinor M 30 Jul '18

30 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are there for testing, or something else? Elinor Holm Software Engineer 781-410-5221 This message and/or attachments may include information subject to GDC4S S.P. 1.8.6 and GD Corporate Policy 07-105 and are intended to be accessed only by authorized recipients. Use, storage and transmission are governed by General Dynamics and its policies. Contractual restrictions apply to third parties. Recipients should refer to the policies or contract to determine proper handling. Unauthorized review, use, disclosure or distribution is prohibited. If you are not an intended recipient, please contact the sender and destroy all copies of the original message.

3 2

CAmkES 3.5.0 Build Error
by Amit Goyal 27 Jul '18

27 Jul '18

Hi, I am running CAmkES 3.5.0 on Ubuntu 16.04, 64 Bit, i5 machine, CMake 3.11.4. I am getting the following error on running ../init --plat pc99 --tut hello-camkes-1 --solution (although seL4 10.0.0 works perfectly fine). ------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 58, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL=hello-camkes-1 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- The C compiler identification is GNU 5.3.1 -- The CXX compiler identification is GNU 5.3.1 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FA... (295 more, please see e.stdout) STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at tools/camkes/camkes.cmake:581 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/tools/camkes/camkes/runner/__main__.py", lin... (614 more, please see e.stderr) -------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a way around? -- Thanks and Regards, Amit Goyal

2 2

Question about wrapper files
by Holm, Elinor M 26 Jul '18

26 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are they for testing, or something else? Elinor Holm

1 0

Image lies outside of usable physical memory v2
by Jeremy Fields 26 Jul '18

26 Jul '18

http://sel4.systems/pipermail/devel/2016-July/000918.html I'm running into the same issue, with likely the same cause. I wanted to see if there is any further insight that can be given on this? I'm guessing there hasn't been any updates to seL4's memory allocation in this aspect. (I'm using seL4 9.0.1) My naive attempt of commenting out that particular check in seL4 just results in the machine hard resetting when it runs (if only it were that easy). >Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner. (2016) Any chance this is on a roadmap? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Implementing a Filesystem on CAmkES
by Grant Jurgensen 25 Jul '18

25 Jul '18

Hello all, I was hoping to get some advice on how to implement a filesystem on my CAmkES project. For now I'm targeting FAT32, but that is flexible. So far, my plan is to port the libsdhcdriver to my platform (which shouldn't be too bad. I'm targeting exynos5, and I see exynos4 is already supported). After that, I assume I'm on my own when it comes to creating a filesystem interface. Perhaps there is an existing library for this that can hook into any standard SD controller implementation? Finally, is there an easy way to integrate said filesystem into musllibc such that one could use the standard open/read/write/close functions? Does this sound like the best way to go, or am I missing a simpler solution? Thanks, Grant

3 2

Re: [seL4] Understanding how SEL4 recognises UART on board
by Sathya Narayanan N 19 Jul '18

19 Jul '18

Hi Experts, I am curious to know how SEL4 recognises the existence of UART on the board and mapped to a particular memory address. I see there is no DTB/ DTS files read from memory. could someone help me understand the concept here ? Or is it something hardcoded in the kernel ? -- regards, Sathya

2 1

RISC-V - sel4test and sel4bench running on SiFive's Unleashed Platform
by Hesham Almatary 18 Jul '18

18 Jul '18

Hi everyone, I pushed my local seL4/RISC-V work to GitHub which contains the following new features: * A new option to run seL4 in machine mode. * A port of seL4 to QEMU's SiFiveU and virt platforms. * DTB parsing in seL4 to read and use UARTs when available. * Ported seL4 to run on VC707 FPGA Freedom Unleashed platform. * Initial Benchmarking support in seL4. * Initial sel4bench port that can measure IPC and trap timing. Link for more details: http://heshamelmatary.blogspot.com/2018/07/new-sel4test-and-sel4bench-relea… -- Hesham

1 0

Porting sel4 on RISCV architecture
by Sathya Narayanan N 16 Jul '18

16 Jul '18

Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya

3 4

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks again for the reply. I was looking for the foolproof way to write safe C code, but seems like the best way to go forward is to carefully design and code. Your advice is helpful to me. On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > >> Clang does have a static analyzer builtin that can be help in some > cases. That being said, the best way forward is for you as a developer to > understand the types of code that can lead to problems and not rely > entirely on a static analyzer. > > >>> >>> >

1 0

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks a lot for the reply. What is your opinion on static checking tool and safe subset of C? Does that help? On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > Hello Wean, > > It is certainly possible to learn how to program in C without spending any > money; all it requires is a basic toolchain and a willingness to learn. > don't sell yourself short by hinting that you might be "stupid" (you almost > certainly aren't). > > In order to get started with C I suggest setting up an environment to > experiment in; for that look into installing LLVM/Clang ( > http://releases.llvm.org/) there are pre-built binaries for most major > operating systems. Once that is done all you need is a text editor (Notepad > on Windows or one of the other many free options) and some patience. As for > tutorials and resources, some options are: > > - Searching on Google for "c tutorial"; one result that looks interesting > is http://www.learn-c.org/. > - Finding an open source project that interests you and trying to > understand the code then implement a change. > - While not free, may people swear by the K&R book as a great resource to > start. > > In terms of writing code that is free of undefined behaviour and > vulnerabilities your best bet is to learn what code constructs cause those > to occur and how to avoid them. A great book for this is The Art of > Software Security Assessment by Mark Dowd, there is a PDF of Chapter 6 (C > Language Issues) available at https://trailofbits.github.io/ > ctf/vulnerabilities/references/Dowd_ch06.pdf. > > Learning about C, undefined behaviour, and vulnerabilities doesn't happen > overnight so be patient and enjoy the journey. > > --Dean > > > >

1 0

Help ! Simulating SEL4 with Zero testcases running
by Sathya Narayanan N 13 Jul '18

13 Jul '18

Hi Experts, I am running sel4 simulation on spike. I want to disable test cases from running. I tried setting default value "" from ".*" in Kconfig file. Is this enough ? Or is something else to be done ? -- regards, Sathya

2 2

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 13 Jul '18

13 Jul '18

?Hey Thad, Thanks for catching that: it turns out that we weren't passing -nostdlib to the linker when linking the ELFLoader, so the cross-toolchain's linker was trying to link the ELFLoader against the cross toolchain's libc, but it shouldn't be doing that and it should instead be using our libmuslc. A fix has been pushed out and you should be seeing it shortly. Thanks for your patience, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

seL4 vm examples with Qemu
by Mike Clark 12 Jul '18

12 Jul '18

Is it currently possible to boot the camkes-vm-example applications using qemu? I followed the directions here (https://github.com/seL4/camkes-vm-examples) to get a build of the minimal application. I then tried to follow the directions here ( https://docs.sel4.systems/Hardware/Qemu/#running-qemu) to boot using qemu. Unfortunately I get an error when trying to boot. The error says: *"seL4 caled fail at /host/camkes_vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :("* *halting...* *Kernel entry via Interrupt, irq 0* I'm running this on a ubuntu 16.04 machine with an Intel i5-4200U ( https://ark.intel.com/products/75459/Intel-Core-i5-4200U-Processor-3M-Cache… ). Thanks!

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > > On 11.07.2018 01:45, Jeremy Fields wrote: > > Here's my results from these permutations, using Genode 18.05 / sel4 > 9.0.1 > > (hopefully the formatting works). I know some permutations probably don't > > make sense, but I did them anyways. Any thoughts? I have the serial > output > > from these tests as well, but didn't want to overload this message with > > that. Additionally, can you folks share specific machine make/models that > > you know work with Genode/seL4? Hopefully some 'consumer off the shelf' > > stuff. > > We have no specific Genode/seL4 x86 hardware list, but there exists an > unofficial list at [0] which may serve your question. > > > PermuationResult > > Legacy / Multiboot 2 + Bender Memory region overlap > > Legacy / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > Legacy / Multiboot 1 crashes/reboots > > Legacy / Multiboot 2 Memory region overlap > > UEFI / Multiboot 2 + Bender Memory region overlap > > UEFI / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > UEFI / Multiboot 1 freezes? > > UEFI / Multiboot 2 Memory region overlap > > Thanks for testing. > > May you please apply the seL4 kernel patch and test, whether this solves > your issue ? > > > [0] http://usr.sysret.de/jws/genode/hcl.html > > -- > 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 >

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > Hello, > > On 05.07.2018 14:34, Jeremy Fields wrote: > > Sure - I've tried a few different combinations, but the latest Genode 18.5 > > used seL4 9.0.1. I'm attempting to use this on an x86 machine that has a > > Xeon 1607 and a dedicated GPU. The thread I referenced in my initial post > > implied that UEFI might be an issue, but I've tried both UEFI and legacy > > boots without success. I tried using/building Genode 17.5 with whatever > > version of seL4 it acquires, but get the same error. Let me know if there's > > anything else I can provide > > some suggestions from my side. > > Try to remove the chain bootloader "bender", just to exclude it as > potential reason of trouble. In genode/tool/run/boot_dir/sel4 remove the > "multiboot2 /boot/bender ..." line and adjust the line below from > "module2 /boot/sel4 ..." -> "multiboot2 /boot/sel4 ...". Use some simple > scenario for testing, like log.run > > If the issue persists, you may try to boot Genode/seL4 the Multiboot 1 > way instead of Multiboot 2, which however will solely work for BIOS > legacy boots (no UEFI). Replace the "multiboot2" and "module2" in > genode/tool/run/boot_dir/sel4 with "multiboot" and "module". > > > Cheers, > > Alex B. > > -- > 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 > Here's my results from these permutations, using Genode 18.05 / sel4 9.0.1 (hopefully the formatting works). I know some permutations probably don't make sense, but I did them anyways. Any thoughts? I have the serial output from these tests as well, but didn't want to overload this message with that. Additionally, can you folks share specific machine make/models that you know work with Genode/seL4? Hopefully some 'consumer off the shelf' stuff. PermuationResult Legacy / Multiboot 2 + Bender Memory region overlap Legacy / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) Legacy / Multiboot 1 crashes/reboots Legacy / Multiboot 2 Memory region overlap UEFI / Multiboot 2 + Bender Memory region overlap UEFI / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) UEFI / Multiboot 1 freezes? UEFI / Multiboot 2 Memory region overlap -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 11 Jul '18

11 Jul '18

Sorry Thad, I want to correct something I said: I recommended that you try the arm-linux-gnueabihf toolchain, but that should have been the arm-linux-gnueabi toolchain. Aside from that, I went and double checked, and this toolchain works just fine -- one thing to note though, is that you don't have to specify the -DCROSS_COMPILER_PREFIX=foo option, and you should be able to just use -DAARCH32=1 and our build system should automatically select the right toolchain to invoke for you (see: https://github.com/seL4/seL4/blob/master/gcc.cmake#L24?) Feel free to ask more questions about the new build system since we expect adaptation to take some time. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

ninja build tool error
by 송대영 11 Jul '18

11 Jul '18

Hello, I have question about sel4's new ninja build tool. *1. From now on, sel4-tutorials use ninja build tool, so I repo new sel4-tutorials.Last step, I executue this command "../init-build.sh --plat pc99 --tut hello-1" but It prints with this error messages.What's the problem?---------------------------------------------------------------------------------------------CMake Warning at tools/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does notCall Stack (most recent call first): tools/cmake-tool/base.cmake:58 (include) tools/cmake-tool/all.cmake:16 (include) CMakeLists.txt:23 (include)CMake Error at projects/sel4-tutorials/CMakeLists.txt:34 (message): You must select a tutorial for compilation. Select using -DTUTORIAL=<PREFERENCE>. Choose one of hello-1;hello-2;hello-2-nolibs;hello-3;hello-3-nolibs;hello-4;hello-4-app;hello-timer;hello-timer-client.-- Configuring incomplete, errors occurred!See also "/home/scribnote5/sel4-tutorials-manifest/build_hello_1/CMakeFiles/CMakeOutput.log".2. How can I build sel4 ia32 images in sel4bench?This command "../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE" doesn't make sel4bench image file.*

2 1

sel4test cross compiling for arm
by Thad Seeberger 11 Jul '18

11 Jul '18

Good day. Trying to build first test and run on qemu. Cmake failing to compile the test program. Does this with different versions of cross compile. Can someone point me in the right direction of where to start looking. thx Thad localhost build-arm]# ../init-build.sh -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DPLATFORM=kzm -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /opt/arm/bin/arm-none-eabi-gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FAILED -- Performing test SOFTFP_FLOAT with flags -mfloat-abi=softfp -- Test SOFTFP_FLOAT FAILED CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring done -- Generating done -- Build files have been written to: /home/maddthad/seL4test/build-arm -- Performing test SOFT_FLOAT with flags -mfloat-abi=soft -- Test SOFT_FLOAT FAILED CMake Error at tools/seL4/cmake-tool/flags.cmake:135 (message): Kernel does not support hardware floating point but toolchain cannot build software floating point Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring incomplete, errors occurred! See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeOutput.log". See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeError.log". CMakeError.log: compiling the C compiler identification source file "CMakeCCompilerId.c" failed. Compiler: /opt/arm/bin/arm-none-eabi-gcc Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status Compiling the CXX compiler identification source file "CMakeCXXCompilerId.cpp" failed. Compiler: /opt/arm/bin/arm-none-eabi-g++ Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status

2 1

Future plans w.r.t. Cortex-R
by piotr＠skrzypek.eu 10 Jul '18

10 Jul '18

Dear seL4 Maintainers, Could you please share what are your future support plans w.r.t. ARM Cortex-R family - the 'reliable' and 'real-time' side of ARM portfolio? Cortex-R implementations include interesting safety features i.a. lockstep processing. It feels like a good match for seL4 safety-oriented philosophy. However, Cortex-R processors have MPU instead of MMU, which seems to be ruling them out for now. Are there any plans to have an seL4 'MPU' branch in order to support these kind of processors? Thank you in advance, Piotr Skrzypek

3 4

Questions on U-boot Verified Boot with CAmkES-ARM-VM
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

2 1

sel4 qemu x86 runtime error
by Thad Seeberger 10 Jul '18

10 Jul '18

Compile now no problem however I'm getting error when running. I believe its an invalid opcode exception. I think my build not matching the qemu but I've tried diff machines and they do the same. I also get this warning during build, not sure if this relevant: Warning: Installation path /home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not found on the PATH environment variable. make: Leaving directory `/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool' Qemu commanr, lines with ????? suspect: qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 (process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation vtable not supported Boot config: parsing cmdline 'images/kernel-ia32-pc99 ' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false ???? Warning: Your kernel was not compiled for the current microarchitecture. Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fefe000 type 1 Adding physical memory region 0x100000-0x1f800000 Physical Memory Region from 1fffe000 size 2000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e ACPI: RSDP paddr=0xf7180 ACPI: RSDP vaddr=0xdfcf7180 ACPI: RSDT paddr=0x1ffffbc1 ACPI: RSDT vaddr=0xdffffbc1 ACPI: FADT paddr=0x1ffff1c0 ACPI: FADT vaddr=0xdffff1c0 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffffb11 ACPI: MADT vaddr=0xdffffb11 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected Detected 1 IOAPICs, but configured to use PIC instead Detected 1 boot module(s): module #0: start=0x161000 end=0x25aed0 size=0xf9ed0 name='images/capdl-loader-experimental-image-ia32-pc99' ELF-loading userland images from boot modules: size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000 p_start=0x25b000 p_end=0x3e4000 Moving loaded userland images to final location: from=0x25b000 to=0x160000 size=0x189000 Starting node #0 with APIC ID 0 Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: ?????? user exception 0x6 code 0x0 in thread 0xff3f5d00 "rootserver" at address 0x805130e With stack: 0x80cfda0: 0x0 0x80cfda4: 0x0 0x80cfda8: 0x0 0x80cfdac: 0x0 0x80cfdb0: 0x0 0x80cfdb4: 0x0 0x80cfdb8: 0x0 0x80cfdbc: 0x0 0x80cfdc0: 0x0 0x80cfdc4: 0x0 0x80cfdc8: 0x0 0x80cfdcc: 0x0 0x80cfdd0: 0x0 0x80cfdd4: 0x0 0x80cfdd8: 0x0 0x80cfddc: 0x0 QEMU: Terminated Have a great day.

2 1

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong). Here is what I did so far: 1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev); --------------------------------------------------- vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){ //uint32_t data = fault_get_data(fault); uint32_t data = fault_get_ctx(fault)->r1; vchan_entry_point(vm, data); // fflush(stdout); advance_fault(fault); return 0; } struct device vchan_dev = { .devid = DEV_CUSTOM, .name = "vchan-driver", .pstart = 0x2040000, .size = 0x1000, .handle_page_fault = &vchan_device_fault_handler, .priv = NULL, }; --------------------------------------------------- 2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following: --------------------------------------------------- int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) { int res = 0; int err; unsigned phys_ptr = virt_to_phys(vmcall); vmcall->data = data; vmcall->cmd = cmd; vmcall->phys_data = virt_to_phys(data); vmcall->size = sz; down(&hyp_sem); /* Set up arguments for the ARM hyp call */ asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1"); asm volatile (".arch_extension virt\n\t” "hvc #0"); asm volatile ("mov %0, r0" : "=r" (res) : : ); err = vargs->err; up(&hyp_sem); return err; } --------------------------------------------------- The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information. --------------------------------------------------- # modprobe driver.ko [81.826621] driver: loading out-of-tree module taints kernel Bad sys call from [Linux]: scone 0 at PC: 0xbf000214 Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407) ————————————————————————— I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang

2 1

reading thread registers
by Michael Neises 10 Jul '18

10 Jul '18

Hello, I know there exists a function seL4_TCB_ReadRegisters, which can read the registers of a certain thread, given a/the capability to the thread. Ultimately, I'm interested in reading memory at runtime to determine whether the data I expect is present. So I'm wondering, is there in seL4 an init process, whose registers contain all the working memory of the system? And furthermore, how can I access a capability to a given thread in order to pass it into the ReadRegisters function mentioned above? Cheers, Michael

2 1

Memory Region overlap error
by Jeremy Fields 09 Jul '18

09 Jul '18

Hello- I'm trying to boot Genode/seL4 on hardware. I've tried a few different combinations of versions, and GRUB configurations, without success. I keep getting the same error despite these different combinations There was a thread that touched on this, but I couldn't find any resolution http://sel4.systems/pipermail/devel/2017-December/001776.html @##################################### Bender: Hello World. framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type Boot config: parsing cmdline 'sel4 disable_iommu' Boot config: console_port = 0x3f8 ▒Boot config: debug_port = 0x3f8 Boot config: disable_iommu = true module #0: start=0xf8f0000 end=0xffff228 size=0x70f228 name='image.elf' Physical Memory Region from 0 size 9ac00 type 1 Physical Memory Region from 9ac00 size 5400 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 18dbb000 type 1 Adding physical memory region 0x100000-0x18ebb000 Physical Memory Region from 18ebb000 size 12d000 type 4 Physical Memory Region from 18fe8000 size 1000 type 1 Adding physical memory region 0x18fe8000-0x18fe9000 Physical Memory Region from 18fe9000 size 17000 type 4 Physical Memory Region from 19000000 size 4ffd000 type 1 Adding physical memory region 0x19000000-0x1dffd000 Physical Memory Region from 1dffd000 size 3000 type 3 Physical Memory Region from 1e000000 size 8e784000 type 1 Adding physical memory region 0x1e000000-0x1f800000 Physical Memory Region from ac784000 size 94000 type 2 Physical Memory Region from ac818000 size fe8000 type 1 Physical Memory Region from b0000000 size 4000000 type 2 Physical Memory Region from fed20000 size 20000 type 2 Physical Memory Region from fed50000 size 40000 type 2 Physical Memory Region from ffa00000 size 40000 type 2 Physical Memory Region from 1000000000 size 350000000 type 1 Physical memory region not addressable Adding physical memory region 0x0-0x1f800000 seL4 failed assertion '!p_region_overlaps(reg)' at /home/critical/Downloads/genode-18.05/contrib/sel4-c59276cc6e3aa138a1e56af8c8a56ce64cf327b8/src/kernel/sel4/src/ arch/x86/kernel/boot.c:123 in function add_allocated_p_region halting... Kernel entry via Interrupt, irq 0 @##################################### Any thoughts? Anything I can try? Any information I can provide to help diagnose? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

3 3

We're hiring OS engineers
by Gernot.Heiser＠data61.csiro.au 06 Jul '18

06 Jul '18

Would you like to work on seL4 inside the TS team? Here’s your chance: https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-System-Engineer/488529400/ https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-Systems-Senior-Engineer/4… Gernot

1 0

Re: [seL4] IOMUX on iMX6 conflict with libethdrivers
by Kofidoku.Atuah＠data61.csiro.au 06 Jul '18

06 Jul '18

Hey Fabrizio?, I'm sorry we took so long to get back to you: The underlying problem here is that we haven't yet finished defining and implementing a driver framework for our userspace code, so in order to satisfy dependencies, we began stuffing them into the io_ops struct. So since lots of devices depend on an initialized mux driver, what you see here is the result of that, unfortunately -- the good news is that we're currently defining a driver framework internally (https://docs.sel4.systems/seL4DriverAPI/ChildEnumeration.html is one of the draft pages of documentation -- but none of this is finalized) over the course of this year. What I'd recommend is that you use the helper function, mux_sys_valid() in mux.h (https://github.com/seL4/util_libs/blob/master/libplatsupport/arch_include/a…) inside of the ethernet driver, and map the whole 16K range inside of the IO-Ops initializer -- essentially what's going on there is that there's a dependency on the mux driver that's satisfied by the IO-Ops object. Thanks very much for your patience,? and this sort of thing should be cleaned up soon. Yours truly, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 3

Re: [seL4] seL4 CNode and capability question
by 송대영 05 Jul '18

05 Jul '18

*I have a question about capability. 1. I know that CNode can consist of hierarchy of CNodes like 1-level, 2-level, 3-level.Can I create new CNode object like them? 2. If I can create hierarchy of CNode, I want to create hierarchy of CNode in order to retype new object to new CNode object.I tried it like below source code but it doesn't work with message "Untyped Retype: Invalid destination address".Would you give some advices?--------------------- source code // ** create CNode & mapping seL4_CPtr new_CNode_cap = info->empty.start + 5; error = untyped_retype_root(untyped, seL4_CapTableObject, seL4_SlotBits, cspace_cap, new_CNode_cap); ZF_LOGF_IFERR(error, "Failed to retype our chosen untyped into an CNode object.\n"); printf("================== seL4_DebugCapIdentify ======================\n"); printf("seL4_DebugCapIdentify seL4_CPtr CNode_cap : %u \n", seL4_DebugCapIdentify(new_CNode_cap)); // ** create new Endpoint object and mapping to new CNode seL4_CPtr new_CNode_cap_Endpoint; new_CNode_cap_Endpoint = info->empty.start + 6; error = seL4_Untyped_Retype(untyped /* untyped cap */, seL4_EndpointObject /* type */, seL4_SlotBits /* size */, new_CNode_cap /* root cnode cap */, new_CNode_cap_Endpoint /* destination cspace */, 32 /* depth */, new_CNode_cap_Endpoint /* offset */, 1 /* num objects */); if(error == 0) printf("error : %d \n", error);3. Can I check CNode level? It means like CNode level number.*

1 0

IPC
by tj5527 04 Jul '18

04 Jul '18

Searching on the sel4 repository, I find there is a manual talking about IPC (https://github.com/seL4/seL4/blob/9dba8e67ccb54e207bbec22e25f21c65e5c6a45f/…) In addition to this material, where - particularly source code - would be a good start point to look into IPC design and implementation? Thanks

2 1

IOMUX on iMX6 conflict with libethdrivers
by Fabrizio Bertocci 26 Jun '18

26 Jun '18

Hi, I need your help in trying to understand what is the best way to implement a permanent fix I can push on the seL4 repository regarding the incompatibility issues between the libethdriver and MUX interface of the platsupport. This apply to the iMX6 ethernet driver. I'm not sure about other platforms. In short, the problem is that platsupport takes ownership of the entire MUX (maps the I/O) when the io_ops are initialized: Repo: seL4/seL4_libs File: libsel4platsupport/src/io.c Function: sel4platsupport_new_io_ops ... mux_sys_init(io_ops, get_mux_dependencies(), &io_ops->mux_sys); ... The above call end up calling the platform-specific mux_sys_init that maps only the first 4Kb of IO space from address 0x020e0000 (the base address of the IOMUX controller - note: the IOMUX controller uses 16Kb of address space for its registers, not 4Kb!!!): Repo: seL4/util_libs File: libplatsupport/src/plat/imx6/mux.c Function: mux_sys_init ... MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); return imx6_mux_init_common(mux); The pointer "io_ops->mux_sys->priv" should point to the base address of the IOMUX of the SoC (in the virtual memory space of the calling process). The Ethernet driver unfortunately attempts to map the IOMUX again: Repo: seL4/util_libs File: libethdrivers/src/plat/imx6/uboot/mx6qsabrelite.c Function: setup_iomux_enet ... void *base = RESOURCE(&io_ops->io_mapper, IOMUXC); ... // Modify the IOMUX registers, then release the mapped IO: ... UNRESOURCE(&io_ops->io_mapper, IOMUXC, base); but using a larger size (the full 16Kb from the same base address of the IOMUX controller). So, the ethernet controller attempt to map the IO fails because it is already mapped, and nothing works. Right now in my project I've entirely commented out the initialization of the MUXC from the sel4platsupport_new_io_ops function. I understand that if the io_ops attempt to map the MUX (and leave it mapped) there must be a reason, unfortunately I fail to see it. The structure describing the MUXC register (struct imx6_iomuxc_regs, defined in libplatsupport/src/plat/imx6/mux.c) is private and not accessible outside that file, and the only two interface functions available (mux_feature_enable/mux_feature_disable) are not enough to be usable by the ethernet driver. The ethernet driver could also attempt to reuse the same mapped IOMUX (beside that the size of the mapped area is different and won't work anyway), but that will require using the 'priv' field of the io_ops->mux_sys (beside, even trying to map the whole 16Kb of the IOMUX and have the driver to reuse the same mapped address, for some unknown reasons it doesn't work). So, what is the right approach to fix this problem? Why the MUX subsystem maps some IO, never release it and keep it private for most of it? The IOMUX has been introduced somewhere between version 1.0 and 9.x... and it seems a half-baked job... Can we just comment it out if nobody is using it? Or if you have some ideas/suggestions on how to expand it in such a way the ethernet driver could use, please let me know. I'll be happy to implement it. Regards, Fabrizio

2 2

Problems with tk1 nonsecure
by Mike Clark 26 Jun '18

26 Jun '18

I just checked out a fresh copy of https://github.com/ SEL4PROJ/camkes-arm-vm-manifest and built an image for the TK1 using the docker build environment. I copied the resulting image to an SD card and it boots fine. If I switch to the unsecure mode, I get an error on boot. SMMU Address translation error: ID: 98 address: 0xae5be000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.204777] mmc1: ADMA error I have not made any changes, so my vm.smmu settings are all default. Any thoughts or help? Mike

3 9

Question about process and thread in tutorials
by 송대영 21 Jun '18

21 Jun '18

* I have question about process and thread in tutorials. 1. sel4 doesn't have process concept.But making new process is exist in tutorial hello-4.What is the exactly difference trhead in hello-2 and process in hello-4?2. In tutorials hello-4, where can I find access path that hello-4 process link hello-4-app?It means I think hello-4 process should designate hello-4-app's path.*

2 1

camkes and compcert
by Michael Neises 21 Jun '18

21 Jun '18

Hello, I understand that the proof for seL4 implies that the compiler and linker do not need to be trusted, because their output can be verified by a tool. Does this output-verification also apply to CAmkES C code for components and interfaces? Specifically, I'm working on a project where we want to have certain functionality implemented in C to be run on the seL4 microkernel. Would we gain any proof by using compcert, or is the output-verification sufficient? And is there any way to execute previously-compiled C binaries in a CAmkES component? I tried system calls, but I learned that won't work with the microkernel :-) I looked into the build architecture of the project, but I couldn't find where CAmkES components were being compiled. I looked into replacing gcc with compcert for the system, but there are used many flags available to gcc that are not available to compcert, so I scratched that idea. Thank you for your help. -Michael

2 1

Regarding porting SEL4 on RISCV hardware
by Sathya Narayanan N 15 Jun '18

15 Jun '18

Hi Members, I am trying to port SEL4 on RISCV hardware. I am stuck in finding the DTB/DTS files path in sel4test folder. Could someone guide me where these files exist and how to change the memory map for UART console. Actually, We changed the code for putchar in systems.c for Linux. So, I am trying to figure out, how to do something similar for SEL4. Please let me know, if someone has ported SEL$ to RISCV hardware. -- regards, Sathya

2 1

feL4: seL4 + Rust
by Jon Lamb 11 Jun '18

11 Jun '18

Hi all! We've been working on a way to write Rust programs for seL4, and would like to share it with you: https://github.com/PolySync/cargo-fel4.git With cargo-fel4, you can write a seL4 task in Rust, expose it through a prescribed entry point, and then build it along with the kernel. For now, it exposes only the system calls by way of Bindgen (a C-to-Rust bindings generator); however, we have plans to build up more idiomatic and Rusty abstractions in the near future. Cheers! Jon, Dan, Zack, and Nathan at PolySync

1 0

seL4_Wait crash if kernel is compiled with -O0 (qemu, pc99, gcc 4.8.2)
by Fabrizio Bertocci 25 May '18

25 May '18

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.

2 1

Tutorials broken?
by Fabrizio Bertocci 21 May '18

21 May '18

Hi all, I was going through the tutorials, unfortunately I've been finding very challenging to follow the instructions as I keep encountering issues after issue. First, the repo command seems to be incorrect. In document: https://docs.sel4.systems/Tutorials/ it says: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m sel4-tutorials.xml but the manifest file 'sel4-tutorials.xml' does not exist on the git repository (of the sel4-tutorial-manifest). What is the correct manifest file to use? There are two manifests (in any branch and tag): master.xml and default.xml. default.xml seems to use the 'new' format of identifying the individual versions of the libraries (through the hash). Let's assume the correct manifest to use is the 'default.xml' from the 'sel4-tutorials' branch and initialize the workspace with: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b sel4-tutorials repo sync So, now: first tutorial, ok (but this tutorial does very little). Second tutorial (hello-2), not so good... to avoid mistake, I am copying directly the solution into the app area: cp projects/sel4-tutorials/solutions/hello-2/src/main.c apps/hello-2/src/main.c make pc99_hello-2_defconfig make ... and the build fails with: [...]/workspaces/sel4-tutorials-2/stage/x86/pc99/lib/libsel4allocman.a(virtual_pool.o): In function `_add_page': [...]/workspaces/sel4-tutorials-2/libs/libsel4allocman/src/mspace/virtual_pool.c:52: undefined reference to `vspace_get_map_obj' The missing function appears to be part of libsel4vspace, that is missing from the library dependency list. Let's add it to add it to the apps/hello-2/Makefile: diff --git a/exercises/hello-2/Makefile b/exercises/hello-2/Makefile index 25c0b35..97a4fc6 100644 --- a/exercises/hello-2/Makefile +++ b/exercises/hello-2/Makefile @@ -28,6 +28,7 @@ ASMFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/plat/${PLA # Libraries required to build the target LIBS = c sel4 sel4muslcsys \ sel4simple sel4vka sel4allocman \ + sel4vspace \ sel4platsupport platsupport \ utils sel4simple-default sel4utils sel4debug Now it builds successfully, unfortunately when running, the child thread doesn't appear to run at all. This is the output of qemu running 'make simulate': Booting all finished, dropped to user space 4 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world I would have expected seeing on the output the string 'thread_2: hallo wereld' somewhere... Why the thread 2 does not run? This code was working last time I checked (version 5.2). I tried then to continue testing the tutorials, and I went to the hello-3. Hello-3 is based on the Hello-2 but adds an endpoint for IPC between the main thread and the child thread. Surprisingly, this app not only builds out of the box without errors (apparently libsel4vspace was already added to its Makefile), but even running it, works as expected: Booting all finished, dropped to user space 3 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world thread_2: hallo wereld thread_2: got a message 0x6161 from 0x61 main: got a reply: 0xffff9e9e Right now I suspect that seL4_TCB_Configure() does not work correctly if we don't provide an endpoint (because that's essentially the main difference between the two tests). Can somebody try to run the tutorials and perhaps confirm the problem? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

1 0

docker build error
by Paolo Crisafulli 18 May '18

18 May '18

Hi all, I'm using the docker build environment provided by https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles Currently, "make sel4" fails with this message: E: Package 'ncurses-dev' has no installation candidate Anyone experimenting the same behaviour? Cheers, Paolo

2 2

Help with Isabelle/AutoCorres
by Burkhart Wolff 18 May '18

18 May '18

Dear all, I stumbled into some problems with AutoCorres and would be grateful if someone could help me. I used the recent version autocorres1.4 under Isabelle2017. A) Running under MacOS, cpp is apparently not running inside install_C_file (yes, I installed the cpp wrapper: >>>>>>>>>>>>>>>>>>>>>> !/bin/bash # Wrapper for clang C preprocessor on MacOS export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre" llvm-gcc -Wno-invalid-pp-token -E -x c $@ <<<<<<<<<<<<<<<<<<<<<< and made sure that it is in the path of the shell in which I started Isabelle.) Does anyone know a cause for this behaviour or a feasible workaround ? (besides doing the expansions by hand) Is there an explicit Isabelle shell variable where the path to cpp must be set ? B) I get a weird crash of AutoCorres without a clue what might cause it: I have a T4.h file with >>>>>>>>>>>>>>>>>>>>>>> #define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn #define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed extern const char *InputField[]; enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 }; enum Status { FAIL, SUCCESS }; enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 }; struct OBits { int C1 ; int C2 ; int C3 ; } Obits; /********* Output data *****************/ extern enum Status O_Position_Valid; extern unsigned int O_Position_Count; extern unsigned int Relative_Position; extern int Instantaneous_Speed; extern int Mean_Speed; <<<<<<<<<<<<<<<<<<<<<<<<<<<<< and a T4.c file with: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> #include "T4_AlgoODO.h" enum Status O_P_V = SUCCESS; unsigned int O_P_C = 0; unsigned int Relative_Position = 0; int I_Speed = 0; int Mean_Speed = 0; int Acceleration = 0; int scale = 1000; int PI_approx = 3141; struct OBits Input; enum State OState; const unsigned int Radius = 500; const unsigned int Sampling_Rate = 400; unsigned int F_O_P_C = 0; int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/]; int FIFO_pointer = 0; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< Loading this in Isabelle/AutoCorres with: >>>>>>>>>>>>>>>>>>>>>>>>> install_C_file "code/c/T4.c” <<<<<<<<<<<<<<<<<<<<<<<<< results in the following AutoCorres crash: … exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array! Can anybody tell me what this means and propose a workaround ? Best regards B. Wolff

2 1

Untyped Retype destination not empty?
by Richard Clark 18 May '18

18 May '18

Hi! I could use a clue as to the cause of this problem. The program has its free slots start index set correctly. It is trying to allocate a dma buffer. (4k with a known physical address). The vspace has been properly set up and knows the phys addresses of its free memory. This used to work fine in a different process, but I can't find anything I've done different/wrong in this one... I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c). /* Ensure that the destination slots are all empty. */ slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)); slots.offset = nodeOffset; slots.length = nodeWindow; for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) { status = ensureEmptySlot(slots.cnode + i); if (status != EXCEPTION_NONE) { userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode); userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow); int j = 0; for(j=0;j<2048;j++){ status = ensureEmptySlot(slots.cnode + (i + j)); if (status == EXCEPTION_NONE) { userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode); status = EXCEPTION_SYSCALL_ERROR; break; } } return status; } } And finally, here is the output from the console: <<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>> <<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>> _refill_pool@split.c:187 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12 I need a hint... help? Thanks! Richard ________________________________ 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.

2 1

Automatic testing using qemu
by Paolo Crisafulli 17 May '18

17 May '18

Hi there, I have written a seL4 app using CAmkES, that I am continuously building using Jenkins. I'd like to add a test step to this continuous integration process, launching the app with qemu and parsing the output to validate my expectations. The thing is, although all the active ("control") components reach their last instruction after a while, seL4 does not "exit" (which is expected I guess) and qemu does not stop, keeping my continuous integration job running for ever. Any idea on how to achieve this? Thank you very much in advance. Cheers, Paolo Crisafulli

3 5

Booting seL4, MMU configuration on armv7a-ve
by Jonas Persson 30 Apr '18

30 Apr '18

Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas

1 0

Announcing seL4 9.0.1: with RISC-V support
by Kent.Mcleod＠data61.csiro.au 25 Apr '18

25 Apr '18

We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: <https://docs.sel4.systems/Hardware/RISCV> See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.1> <https://docs.sel4.systems/camkes_release/CAmkES_3.4.0> # seL4 Version 9.0.1 Release Announcing the release of `seL4 9.0.1` with the following changes: 9.0.1 2018-04-18: BINARY COMPATIBLE ## Changes * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs which use any of the following functions may break, if the program relies on these functions to mask the `label` field to the previous width of 20 bits. - `seL4_MessageInfo_new` - `seL4_MessageInfo_get_label` - `seL4_MessageInfo_set_label` * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or or multicore support on the Spike simulation platform. There is *no verification* for this platform. ## Upgrade Notes --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 9.0.0..9.0.1` # More details See the [9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release ---- # CAmkES Version camkes-3.4.0 Release Announcing the release of `` with the following changes: camkes-3.4.0 2018-04-18 Using seL4 version 9.0.1 ## Changes ## Upgrade Notes --- # Full changelog Use `git log camkes-3.3.0..camkes-3.4.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/i… or ask on the mailing list!

7 10

Further use of Device Tree?
by Jeff Waugh 23 Apr '18

23 Apr '18

Hello, Congrats on the RISC-V release! I noticed some Device Tree code snuck in, replacing some hard coded bits in the platform, and is intended to be exposed to the rootserver… Any interest or intention to bring that to the ARM code, and possibly avoid building kernels for specific platforms? Thanks, Jeff

2 1

UART1 getchar
by Wei Xiang Leow 19 Apr '18

19 Apr '18

Hello all, I'm new to seL4 and embedded systems, please bear with me. I'm trying to use Sabrelite's UART1 (PS_SERIAL0), while I can make it write data (putchar), I can't make it read (getchar). The code is as follows on sel4 7.0.0, using platsupport/sel4platsupport: ps_io_ops_t io_ops; error = sel4platsupport_new_io_ops(vspace, vka, &io_ops); printf("Initialising io_ops: %d\n",error); ps_chardevice_t serial0; ps_cdev_init(PS_SERIAL0,&io_ops,&serial0) ps_chardevice_t serial1; ps_cdev_init(PS_SERIAL1,&io_ops,&serial1); //CONSOLE int character; while (1) { character = ps_cdev_getchar(&serial0); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial1,character); printf("%d\n",character); } } This runs fine on QEMU with -serial file/ttyUSB -serial mon:stdio. Next I tried to run this on the Sabrelite board: -Clone the 08-09 uboot from git, according to https://sel4.systems/Info/ Hardware/sabreLite/ -Apply patches 1 and 2 (applying 3 and 4 caused uboot to stall) -Put uboot into SPI flash -Restart, run the sel4 image on the SD card, with UART2 connected to PC's RS232 and displayed by minicom, and UART1 connected to /dev/ttyUSB0 -Have a python script writing 'A's to /dev/ttyUSB0 sel4 loads but fails to read anything from /dev/ttyUSB0, UART1 just receives EOFs (-1s). The rxd seems to always be 0. Swapping the UARTs works, at the cost of losing the console: while (1) { character = ps_cdev_getchar(&serial1); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial0,character); printf("%d\n",character); } } So UART2 (default console) can read and write, while UART1 can write but not read. Has anyone encountered the same problem? Suggestions much appreciated. Regards, Leow Wei Xiang

1 0

Camkes manifest now requires cmake 3.7.2 or higher to be built
by Amit Goyal 12 Apr '18

12 Apr '18

I was running the following commands to build camkes: 1. repo init -u https://github.ls com/sel4/camkes-manifest.git 2. repo sync 3. make clean 4. make ia32_simple_defconfig; make silentoldconfig 5. make -j4 6. qemu-system-i386 -nographic -m 512 -cpu Haswell -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Earlier it used to work perfectly fine but now it requires cmake 3.7.2 or higher which can be obviously be done by using pip install. I just wanted to convey this so that the same may be updated on prerequisites page. (https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md) -- Thanks and Regards, Amit Goyal

1 0

Unable to Run seL4test
by Amit Goyal 12 Apr '18

12 Apr '18

Hi Kofi, I am getting the attached error (Error Log.txt) while running seL4test. Earlier it used to run perfectly fine. I am running the following commands: $ repo init -u https://github.com/seL4/sel4test-manifest.git $ repo sync $ make clean $ make ia32_simulation_release_xml_defconfig $ make -j libmuslc && make $ make simulate-ia32 Can you please look into this. -- Thanks and Regards, Amit Goyal

2 2

New documentation website: https://docs.sel4.systems
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

We are pleased to annouce a new documentation website at <https://docs.sel4.systems>! The documentation site is now using GitHub pages, generated from a GitHub repository <https://github.com/SEL4PROJ/docs> using a popular static site generator, Jekyll. GitHub pages hosted documentation is a standard documentation pattern familiar to many in the open-source community. Content from the previous wiki has been migrated to the new site, while the wiki itself is no longer available. The new documentation format should welcome community contributions, and be easier to maintain for the following reasons: * Contributions are welcome via pull request. * Easier editing through Markdown (GFM), an open document format. * Content styling is now separate from presentation. * The site can be checked out and hosted locally. * Contributions are versioned and reviewed, and tagged at released versions of seL4. We hope that this will lead to the quality of our documentation increasing as it is easier and more accessible to update. Contributions, via pull requests or feature requests on github, are welcome. Kent

1 0

seL4 9.0.0 and CAmkES camkes-3.3.0 release
by Kent.Mcleod＠data61.csiro.au 12 Apr '18

12 Apr '18

See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.0> <https://docs.sel4.systems/camkes_release/CAmkES_3.3.0> # seL4 Version 9.0.0 Release Announcing the release of `seL4 9.0.0` with the following changes: 9.0.0 2018-04-11: BREAKING # Changes * Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to dangerous code injection) * Mitigation for Meltdown (https://meltdownattack.com) on x86-64 implemented. Mitigation is via a form of kernel page table isolation through the use of a Static Kernel Image with Microstate (SKIM) window that is used for trapping to and from the kernel address space. This can be enabled/disabled through the build configuration depending on whether you are running on vulnerable hardware or not. * Mitigation for Spectre (https://spectreattack.com) on x86 against the kernel implemented. Default is software mitigation and is the best performing so users need to do nothing. This does *not* prevent user processes from exploiting each other. * x86 configuration option for performing branch prediction barrier on context switch to prevent Spectre style attacks between user processes using the indirect branch predictor * x86 configuration option for flushing the RSB on context switch to prevent Spectre style attacks between user processes using the RSB * Define extended bootinfo header for the x86 TSC frequency * x86 TSC frequency exported in extended bootinfo header * `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which can now be retrieved through the extended bootinfo * Invocations to set thread priority and maximum control priority (MCP) have changed. - For both invocations, users must now provide a TCB capability `auth` - The requested MCP/priority is checked against the MCP of the `auth` capability. - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy problem. * `seL4_TCB_Configure` no longer takes prio, mcp as an argument. Instead these fields must be set separately with `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority`. * `seL4_TCB_SetPriority` and `seL4_TCB_SetMCPriority` now take `seL4_Word` instead of `seL4_Uint8`. - `seL4_MaxPrio` remains at 255. * `seL4_TCB_SetSchedParams` is a new method where MCP and priority can be set in the same sytsem call. * Size of the TCB object is increased for some build configurations # Upgrade notes * `seL4_TCB_Configure` calls that set priority should be changed to explicitly call `seL4_TCB_SetSchedParams` or `SetPriority` * `seL4_TCB_Configure` calls that set MCP should be changed to explicitly call `seL4_TCB_SetSchedParams` or `seL4_TCB_SetMCPriority` --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 8.0.0..9.0.0` # More details See the [9.0.0 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.0.pdf) included in the release or ask on the mailing list! ---- # CAmkES Version camkes-3.3.0 Release Announcing the release of `camkes-3.3.0` with the following changes: camkes-3.3.0 2018-04-11 Using seL4 version 9.0.0 ## Changes * Hardware dataport with large frame sizes issue has been fixed * Bug fix: Enumerating connections for hierarchical components with custom connection types is now done correctly * Bug fix: Data structure caching is now correctly invalidated between builds * Initial CMake implementation for CAmkES. See the CAmkES test apps for examples. ## Upgrade notes * No special upgrade requirements. ## Known issues * Hierarchical components that export dataport connectors create compilation errors as the templates cannot accurately tell that the connector of the parent component is exported from the child and no code should be generated. A temporary workaround involves making the dataport connection explicitly available to the parent component. --- # Full changelog Use `git log camkes-3.2.0..camkes-3.3.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.3.0/docs/i… or ask on the mailing list!

1 0

camkes tutorial build compilation error
by Thad Seeberger 03 Apr '18

03 Apr '18

Good day, I am working thru the examples. make arm_hello-camkes-0_defconfig; make -- compiles and run on qemu The I tried x86 architecture make ia32_hello-camkes-0_defconfig; make -- build error I cant find declarations for any of the listed errors. I'm guessing these should be dynamically defined before the build based on the architecture. Please let me know what I'm doing wrong. thx [CC] kernel_final.s /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c: In function ‘decodeIA32PageDirectoryInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: error: ‘X86PageDirectoryGetStatusBits’ undeclared (first use in this function); did you mean ‘performIA32PageDirectoryGetStatusBits’? case X86PageDirectoryGetStatusBits: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ performIA32PageDirectoryGetStatusBits /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: note: each undeclared identifier is reported only once for each function it appears in /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86FrameInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:854:10: error: ‘X86PageMap’ undeclared (first use in this function); did you mean ‘ARMPageMap’? case X86PageMap: { /* Map */ ^~~~~~~~~~ ARMPageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1012:10: error: ‘X86PageRemap’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageRemap: { /* Remap */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1143:10: error: ‘X86PageUnmap’ undeclared (first use in this function); did you mean ‘X86PageRemap’? case X86PageUnmap: { /* Unmap */ ^~~~~~~~~~~~ X86PageRemap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1166:10: error: ‘X86PageMapIO’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageMapIO: { /* MapIO */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1175:10: error: ‘X86PageGetAddress’ undeclared (first use in this function); did you mean ‘ARMPageGetAddress’? case X86PageGetAddress: { ^~~~~~~~~~~~~~~~~ ARMPageGetAddress /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86PageTableInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1236:21: error: ‘X86PageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86PageTableUnmap) { ^~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1246:21: error: ‘X86PageTableMap’ undeclared (first use in this function); did you mean ‘X86PageTableUnmap’? if (invLabel != X86PageTableMap ) { ^~~~~~~~~~~~~~~ X86PageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86MMUInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1365:25: error: ‘X86ASIDControlMakePool’ undeclared (first use in this function); did you mean ‘ARMASIDControlMakePool’? if (invLabel != X86ASIDControlMakePool) { ^~~~~~~~~~~~~~~~~~~~~~ ARMASIDControlMakePool /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1434:25: error: ‘X86ASIDPoolAssign’ undeclared (first use in this function); did you mean ‘ARMASIDPoolAssign’? if (invLabel != X86ASIDPoolAssign) { ^~~~~~~~~~~~~~~~~ ARMASIDPoolAssign /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c: In function ‘Arch_decodeIRQControlInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:122:10: error: ‘X86IRQIssueIRQHandlerIOAPIC’ undeclared (first use in this function); did you mean ‘invokeIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerIOAPIC: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~ invokeIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:144:10: error: ‘X86IRQIssueIRQHandlerMSI’ undeclared (first use in this function); did you mean ‘X86IRQIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerMSI: { ^~~~~~~~~~~~~~~~~~~~~~~~ X86IRQIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c: In function ‘decodeX86PortInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:21: error: ‘X86IOPortOut8’ undeclared (first use in this function) if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~ /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:50: error: ‘X86IOPortOut16’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:80: error: ‘X86IOPortOut32’ undeclared (first use in this function); did you mean ‘X86IOPortOut16’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:75:10: error: ‘X86IOPortIn8’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? case X86IOPortIn8: { /* inport 8 bits */ ^~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:89:10: error: ‘X86IOPortIn16’ undeclared (first use in this function); did you mean ‘X86IOPortIn8’? case X86IOPortIn16: { /* inport 16 bits */ ^~~~~~~~~~~~~ X86IOPortIn8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:103:10: error: ‘X86IOPortIn32’ undeclared (first use in this function); did you mean ‘X86IOPortIn16’? case X86IOPortIn32: { /* inport 32 bits */ ^~~~~~~~~~~~~ X86IOPortIn16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c: In function ‘decodeX86IOPTInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:195:21: error: ‘X86IOPageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86IOPageTableUnmap) { ^~~~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:201:21: error: ‘X86IOPageTableMap’ undeclared (first use in this function); did you mean ‘X86IOPageTableUnmap’? if (invLabel != X86IOPageTableMap ) { ^~~~~~~~~~~~~~~~~ X86IOPageTableUnmap make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2

2 1

Status of cmake support?
by Bruce Mitchener 30 Mar '18

30 Mar '18

Hello! I've been looking at doing some builds with cmake and ninja experimentally again. Is anyone else doing this? I noticed that some bugs are being filed about warnings from clang, but I was only able to get some of the cmake + ninja stuff working when I used gcc. How are people using clang? So far, I haven't gotten a working build with cmake of sel4-tests. Is there a good way to trouble shoot this or should I post more detailed info in a thread on this list? Thanks, - Bruce

2 1

Haskell and language support
by jonas.cl＠protonmail.com 27 Mar '18

27 Mar '18

Hi, Does anyone know when the Haskell support will be released in public? In the Language support section of https://wiki.sel4.systems/Suggested%20projects is says that it will be released in the near future, but the page was last edited on June 2016. I propose that the language section also contains links to where the source can be found. I am also writing since I am working on porting the sel4-tutorial to Idris, which could be added to the list of languages, with a link to https://github.com/mokshasoft/sel4-idris-manifest There is a long way to go before it is finished, but if people want to help I accept patches. /Jonas Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.

2 3

OPENSSL for seL4
by Daniel Wang 27 Mar '18

27 Mar '18

Hi all, Anyone has openssl working for seL4? I compiled a version of openssl it links correctly but as soon as the code calls BIO_new_mem_buf() the system crashed with: FAULT HANDLER: data fault from vm.control (ID 0x03) on address 0xffffffb4 ,pc = 0xe259c, fsr = 0x3800006 If openssl is not available for now I wonder has anyone used other crypto library before, such as wolfssl, bearssl, etc.? Best Regards -Daniel Wang

1 0

Booting BIN abort after elfloader
by Daniel Wang 26 Mar '18

26 Mar '18

Hi all, With help from Dr. Chubb, I found there is a config to build CAmkES-ARM-VM as binary instead of ELF. However when I boot it on TK1 the process abort after loader code as follow. It is the same result when I convert ELF to BIN. Do you have any suggestion why this is happening (the paddrs and virt_entry are correct). Thank you very much! Tegra124 (TK1-SOM) # ext2load mmc 0 0x90000000 capdl-loader-experimental-image-arm-tk1-bin 31897292 bytes read in 884 ms (34.4 MiB/s) Tegra124 (TK1-SOM) # go 0x90000000 ## Starting application at 0x90000000 ... Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001d3 ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..91e7ffff] ELF-loading image 'kernel' paddr=[80000000..8003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[8003d000..81f3efff] vaddr=[10000..1f11fff] virt_entry=184f8 Enabling MMU and paging Jumping to kernel-image entry point... abort() called. Best Regards -Daniel Wang

1 0