March 2018 - Devel - lists.sel4.systems

Unable to Compile Tutorial 2 Exercises
by Amit Goyal 20 Mar '18

20 Mar '18

Hi, I am new to sel4 and was thus practising the tutorials given at: https://wiki.sel4.systems/Tutorials While compiling tutorial 2 exercises, I got the attached error (I have also attached the main.c file). Can someone please help me in resolving it. -- Thanks and Regards, Amit Goyal

2 1

Ethernet driver for TK-1
by Michal Podhradsky 20 Mar '18

20 Mar '18

Hello, I would like to use a similar Ethernet driver component as for x86 platforms here: https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver But in the camkes-vm-arm repository I don't see an equivalent component: https://github.com/SEL4PROJ/camkes-arm-vm/tree/master/apps/vm/components Is the ethernet currently just passed to Linux? And if so, what would entail making a new driver etc similar to x86 platforms? Regards Michal

2 1

VM and VMM Communication for ARM
by Daniel Wang 17 Mar '18

17 Mar '18

Hi all, I have a couple questions about VM an VMM communication for CAMKES-ARM-VM. Please correct me if I’m wrong. I found when VMM load Linux device it installs a vgic (install_linux_devices() -> vm_install_vgic()) But how exactly a interrupt caused by VM is distributed from GIC to VGIC (kernel to VMM)? I saw that we can register a virq to the VGIC (vm_virq_new()), but I’m not sure when a interrupt is generated how it is passed to the VGIC. Second, I found that we can install virtual devices to VM (e.g. for Vchan communication). Seems like when Linux tries to access the mapped virtual device, a page_fault will generated. Does it create a interrupt? How does it processed by VMM code exactly? I found post_main() in the generated camkes.c file has 3 threads, case 3 runs the control thread -> run(), case 5 runs vevent interface vevent__run(), and case 7 runs fault hander. Does it triggers vevent? I’m not sure the control flow. Thank you in advance! Best Regards -Daniel Wang

1 0

irq_server example? Interrupt handlers?
by Richard Clark 14 Mar '18

14 Mar '18

Hi all! I have an Ethernet driver underneath an lwip implementation that I've gotten to run threaded tcpip. It happily passes messages back and forth and all around between half a dozen threads over a dozen ports all on localhost. Every once in a while though, it wants to send a packet to the outside world... this of course invokes the Ethernet driver, which rather annoyingly, is polled. I am looking for the proper way to convert my polled Ethernet driver to be interrupt-driven.... however the sel4 interrupt-handling/dispatching seems to escape my grasp and I could use a little help... It would appear that there is a mechanism to register a request to receive a message whenever an interrupt occurs? irq_server.c? Are there some nice simple examples out there? Is there an easier way perhaps? Thanks! Richard H. Clark ________________________________ 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

Questions about Vchan
by Daniel Wang 14 Mar '18

14 Mar '18

Hi all, I’m trying to figure out how to use the Vchan library to setup communication between guest OS and native components. I got couple questions how you can give me some advices. 1. I saw the camkes_vchan_con_t structure in the helloworld components (camkes-arm-vm), but I could not find the implementation for vchan_con_new_connection(), vchan_con_rem_connection(), etc. Are those autogenerated by camkes? If so how it is generated? static camkes_vchan_con_t con = { .connect = &vchan_con_new_connection, .disconnect = &vchan_con_rem_connection, .get_buf = &vchan_con_get_buf, .status = &vchan_con_status, .alert = &vchan_con_ping, .wait = &vevent_wait, .poll = &vevent_poll, .dest_dom_number = 0, .source_dom_number = 50, }; 2. I tried to compile the Vchan support and demo helloworld components for odroid-xu. But the compile shows error due to the VM.h file (camkes-arm-vm/projects/vm/components/VM/src/cmks_vchan_vm.c:23) cannot be found. How can I generate the VM.h file? Thanks a lot! Best Regards -Daniel Wang

4 5

seL4 developer review of RISC-V privileged ISA spec?
by Kelly Dean 14 Mar '18

14 Mar '18

The RISC-V privileged ISA is not yet finalized. Have the seL4 developers reviewed the draft [1], in case they might have any recommendations for improvement? For example, just last year a blunder (H-mode) was removed from the draft per a proposal [2] on the mailing list. Finalization is planned for this year. Speak now or forever hold your peace. The first public draft of the memory consistency model [3] was also released just last December. And platform standardization, especially the IOMMU, is in progress. [1] https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10… [2] https://groups.google.com/a/groups.riscv.org/forum/#!msg/isa-dev/SfEDPLU0NU… [3] https://groups.google.com/a/groups.riscv.org/forum/#!topic/isa-dev/hKywNHBk…

