- Devel - lists.sel4.systems

run seL4 on pandaboard
by Pei.XiLong(裴喜龙) 14 Nov '14

14 Nov '14

Hi, I have built an image for my pandaboard, but I have no bootelf u-boot command, I use go command instead, get the following error: Panda # fatload mmc 0 0x82000000 sel4test-driver-image-arm-omap3 Panda # go 0x82008000 ## Startting application at 0x82008000 ... after this message, the system is dead. How to do next? Xilong Pei Tongji University 2014/11/14

1 0

Re-identification of capabilities
by Norman Feske 13 Nov '14

13 Nov '14

Hello, I hope you don't mind me spamming the list with my problems. I have a question about the association of capabilities with process-local meta data. As far as I understand, the "badging" of capabilities is the recommended mechanism for servers to attach a server-local meaningful value to a capability. After having handed out the capability to a client, it gets this value reported each time the client (or any other process to which the capability was delegated to) invokes the capability or delegates the capability back to the server (e.g., as RPC argument). Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). The factory is responsible for physically allocating objects (e.g., in Genode's case, one example would be the core process that hands out dataspaces). The mediator is a process that sits in-between the client and the factory (in the Genode world, this could the the init process). It keeps records about the allocation and may use this information to implement a policy. The client is the designated user of the object. To create an object, C will call M, which, in turn, will call F on behalf of C: alloc create F <-------- M <--------- C F will create the actual object and a corresponding badged capability and returns the badged capability as return value to M. Because M wants to keep records about the lifetime and parameters of the created objects, it needs to associate a process-local meta-data structure to the capability. badged cap F ---------> M C : (meta data <-> cap) M stores the meta data in a process-local data base using the cap as key. It then hands out the cap to the actual client. Sometime later, the client decides to destroy the object (or perform another operation at M that takes the cap as argument): badged cap F M ---------> C | | uses object (e.g., invoking the cap) destroy | (cap arg) | ? <----------+ When M receives the destroy request with the cap of the to-be-destroyed object as argument, it wants to look up the corresponding meta data from its data base. But unfortunately, the cap argument of the destroy function got assigned a new local name within M (some number within the receive window of M). How can M find the meta data associated with the allocated object? 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

5 8

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 10 Nov '14

10 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 06 Nov '14

06 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