- Devel - lists.sel4.systems

Missing untypeds on x86?
by Jeff Waugh 18 Oct '16

18 Oct '16

Hi all, Using x86 master on qemu with 2G memory, the kernel's map looks good: Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fee0000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from 7ffe0000 size 20000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 But the largest physical address of non-device untyped I get from bootinfo is 0x1faf9000. Same at 1G to 3G, though it does the right thing at 128M. On the other hand, x86_64 looks fine with 0x7ffc0000, and adapts to more. btw, very exciting to see x86_64 code land! Working well so far. Thanks, Jeff

2 1

question about adding device to ARM VM linux
by PX 18 Oct '16

18 Oct '16

Hi, all I have a question about adding a device to ARM VM linux. When a device is added to the vmlinux, two functions, map_device () and map_ram () are invoked. I don't understand the purpose of map_ram(). In map_device(), the capacity to the device is used to set up the mapping between a virtual address and the MMIO (of the device). Then, in the map_ram (), a capacity to the virtual address is allocated. I am confused because the virtual address is already mapped to the mmio of the device. why do we need to allocate a capacity for the virtual address? Should the capacity be the same as the one for the device? Thanks Peng

1 0

Benchmark results?
by Corey Richardson 18 Oct '16

18 Oct '16

Hello, Are there any public results from sel4bench, or should I get my own numbers for some hardware? -- cmr http://octayn.net/

2 1

adding code to the main.c for ARM VMM
by PX 18 Oct '16

18 Oct '16

Hi, I have posted this question before and my problem is not totally solved because I am not familiar with Makefile. I try to make my question more specific as follows. I want to add new code, which is already organized under a directory, say, test. I want to add the directory test to main.c file for ARM VMM, located at ~/projects/vm/apps/vm/components/VM/src/main.c. In the program, we want to refer to the sub-directories by relative path to the directory test. what is the easy to do that? How can we add the directory test to the search path so that we can include the header files by the relative path to the directory test, say include "test1/test1.h"? We tried to modify the makefile at ~projects/vm/apps/vm, but we have to add all the sub-directories, and there are problems for the files with the same name under different directories. thanks Peng

2 1

Re: [seL4] endpoint.c
by Vasily A. Sartakov 17 Oct '16

17 Oct '16

