- Devel - lists.sel4.systems

Hello world - simple example thread creation
by Piotr 31 May '15

31 May '15

I would like to start from scratch - simple thread or process creation helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4 application, but I am looking for something smaller. I have found here on page 39 "Creating a Thread in Own AS and cspace_t" http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf example of thread creation. Unfortunetly I cannot find header file with " cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements? Are there any small and simple hello-world tutorials or examples avaliable?

1 0

why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys
by Pei.XiLong(裴喜龙) 29 May '15

29 May '15

Hi, Siwei Zhuang, Why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the foundation of libmuslc, it shoud be a libc for any seL4 program, and there should be no diference among any branches. https://github.com/seL4/libsel4muslcsys/commits/camkes Xilong Pei Tongji University 2015/5/29

3 3

[sel4] Porting seL4 to RISC-V - Status Report 1
by Hesham ALMatary 26 May '15

26 May '15

Hi all, As a warm up, I've written a blog entry [1] of the project giving some introductory details for both RISC-V and seL4 microkernel and what has been done so far. Open to questions/suggestions. [1] http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-… Thanks, -- Hesham

2 3

Progress of bringing Genode to seL4
by Norman Feske 26 May '15

26 May '15

Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

Virtual address space (kernelBase) restriction
by Hesham ALMatary 23 May '15

23 May '15

Hi all, Is it a must that every platform/architecture mapped to virtual addresses higher than 0xF0000000? Thanks -- Hesham

1 0

lowRISC Google Summer of Code
by Stefan Wallentowitz 19 May '15

19 May '15

Hi all, I just wanted to take the chance to introduce Hesham ALMatary and myself. Hesham participates in Google's Summer of Code in the lowRISC organization and I am his mentor. During summer, Hesham will port seL4 to the RISC-V architecture, specifically for the lowRISC project. Please find more details here: http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/ Hesham and I will keep you updated about the progress, I believe he will also give updates in his blog: http://heshamelmatary.blogspot.it/. Best Regards, Stefan

2 1

sel4 example compilation - cygwin
by Piotr 12 May '15

12 May '15

Hi, I am trying to compile example from 'Download' tutorial under Cygwin. http://sel4.systems/Download/ What I get is: [KERNEL] [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/ia32/machine_asm.s [AS] src/arch/ia32/machine_asm.o /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages: /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i' .......... What to do with it?

4 3

CSpace: resolveAddressBits
by Norman Feske 04 May '15

04 May '15

Hello, I am trying to construct a custom CSpace for my root task using seL4's guarded page-table concept. At the 1st level, there is a CNode with a radix of 12 and a guard of 0. At the 2nd level, there is a CNode with a radix of 14 and a guard of 6. After copying the initial capabilities to the 2nd-level CNode, switching to this CSpace, and invoking a system call that takes a capability as argument (seL4_TCB_Suspend), the kernel tells me: <<seL4 [decodeInvocation/609 Te3ffa880 @10245c2]: Attempted to invoke a null cap #1.>> The problem seems to be a failed 'lookupCapAndSlot', which internally calls 'resolveAddressBits': https://github.com/seL4/seL4/blob/experimental/src/kernel/cspace.c#L138 While inspecting the function, it does not appeared to me why it does not consider any guard bits within the while loop. The 'levelBits' variable is simply set to 'radixBits'. Interestingly, the same function in the master branch looks different. Here, the 'guardBits' are taken into account, which is consistent with the documentation. I wonder, why differs the experimental branch to the master branch in this respect? Is there a way to construct the scenario above with the experimental branch? The only work-around I see is to allocate an intermediate CNode with a size of 2^6 that sits between the 1st and 2nd level. Or is there a better way? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 2

Does sel4 support pthread?
by 小健 24 Apr '15

24 Apr '15

I am using sel4 to develop a multi-thread program on ARM platform. I know that sel4 support musl libc. But when I call __pthread_create the program returns an error. Does sel4 support pthread on ARM platform? By the way, I get the libmuslc from seL4test. So if there is a musl libc which has pthread inside that can be used by sel4, please tell me where I can get it. Thank you.

2 1

Port seL4 to allwinnerA20
by Jensen Zhang 20 Apr '15

20 Apr '15

Hello everyone, We have ported seL4 to allwinnerA20, although the cache cannot still work well. All tests passed, except for CACHEFLUSH0001 and CACHEFLUSH0002. A git clone can be gotten from here [1]. And the 'zener' directory in this project has a similar structure to sel4test. But there is a problem about TIMER API. For allwinnerA20, there are several registers (Timer IRQ Enable/Status Register) used by all timers. Both kernel and libsel4platsupport will use timers, and they have to use different timers. But some registers can be accessed by both kernel and libsel4platsupport. That's very dangerous! Because libsel4platsupport can disable the timer of kernel by modifying the register. How to solve this problem? [1] git clone http://elastos.org/review/HD-Elastos -- Jensen Zhang Tongji University

2 1