Devel October 2016

devel@sel4.systems

24 participants
30 discussions

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

18 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 13 Oct '16

13 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

Spawn new process
by Andrew Mine 11 Oct '16

11 Oct '16

Hi I am working with sel4-tutorials and wanted to spawn a new process using int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka, vspace_t *spawner_vspace, sel4utils_process_config_t config); However, I am not able to understand some of the details required to initialize the parameter config used in the function. Can someone give me link to an example of sorts where this is used. Regards Andrew Mine

1 0

adding new code to VMM on TK1
by PX 11 Oct '16

11 Oct '16

Hi, Please forgive my ignorance. I want to add new code to the seL4-based VM for TK1. However, I find it is hard to add new directories. The newly added directories are always ignored or can not be found by compiler. What's the correct way to add new directories? which scripts we should look into? thanks Peng

3 4

questions about the device driver in virtual machine on ARM seL4 (TK1 board)
by PX 06 Oct '16

06 Oct '16

Hi, I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio. 2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. Do I miss something? Thanks Peng

2 4

Post-mutikernel approach to multiprocessor support?
by Jeff Waugh 04 Oct '16

04 Oct '16

Hi all, Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support? (I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.) Thanks, Jeff

2 5

Possible seL4 developer day Dec 15–16 in Malibu
by Gernot.Heiser＠data61.csiro.au 04 Oct '16

04 Oct '16

Dear seL4 Community, Part of the Data61 seL4 Team will be in Malibu in mid December and we are considering running another Developer Day. As in the past, this would actually run over 1.5 days, from the morning of the 15th to about mid-day on the 16th and be a combination of lectures and hands-on sessions. As usually we’ll try to make this a free event, provided that our friends at HRL Labs can host us. We have been discussing the possibility of providing an advanced stream besides the “newbie” version we had been running in the past. Right now, we are gauging interest in this. So, if you are interested in participating on those two days, would you please let Ihor know 1) how many participants you expect from your organisation 2) whether you are interested in the newbie or an advanced version, 3) if advanced, what topics you would like covered Examples of advanced materials - advanced driver writing/porting, eg how to port a real Linux driver - advanced real-time topics: eg building stuff from scratch rather than filling in templates - locking and synchronisation - architecting seL4-based systems - process for building real systems: throw everything into a VM, and then extract bits into native components - anything specific you are interested in We’d imagine the advanced stream to be less structured, emphasising largely independent work on a specific problem, with people around to help. It could even be solving a particular problem you have (but we’d need to understand what you’re trying to build beforehand). Gernot & Ihor

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2016