> we take address that causes syscall from the ksCurThread and set them back. Thus, FaultInstruction should point to something different, right? > I have add FaultInstruction in the same manner as it made in ARM platform: sub lr, lr, #4 /* Store FaultInstruction */ str lr, [sp, #(PT_FaultInstruction - PT_LR_svc)] I am tacking address of an instruction causes exception, subtract 4 from the value, and save it into the FauiltInstruction. Now get* and set* functions are: word_t PURE getRestartPC(tcb_t *thread) { return getRegister(thread, FaultInstruction); } void setNextPC(tcb_t *thread, word_t v) { setRegister(thread, CP0_EPC, v); } Also, Faultinstruction is part of frameRegisters and «linked» with cp0_epc of seL4_UserContext (sel4arch.xml) Now both tests are passed: Starting test 27: TEST_RECYCLE0001 TEST_RECYCLE0001 Running test RECYCLE0001 (Basic endpoint recycle testing.) <<seL4 [decodeInvocation/609 T0x8fee3f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #101.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #163.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #230.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #303.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #364.>> <<seL4 [decodeInvocation/609 T0x809db100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #428.>> <<seL4 [decodeInvocation/609 T0x809db300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #491.>> <<seL4 [decodeInvocation/609 T0x809db500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #564.>> <<seL4 [decodeInvocation/609 T0x809db700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #619.>> <<seL4 [decodeInvocation/609 T0x809db900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #694.>> <<seL4 [decodeInvocation/609 T0x809dbb00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #761.>> <<seL4 [decodeInvocation/609 T0x809dbd00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #828.>> <<seL4 [decodeInvocation/609 T0x809dbf00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #831.>> <<seL4 [decodeInvocation/609 T0x8fe29100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #898.>> <<seL4 [decodeInvocation/609 T0x8fe29300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #965.>> <<seL4 [decodeInvocation/609 T0x8fe29500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1032.>> <<seL4 [decodeInvocation/609 T0x8fe29700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1099.>> <<seL4 [decodeInvocation/609 T0x8fe29900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1170.>> <<seL4 [decodeInvocation/609 T0x8fe29b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1221.>> <<seL4 [decodeInvocation/609 T0x80a13100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1295.>> <<seL4 [decodeInvocation/609 T0x80a13300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1354.>> <<seL4 [decodeInvocation/609 T0x80a13500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1427.>> <<seL4 [decodeInvocation/609 T0x80a13700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1490.>> <<seL4 [decodeInvocation/609 T0x80a13900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1563.>> <<seL4 [decodeInvocation/609 T0x80a13b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1628.>> <<seL4 [decodeInvocation/609 T0x80a13d00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1635.>> <<seL4 [decodeInvocation/609 T0x80a13f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1698.>> <<seL4 [decodeInvocation/609 T0x80aa1100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1765.>> <<seL4 [decodeInvocation/609 T0x80aa1300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1828.>> <<seL4 [decodeInvocation/609 T0x80aa1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1897.>> <<seL4 [decodeInvocation/609 T0x80aa1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1966.>> <<seL4 [decodeInvocation/609 T0x80aa1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #2033.>> Test RECYCLE0001 passed Starting test 28: TEST_RECYCLE0002 TEST_RECYCLE0002 Running test RECYCLE0002 (Recycle deletes caps) <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #361.>> <<..> <<seL4 [decodeInvocation/609 T0x80a90700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2003.>> <<seL4 [decodeInvocation/609 T0x80a90900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2073.>> <<seL4 [decodeInvocation/609 T0x80a90b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2131.>> <<seL4 [decodeInvocation/609 T0x80a90f00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2203.>> Test RECYCLE0002 passed Can you please tell me something about the Faultinstruction context field, and, in general, what the assumptions about the behaviour of CPU you put into the design. For example, in MIPS, in a case of a trap, EPC points on instruction causes a trap, but in a case of an interrupt, PC and further EPC points on next instruction. Should I take this into the account somewhere in the kernel? > >> Hope that helps. >> >> Regards, >> Hesham >> ________________________________________ >> From: Devel <devel-bounces(a)sel4.systems> on behalf of Vasily A.Sartakov <sartakov(a)ksyslabs.org> >> Sent: Friday, October 14, 2016 12:33 AM >> To: devel(a)sel4.systems >> Subject: [seL4] endpoint.c >> >> Hello. >> >> I have a problem with endpoint.c test (RECYCLE0001): >> >> Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c >> >> I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look?

2 2

Fwd: Microkernels / Component-based OSes devroom - Call for Participation
by Vasily A. Sartakov 17 Oct '16

17 Oct '16

