- Devel - lists.sel4.systems

Re: [seL4] Suggestion for Abdurahman
by Harry Butterworth 12 Jan '20

12 Jan '20

Take a look at Andy’s Binary Editor nyangau.org/be/be.html and implement an open source equivalent as an integrated debugger for seL4. You will need to be able to get keyboard input, write characters to the screen and get access to files containing the structure definitions. You can provide the structure definitions at boot time. You won’t need an OS or POSIX or even much of a standard library; the implementation just requires the language runtime, a parser, a few data structures, and a bit of printf-like code. You could write it all and make it completely self-contained which would allow you to keep the footprint really small. Steps to proceed are as follows: 1) Pick a language. I’d probably pick C++ for this but you might also consider D or Rust or maybe COGENT. 2) Work out how to write a small test program in your chosen language and get seL4 to run it. This will require an implementation of the runtime for the language. If this hasn’t been done already for the language you pick, you can implement bits of the runtime as you go along when they are needed. If you fail at this step, go back to step 1, pick a different language. 3) Work out how to get your test program to write characters to the screen (or serial console perhaps). 4) Work out how to get keyboard input. 5) Define the grammar for the structure definitions. If you happen to pick COGENT you might look at DARGENT. 6) Understand the Model View Controller design pattern. 7) Write a parser to parse the structure definitions to create a model. You’ll want the model to use lazy evaluation so the whole system defined by the structure definitions can be represented but there is only overhead for the bits that are being actively browsed. 8) Implement a view for the model which displays a selected part on the console. 9) Implement a controller for the view and model which is an event loop that handles keyboard input and manipulates the model and view accordingly. After getting your new debugger to work for browsing the entire system including the kernel data structures, find a way to integrate it which allows it to be configured to run with only the capability it needs for the debugging you want to do. After that you could make sure it can be used for debugging real time applications with a guarantee not to interfere with their real time operation. For bonus points, if you have picked COGENT, you might finish off with a formal proof that your debugger displays the correct characters on the console according to the structure definitions, contents of memory and history of keyboard input. This (in fact the whole task) would be complicated by the fact that the memory contents change all the time underneath you as you browse a live system so you’d have to work out how to incorporate that and still prove something useful. Enjoy On Fri, Jan 10, 2020 at 8:21 PM abdi mahmud haji < abdimahmudhaji227(a)gmail.com> wrote: > hey guys > I'm abdurahman and i have same question for you > i have been studying microkernel for a little well now specially seL4 and > i have done almost every tutorials in sel4 -tutorials and i have a crazy > idea ,that is i when try to build a 'shell or prompt' on the seL4 > mircokernel but i don't have any idea how to do or where to start . does > any one have a suggestion for me > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel >

1 1

(no subject)
by abdi mahmud haji 11 Jan '20

11 Jan '20

hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me

4 3

Using seL4_DebugSnapshot()
by rasd＠riseup.net 09 Jan '20

09 Jan '20

Can someone provide more information about using seL4_DebugSnapshot? >From its description in documentation, I would expect it to print out a CapDL struct over a debugging port/console. Instead, it waits for user commands for various data types sends back binary data[0]. Since the commands are all 0xa0-0xff[1], it doesn't seem like DebugSnapshot expects a human and a keyboard to be present on the other end. Is there some internal debugging tool that is supposed to be used with this system call? Is DebugSnapshot still used? Any advice or information is appreciated. ras [0] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/capdl.c [1] https://github.com/seL4/seL4/blob/master/include/machine/capdl.h

2 1

答复: some question about the compile of global-components in camkes_arm_vm project
by yadong.li 09 Jan '20

09 Jan '20

I found some example in odroid_vm, I want to make sure my understanding is correct? In CMakeLists.txt DeclareCAmkESComponent(HelloWorld) is just tell me there is a component called “HelloWorld” If you want this component to be compiled to project You must add call in your assembly in .cmakes file like below: assembly { composition { component HelloWorld hello; } Thank you very much 发件人: yadong.li 发送时间: 2019年12月28日 15:32 收件人: 'devel(a)sel4.systems' 主题: some question about the compile of global-components in camkes_arm_vm project hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

2 1

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes and the warning was resolved and I could build seL4. Is pulling that docker image supposed to be necessary? Thanks! -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

2 1

fastpath performance test
by Dd Nirvana 05 Jan '20

05 Jan '20

Hi guys, I have downloaded the lastest seL4 repo and built the seL4 kernel. And I reuse the code in sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c. To test the fast, I made minor modifications: first, set caller and callee to the same priority; second, caller uses seL4_Call while callee uses seL4_ReplyRecv. However, the fastpath takes more than 2000 cycles (a round trip). Build: use the lastest provided docker and ../init-build.sh - DPLATFORM=x86_64 -DCMAKE_BUILD_TYPE=Release Both hardware and Qemu show similar results. (4.0GHz skylake CPU) BTW. The manifest is the same as https://sel4.systems/About/Performance/home.pml (i.e., bf13e9f673484825a60f9950cf688ff33ac841ad). Any advices about the issue? Best, Jinyu Gu, Institute of Parallel and Distributed Systems (IPADS), School of Software, Shanghai Jiao Tong University

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9 SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15 So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9. (Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 01 Jan '20

01 Jan '20

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf 0x41000000 CACHE: Misaligned operation at range [10598000, 105980a4] CACHE: Misaligned operation at range [10599000, 105a3434] CACHE: Misaligned operation at range [105a3434, 105a3c23] CACHE: Misaligned operation at range [107fc000, 1080a038] ## Starting application at 0x10598000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[10598000..1080a037] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 1069c064. Loaded DTB from 1069c064. paddr=[10038000..10042fff] ELF-loading image 'kernel' paddr=[10000000..10037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' paddr=[10043000..1019bfff] vaddr=[10000..168fff] virt_entry=188dc ELF loader relocated, continuing boot... Enabling MMU and paging It seems It does not go to kernel-image entry point and bootstrap the kernel! Is there any thing that I need to perform on board? Thank you, Parvaneh Aghajani.

2 1