6 5

Questions about Allocman
by Daniel Wang 12 Mar '18

12 Mar '18

Hi all, I’m trying to understand the code a little bit more. This is kind of a random question. I’m wondering that in a case where we call to allocate a frame using allocman library, where is the physical address of a certain region is stored? In allocman_t there are multiple fields: size_t num_utspace_chunks; struct allocman_utspace_chunk *utspace_chunk; size_t *utspace_chunk_count; struct allocman_utspace_allocation **utspace_chunks; struct allocman_utspace_chunk { size_t size_bits; seL4_Word type; size_t count; }; struct allocman_utspace_allocation { seL4_Word cookie; cspacepath_t slot; }; I didn’t find struct that hold the paddr, also after we create a frame where is that paddr stored? It is stored in slot.capPtr? Also What does the field cookie for? Best Regards -Daniel Wang

3 3

Share UART with Guest Linux
by Daniel Wang 10 Mar '18

10 Mar '18

Hi all, For experiment, I created a simple app along with the vmm using CamKES-ARM-VM repository. Currently the simple app only prints strings periodically using printf(). However as soon as the guest Linux starting running. I cannot print anything and also receives error as following: I assumes it is due to the iommu capability got assigned to Linux by VMM. Is there a way to allow native app also prints information on the screen using printf()? ------------------ libsel4muslcsys: Error attempting syscall 162 FAULT HANDLER: data fault from hello.control (ID 0x1) on address 0xffffff80, pc = 0x135ac, fsr = 0x3840046 FAULT HANDLER: pc = 0x135ac FAULT HANDLER: sp = 0x142d20 FAULT HANDLER: lr = 0x135ac FAULT HANDLER: r0 = 0xffffff80 FAULT HANDLER: r1 = 0 FAULT HANDLER: r2 = 0 FAULT HANDLER: r3 = 0 FAULT HANDLER: r4 = 0x26 FAULT HANDLER: r5 = 0 FAULT HANDLER: r6 = 0 FAULT HANDLER: r7 = 0xfffffff2 FAULT HANDLER: r8 = 0x1 FAULT HANDLER: r9 = 0 FAULT HANDLER: r10 = 0 FAULT HANDLER: r12 = 0x142caa FAULT HANDLER: r14 = 0x135ac FAULT HANDLER: cpsr = 0x20000050 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x00143fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00143000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0013f000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0013e000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00137fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00137000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x00136000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00135000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00131fff -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x00010000 -- CPIO: 2 files found. 0) linux 0x00059c70, 16302080 bytes 1) linux-dtb 0x00fe5ce8, 29415 bytes Best Regards -Daniel Wang

1 1

Compilation Error with version
by Thad Seeberger 08 Mar '18

08 Mar '18

Good day. I am getting hung up compiling the CAmkES compiles. I'm getting following error which I believe is because the version.h.d does not exist. Where is the version set? thx [camkes-accelerator] building... -- Configuring done -- Generating done -- Build files have been written to: /home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator ninja: error: '/home/xxxx/seL4_camkes_x86_64/tools/camkes/tools/accelerator/DEPFILE', needed by '.', missing and no known rule to make it make: *** [/home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator/camkes-accelerator] Error 1 ive traced it down I think to this block in the Cmakeadd_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR} OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/include/version.h OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/version.h.d # Build a valid dependency file from the print-deps script, this is a little awkward COMMAND echo "include/version.h: " > "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/print-deps.py" >> "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND sed -i "s/$$/\\/" "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/mkversion.py" >"${CMAKE_CURRENT_BINARY_DIR}/include/version.h" DEPENDS mkversion.py DEPENDS print-deps.py DEPFILE ${CMAKE_CURRENT_BINARY_DIR}/version.h.d )

4 8

CapDL spec for Camkes-ARM-VM
by Daniel Wang 08 Mar '18

08 Mar '18

Hi all, I’m trying build a PoC system based on the camkes-arm-vm repository. I saw the init process is created using CapDL, but I’m having trouble to find the the CapDL spec file. Could you please point it out for me? Also for the first step, I’m trying to build another app side-by-side with the VMM and guest Linux. I assume I need to modify the CapDL. I’m not exactly the work flow with CapDL can you give me a hint? Thanks. Best Regards -Daniel Wang

2 2