Just want to invite you to FOSDEM’17 > The developers of several free and open-source microkernel-based > operating systems will meet at FOSDEM 2017 [1] in Brussels, Belgium > and will share a developer room on Saturday of February 04, 2017 [2]. > The devroom is currently looking for content in the form of talks and > activities related to the area of microkernel-based operating systems. > Possible topics include, but are not limited to: > > * Introduction of a specific OS or framework > * Design of subsystems and the general architecture of an OS > * Enabling support for hardware (architectures, device drivers) > * Used languages and tools > * Maintainance and testing > * Security and robustness > * Trends and challenges > * Use cases, experiences, lessons learned and demos > > Please use the Pentabarf [3] system to submit your proposals and file it > under the track “Microkernels and Component-based OS”. You do not need > to create a new account if you already have one. When in doubt, please > use the devroom mailing list [4]. If you do not want to give a talk > yourself, you may still send suggestions for what else you would like to > see, or do in the devroom. Please send your suggestions to the mailing > list. The deadline for your proposal is on December the 4th. > > Make sure to include the following in your proposal: > > * Title of your talk (will be printed in the FOSDEM booklet) > * Your full name (will be printed in the FOSDEM booklet) > * A short abstract (one or two paragraphs) > * Duration of your talk (please, at least 25 and no longer than 45 min) > > The official devroom schedule (along with the accepted talks) will be > announced on December the 11th on the devroom's mailing list and the > speakers will be notified via e-mail. The schedule will also be published > on the FOSDEM website. > > > About FOSDEM > > FOSDEM is a two-day event organised by volunteers to promote the > widespread use of free and open source software. Taking place in the > beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the > best such conference in Europe. FOSDEM covers a wide spectrum of free > and open source software projects, and offers a platform for people to > collaborate. To this end, FOSDEM has set up developer rooms (devrooms) > with network/internet connectivity and projectors where teams can meet > and showcase their projects. Devrooms are a place for teams to discuss, > hack and publicly present latest directions, lightning talks, news and > discussions. Besides developer rooms, FOSDEM also offers main tracks, > lightning talks, certification exams and project stands. Every year, > FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. > Participation and attendance is totally free, though the organisers > gratefully accept donations and sponsorship. No registration necessary. > > > About the devroom > > Since the first Microkernel devroom in 2012 this devroom has been part of > each following FOSDEM. By now it has become a somewhat institutionalized > tradition for the micro kernel community to meet there; to this date over > a dozen projects have participated in one way or another. Each of the > projects face similar challenges but come up with partially differend > solutions. Therefore, the goal of the Microkernel devroom is to bring the > various projects together, let them exchange ideas, cross-pollinate and > socialize. > > > Social events > > It also has become a habit that the microkernel projects dine together > somewhere in downtown Brussels after the devroom closes. The year 2017 > will not be any different, so there is going to be a microkernel family > dinner on Saturday night. The exact location and time will be specified > later. Consult the FOSDEM web and other projects for additional social > events such as the famous FOSDEM-organized Friday Beer Event and the > FOSDEM-arranged free sightseeing tours for spouses. > > > Important dates recap > > * 04.12.2016: Deadline for submissions > * 11.12.2016: Schedule published and speakers notified of acceptance > * 04.02.2017: The devroom takes places > > > Links > > [1] http://fosdem.org/ > [2] https://fosdem.org/2017/practical/transportation/ > [3] https://fosdem.org/submit > [4] https://lists.fosdem.org/listinfo/microkernel-devroom -- Vasily A. Sartakov sartakov(a)ksyslabs.org

1 0

General Questions
by Mark Reus 17 Oct '16

17 Oct '16

Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards Mark

3 2

endpoint.c
by Vasily A. Sartakov 14 Oct '16

14 Oct '16

Hello. I have a problem with endpoint.c test (RECYCLE0001): Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

sel4 hypervisor communication
by Horace Blanc 12 Oct '16

12 Oct '16

Hi, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? 2) If the VMMs run in kernel mode (PL1), as I was told, does it mean they use hvc commands instead of swi/svc commands when sending messages to seL4 as hypervisor? Thank you in advance,

2 1

syscall.c
by Vasily A. Sartakov 11 Oct '16

11 Oct '16

Greetings. I have moved forward to tests in my our MIPS port. Some of them work fine, but not all. Now I have a question about syscall.c test. What exactly we test here? In ARM-based part I see initialisation of 12 registers, performing syscall with further checking that our initialised registers have original values. So, as far I understand, these registers should be modified in a syscall’s inline, thus, they should be allocated on the stack and reloaded after the end of syscall. Right? My issue here is that I have much many than 12 registers and my compiler chooses them randomly (for me). For example, sometimes it uses only S0-S7 with some T0-T9 registers, sometimes all T0-T9 with some S0-S7 registers. Moreover, I cannot put more than 30 asm instructions in one inline (gcc error), thus, maybe I should specify proper register name here. But for that, I should be sure that I understand this test correct. Can we help me? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2