- Devel - lists.sel4.systems

the omap3 image can't run on pandaboard
by XilongPei(裴喜龙) 13 Nov '14

13 Nov '14

Hi, The OMAP3 Beagle board is too out of date, I buy a pandaboard http://omappedia.org/wiki/PandaBoard , but the omap3 image can't run on this board. The error information look like these: ----------------------------------------------------------------- Panda # Panda # fatls mmc 0 31644 mlo 208784 u-boot.img 4782336 uimage 208273 uinitrd 449 boot.scr 3092757 sel4test-driver-image-arm-omap3 9 file(s), 0 dir(s) Panda # fatload mmc 0 0x81ff8000 omap3 reading sel4test-driver-image-arm-omap3 3092757 bytes read Panda # go 0x82000000 ## Starting application at 0x82000000 ... data abort MAYBE you should read doc/README.arm-unaligned-accesses pc : [<820024bc>] lr : [<82002194>] sp : 822d7f78 ip : 00000000 fp : 822d7f84 r10: 00000002 r9 : 00000000 r8 : bfefdf68 r7 : bffabd14 r6 : 82000000 r5 : bfeffd5c r4 : 00000002 r3 : 49020014 r2 : 00000001 r1 : 00000000 r0 : 0000000a Flags: Nzcv IRQs off FIQs off Mode SVC_32 Resetting CPU ... resetting ... ----------------------------------------------------------------- Who can give me some help? thanks first! Xilong Pei Tongji University Shanghai China 2014/11/13

1 0

seL4 : Queries
by Yashwardhan Singh 09 Nov '14

09 Nov '14

Hi I am trying to modify the seL4 scheduler as a part of my project. I was wondering if there is any function present in the library OS like scanf which can help me in writing an interactive process , to measure the response time of the scheduler for interactive process. I was also curious if there is any shell like framework for sel4, from which multiple processes can be started concurrently and so that they run in background. Is there a benchmark suite for generation of performance metrics using the data structures present in /kernel/src/arch/ia32/api/benchmark. Please help. Thanks and Regards Yash

2 1

Clang & LLVM
by da Tyga 08 Nov '14

08 Nov '14

Hi ! There seems to be a general trend towards using Clang / LLVM in the ARM area. AFAIK ARM are going LLVM for V8. Is it viable to do seL4 work with that environment? Cheers!

1 0

Reasoning behind the root cnode's guard value
by Norman Feske 05 Nov '14

05 Nov '14

Hello, the seL4 kernel constructs the root task's CNode (in kernel/boot.c) by using the configurable number CONFIG_ROOT_CNODE_SIZE_BITS as size and a guard value calculated as 32 - CONFIG_ROOT_CNODE_SIZE_BITS. I understand that it makes the capability name space nicely linear. But on the hand, doesn't it impede the number of kernel objects addressable by root task? When using Genode's core as root task on seL4, I will need to maintain a large number of capabilities to kernel objects, in particular one for each page managed by the core process. Naturally. I would like to organize the root task's capability namespace hierarchically, allocating CNodes depending on the dynamic work load. As far as I understand, however, root task would have no way to address slots within such additional CNodes because all address bits are already consumed by the root CNode indices + guard. For example, how is root task supposed to specify capabilities that are not contained in the root CNode as "service" argument to functions like 'seL4_TCB_WriteRegisters'? One way I see would be to move capabilities back and forth between the root CNode and other CNodes using 'seL4_CNode_Copy', effectively using the root CNode as a kind of CNode cache. But this solution seems overly complicated. Another way would be to dimension CONFIG_ROOT_CNODE_SIZE_BITS pessimistically. But introducing such an upper bound a-priory would somehow contradict with seL4's otherwise nicely dynamic resource management. Yet another way would be to let root task use a smaller guard value that leaves enough bits available to be used for second-level or third-level CNodes. But since that would require a change of the kernel code, I suspect that this approach is not in line with right seL4 way. Could you share the reasoning behind the guard-value calculation and help me to get on the right track? Or would you consider a configurable guard value for root task as a reasonable feature request? 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

2 2

Make Error : seL4 kernel
by Yashwardhan Singh 29 Oct '14

29 Oct '14

Hi I downloaded the latest repository of seL4 from GitHub. When I am trying to build the kernel using make for ia32 architecture and pc99 platform I am getting this error : *yashward@macaroni-09:~/cs736-proj/seL4$ make ARCH=ia32 PLAT=pc99* * [CC] kernel_final.s* *src/arch/ia32/kernel/boot_sys.c:75:26: error: ‘CONFIG_MAX_NUM_IOAPIC’ undeclared here (not in a function)* * paddr_t ioapic_paddr[CONFIG_MAX_NUM_IOAPIC];* * ^* *src/plat/pc99/machine/hardware.c: In function ‘maskInterrupt’:* *src/plat/pc99/machine/hardware.c:54:9: error: implicit declaration of function ‘pic_mask_irq’ [-Werror=implicit-function-declaration]* * pic_mask_irq(mask, irq);* * ^* *src/plat/pc99/machine/hardware.c:54:9: error: nested extern declaration of ‘pic_mask_irq’ [-Werror=nested-externs]* *cc1: all warnings being treated as errors* *make: *** [kernel_final.s] Error 1* I am trying to compile it on a 64 bit machine with red hat linux machine operating system on it. Please help me with this issue. Regards Yash

2 1

A missing function?
by chengkunck＠gmail.com 29 Oct '14

29 Oct '14

Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth.

3 4

Dynamic number of arguments in interface method
by Lukas Masek 27 Oct '14

27 Oct '14

Hello Everyone, I'm trying to implement interface which will accept similar syntax like printf method in c is accepting. syntax of function in c: void printer(int i,char* format,...){ } However I have problem to create valid syntax in idl4 interface definition for CAmkES. Can somebody help me to create valid syntax for procedure definition used in interface? procedure Test { void printer(in int i,in string format,in ...); }; Or is this approach even supported? Also If there is more complex reference guide for idl4 used by CAmkES which I can use to find answers like this? Thank you for help and if question is stupid please accept my apologize I'm just starting to play with this project. BR, Casper

2 1

sel4 on multi-core
by Yuxin Ren 21 Oct '14

21 Oct '14

Hi All, I think, on IA-32, sel4 supports multi-core machine. But I do not how to use that. Here I have two specfic questions. 1. How to assign a specific core to a process/thread? And can I change this affinity? 2. How to two process/threads communicate via IPC on different cores? I want to know some implementation details in kernel to support cross-core IPC. Could anyone explain its logic or tell me the code for it in the kernel? Thank you very much. Best, Yuxin

6 6

IPC performance for slowpath
by Yuxin Ren 18 Oct '14

18 Oct '14

Hi All, I find there have slow and fast path for IPC. I want to know the performance difference between those two. More accurate, on x86, how many cycles for slow path round-trip ipc between two address space?(on single core) And how many for fast path? Thank you very much. Yuxin

2 3

How to get a capability of a virtual address
by Yuxin Ren 18 Oct '14

18 Oct '14

Hi All, In sel4, how can a process/thread get the capability of its virtual address? I know there is function vspace_get_cap(vspace_t *vspace, void *vaddr) But how can I know the current vspace the process/thread is in? Thank you very much. Yuxin

3 5