December 2018 - Devel - lists.sel4.systems

Camkes Cross-VM Communication
by Amit Goyal 14 Dec '18

14 Dec '18

Hi All, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running Camkes Cross-VM communication tutorial available at: https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html I am able to build the system properly but when I run the system, I get the following error: --------------------------------------------------------------------------------------------------------------------------------- Creating dataport node /dev/camkes_reverse_src Creating dataport node /dev/camkes_reverse_dest Allocating 8192 bytes for /dev/camkes_reverse_src dataport_map_guest@cross_vm_dataport.c:25 Dataport guest size and host size are different (8192 and 4096) dataport_vmcall_handler@cross_vm_dataport.c:75 Failed to map dataport into guest VM_FATAL_ERROR ::: vmexit handler return error vmm_print_guest_context:27 | ================== GUEST OS CONTEXT ================= vmm_print_guest_context:30 | exit info : reason 0x12 qualification 0x0 instruction len 0x3 interrupt info 0x0 interrupt error 0x0 vmm_print_guest_context:32 | guest physical 0x0 rflags 0x286 vmm_print_guest_context:34 | guest interruptibility 0x0 control entry 0x34 vmm_print_guest_context:37 | eip 0xd881714a vmm_print_guest_context:39 | eax 0x 1 ebx 0x 1 ecx 0x 1 vmm_print_guest_context:41 | edx 0x16a42000 esi 0x 2000 edi 0x 10 vmm_print_guest_context:43 | ebp 0xd6b17f0c vmm_print_guest_context:45 | cr0 0x80050033 cr3 0x16b1e000 cr4 0x2680 --------------------------------------------------------------------------------------------------------------------------------- I tried troubleshooting it a bit and changed the file: ~/camkes_vm_com/projects/vm-linux/camkes-linux-artifacts/camkes-linux-init-scripts/buildroot_init/camkes_init as follows: Earlier: dataport_init /dev/camkes_reverse_src 8192 /dev/camkes_reverse_dest 8192 Changed: dataport_init /dev/camkes_reverse_src 4096 /dev/camkes_reverse_dest 4096 But this also does not work. Please suggest. -- Thanks and Regards, Amit Goyal

2 2

Patent on formal verification
by Tom Mitchell 11 Dec '18

11 Dec '18

Patents possibly gone wrong. https://www.eff.org/deeplinks/2018/11/stupid-patent-month-patent-using-math… Claim 1 of the patent describes creating mathematical “axioms”—formal mathematical statements—that describe a computerized trading forum. The patented method then describes analyzing, with a “computer assessment system … the mathematical axioms that describe the operation of the trading forum.” In other words, the patent describes using formal proofs to check for bugs in a “computerized trading forum.” It’s formal verification—just applied to the financial services industry. -- T o m M i t c h e l l

1 0

Network lwip for imx6
by wong xuguo 11 Dec '18

11 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

sel4 on Raspberry Pi 3b Not Working
by Amit Goyal 06 Dec '18

06 Dec '18

Hi All, I tried running seL4 on Raspberry Pi 3b using the following links: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I get the following: CACHE: Misaligned operation at range [20000000, 20000014] CACHE: Misaligned operation at range [20008c80, 200092ef] CACHE: Misaligned operation at range [200192f0, 203bb4f0] CACHE: Misaligned operation at range [203bc000, 203c6030] CACHE: Misaligned operation at range [203c6030, 203c8000] ## Starting application at 0x20000000 … and then nothing works and the processor halts. I have tried the pre-built uboot binary, complied uboot versions v2017.1 and v2016.11 as suggested by steve sloloski (on the blog) and uboot version v2016.05 (out of curiosity) but nothing works. Can someone please suggest a possible way out. -- Thanks and Regards, Amit Goyal

2 4

[sel4] Building seL4test for x86_64 on Debian
by Dave Richards 06 Dec '18

06 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on a Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

1 0

Building seL4x86_64 on Debian
by Dave Richards 05 Dec '18

05 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

3 2

seL4 cache pinning
by 송대영 02 Dec '18

02 Dec '18

Hi, I read "Improving Interrupt Response Time in a Verifiable Protected Microkernel" paper. This paper improved IPC performance by using cache pinning and I want to know how to implement cache pinnng. But this paper doesn't refer how to manipulate cache lines. Would you give me some methods how to read cache lines and write cache lines?

3 2

Is the ASID used in seL4 by default?
by Dd Nirvana 02 Dec '18

02 Dec '18

Hi guys, I found that seL4's ARM version still need "isb" and "dsb" around updating TTBR0_EL1. This fence will flush the TLB and will affect IPC performance. However, it seems that enabling ASID can avoid this costs. I am not sure, is there any concern that makes seL4 to avoid using ASID? BTW, I have seen ASID management in seL4 (ASID control and ASID pool), so maybe I misunderstood something? Dong Du, Shanghai Jiao Tong University

2 1