- Devel - lists.sel4.systems

wrong word spelling in program
by XilongPei(裴喜龙) 27 Nov '14

27 Nov '14

Hi, Who wrote the program in file $/libplatsupport/plat_include/omap4/platsupport/plat/gpt_constants.h , GPT4_DEFICE_PADDR is wrong spelled, it should be GPT1_DEVICE_PADDR. static void *paddrs[] = {(void *) GPT1_DEVICE_PADDR, (void *) GPT2_DEFICE_PADDR, (void *) GPT3_DEFICE_PADDR, (void *) GPT4_DEFICE_PADDR, (void *) GPT5_DEFICE_PADDR, (void *) GPT6_DEFICE_PADDR, (void *) GPT7_DEFICE_PADDR, (void *) GPT8_DEFICE_PADDR, (void *) GPT9_DEFICE_PADDR, (void *) GPT10_DEFICE_PADDR, (void *) GPT11_DEFICE_PADDR}; Xilong Pei Tongji University 2014/11/19

2 1

Confused on porting/using musl lib c
by chengkunck＠gmail.com 27 Nov '14

27 Nov '14

Hi All, I want to use musl lib c but I'm a little confused on the following two projects: libmuslc and musllibc. I went through their Kconfig and brief intros, so my question now is do I need them both to port/use musl lib c on sel4? It might be a dumb question but I'm stuck here, any help is appreciated. Best regards, Kenneth

2 2

where can I get beagle_run_elf program
by XilongPei(裴喜龙) 21 Nov '14

21 Nov '14

Hi, In the Makefile, a program beagle_run_elf is referred, Where can I get it? --------------------------------------- # This relies on a helper script to build a bootable image simulate-beagle: beagle_run_elf images/sel4test-driver-image-arm-omap3 --------------------------------------- Xilong Pei Tongji University 2014/11/19

2 1

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 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