Devel December 2018

devel@sel4.systems

21 participants
17 discussions

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2018