- Devel - lists.sel4.systems

Re: Rust bindings, was: Re: What do you want from the next seL4 Summit?
by Andrew Warkentin 13 Jan '21

13 Jan '21

On 1/12/21, Jimmy Brush <code(a)jimmah.com> wrote: > > Based on these discussions we have started prototyping a > procedurally-generated native rust seL4 library built from a complete > seL4 IDL specification. > > Once we have built this out we intend to share our learnings and > continue to advocate for changes to seL4 and/or upstream work that > improves the experience for everyone building their own language > bindings or dynamic systems on seL4. > Is there any particular reason why you didn't just port your bindings to feL4? It does use the C bindings underneath (through bindgen), but I don't think that's a big problem, as they don't have much room for memory bugs (and UX/RT is not meant to be a "Rust OS" like Redox and Robigalia; it will just be an OS that has a lot of subsystems written in Rust, but there will still be a lot of third-party C code). It was relatively easy for me to port your old bindings and allocators to my fork of feL4. Here is the UX/RT subproject with the bindings and allocators (rust-bitmap, rust-sel4, and sel4-alloc are forked from Robigalia; the rest is from feL4 except for sel4-slabmalloc): https://gitlab.com/uxrt/core-supervisor/fel4/

1 0

What do you want from the next seL4 Summit?
by Gernot Heiser 13 Jan '21

13 Jan '21

Dear seL4 community, A couple months ago we had a successful 3rd seL4 Summit. Despite having to revert to virtual format, it was a very good event, and I’m sure I’m not the only one who enjoyed it. Thanks for the great work to our friends at IAI, Siege Technologies and the Griffiss Institute for the organisation, and DARPA and AFRL for funding the Summit in particular, and seL4 in general for many years. DARPA funding for the seL4 Summits is coming to an end, and, as you know, the seL4 Foundation has been created as the community-driven guardians of seL4. Among others, this means it is time to think about how future summits will look like. For example, much of the funding for seL4 has come from defence budgets, but the technology is equally important for critical civilian systems, and the Summit should reflect this. We would also like to see broadened community participation, maybe a flavour of FODSEM or LCA, while continuing to involve our corporate partners, who are key to financial support and widespread deployment. So we are asking you, the seL4 developer community, what you would like to see at the next summit, in content and format. After this informal community consultation we expect to issue an EOI for organising the next Summit, anticipated timeframe is similar as in the past, Sep–Nov. Please make/discuss suggestions via reply email within a month (and note that I’ll be off-lline for a fair chunk of this). Gernot PS: For those who have missed it, the Summit presentations are still available for about another month to those registered, see https://www.sel4-us.org/summit2020/

4 4

Ethdriver OdroidC2
by Nkem Ogosi 06 Jan '21

06 Jan '21

I have been trying to get an example sel4 programs that demonstrate a network connection, most notably picoserver, to work on an odroid board. Many resources were referenced such as an eth driver and the types of files I needed to get a camkes implementation to work. However, I haven't been very successful. I don't really understand what I am supposed to be included in some of the files or more importantly where to find the information I need to populate the file specifically for odroid as similar files for other boards have other files as dependecies. Sincerly, Nkem

1 0

seL4 YouTube Channel
by Gernot Heiser 31 Dec '20

31 Dec '20

Dear seL4 community, As some of you have already noticed, we now have a YouTube channel run by the seL4 Foundation: https://www.youtube.com/channel/UCIqVY1XFPOPIZ1z2A9TrmMA/about. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems. More to come, enjoy Gernot

2 2

Debugging seL4 for RISC-V
by porter.188＠osu.edu 24 Dec '20

24 Dec '20

I'm building a simple "hello, world" project and running into some bugs. The code works, but the after execution there is an exception. It appears to be in restore_user_context or nearby. Can anyone point out what the problem could be here? user@user-KVM:/mnt/data/sel4hello_manifest/build$ qemu-system-riscv64 --machine spike --nographic --serial mon:stdio --m size=4095M --bios images/hello-image-riscv-spike bbl loader ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..80312d0f] Looking for DTB in CPIO archive...found at 802e5910. Loaded DTB from 802e5910. paddr=[8401e000..8401efff] ELF-loading image 'kernel' paddr=[84000000..8401dfff] vaddr=[ffffffff84000000..ffffffff8401dfff] virt_entry=ffffffff84000000 ELF-loading image 'hello' paddr=[8401f000..84157fff] vaddr=[10000..148fff] virt_entry=14aa4 Jumping to kernel-image entry point... Init local IRQ Initialing PLIC... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac Caught cap fault in send phase at address 0 while trying to handle: vm fault on code at address 0 with status 0x1 in thread 0xffffffc17fee8200 "rootserver" at address 0 With stack: 0x143ea0: 0x143ec0 0x143ea8: 0x101ea 0x143eb0: 0x143f00 0x143eb8: 0x14b90 0x143ec0: 0x0 0x143ec8: 0x143f30 0x143ed0: 0x143f20 0x143ed8: 0x143f10 0x143ee0: 0x1 0x143ee8: 0x101d6 0x143ef0: 0x144000 0x143ef8: 0x14cbc 0x143f00: 0x0 0x143f08: 0x14a000 0x143f10: 0x20110 0x143f18: 0x0

1 0

I.MX7, Timeout in SEL4 USB driver
by MOHAMAD REZA SHAFIEI 16 Dec '20

16 Dec '20

Hi there, I'm working on USB Storage in Sel4 on I.MX7, when I read/write some block of data from/to USB Driver , sometimes US‌‌‌B Driver fails with this output by this output: ehci_wait_for_completion@async.c:594 Timeout this error happened in ehci_schedule_xact function that waiting for transaction completion. I port USB Driver on I.MX7 but because of above bug, it isn't Stable. Can anyone help me how to fix this bug? regards, Mohamad -- This email was Anti Virus checked by Security Gateway.

1 0

[Camkes] Access control for memory or the entire component?
by Seo Yeon Hwang 11 Dec '20

11 Dec '20

Hello all, I wonder if it is possible for a component to directly access some specific part of memory with an address or access the whole component (not some dataports) using Camkes. I can see how to set up the permissions (R/W) for each dataport in the tutorial #port_privileges part, but I wonder if one component can read some specific memory region with starting and ending addresses, or read the whole memory where another component is located. Thanks for your help! Best regards, Seoyeon

2 1

CfP: FOSDEM 2021 - Microkernel Devroom
by Martin Decky 08 Dec '20

08 Dec '20

Microkernel Devroom at FOSDEM 2021 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based operating systems will meet on-line as part of FOSDEM 2021 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 6th 2021. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages, tools and toolchains * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * development processes, debugging * maintenance, testing and release engineering * security and robustness * trends and challenges * community and governance * use cases, experiences and status updates * best practices, lessons learned and demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 26th 2020. Please use the Pentabarf website [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Please make sure to select the Microkernel devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes), excluding a Q&A part * your short bio * your photo The talks will be pre-recorded in advance in January and streamed during the event. This means that you will need to complete and submit your talk by around mid January. However, each speaker should be also present on-line just after the streaming of the talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2020 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are also invited to send any other suggestions for what you want to see or do at the devroom to the mailing list. About the Devroom Since the first Microkernel devroom at FOSDEM 2012 [4], this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based and unikernel-based operating systems. By now it has become a somewhat institutionalized tradition for the 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 different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2021 Due to the extraordinary mode of organization of FOSDEM 2021 (being an on-line event for the first time), many practical aspects of the devroom are still in the process of determination. For example, the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A), but the technical details are still sketchy at this moment. The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of our devroom regularly. We will keep updating it as new guidelines will be determined by the FOSDEM organizers. Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time. However, we plan to organize an on-line replacement. The details will be announced later in January. On the other hand, the on-line nature of the devroom allows us to "overflow" to a second day in case we receive a substatial number of quality proposals. About FOSDEM FOSDEM [6] is a two-day event organised by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognised as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) 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 proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, and in the past instances certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2021 will be organized as an on-line event. Despite this, the participation in FOSDEM is still totally free, although the organisers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2020-12-26: Deadline for talk proposal submission * 2020-12-31: Schedule published and speakers notified of acceptance * mid January 2021: Time frame for talk pre-recoding * 2021-02-06: Devroom taking place on-line Contact In case of any questions, comments and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2021 are: * Martin Decky * Jakub Jermar Links [1] https://fosdem.org/2021/ [2] https://penta.fosdem.org/submission/FOSDEM21/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2021/practical/conduct/

1 0

More enhancements for general-purpose systems that wouldn't be accepted into seL4?
by Andrew Warkentin 06 Dec '20

06 Dec '20

Am I correct to assume that support for running 32-bit code on a 64-bit kernel using compatibility mode rather than virtualization and support for (presumably limited) direct system calls from VMs, bypassing any user-mode VMM (using something like Xen's trampoline page) wouldn't be accepted into seL4? These are yet more things that I am going to want at some point and can't think of any other way to do them (besides adding them to the kernel) without significant penalties to hardware compatibility (in the case of the 32-bit support; while UX/RT will mostly be focused on 64-bit systems, it will support 32-bit Linux programs in its compatibility layer) or performance (in the case of direct kernel traps from VMs; I am planning to write a dynamic general-purpose hypervisor to go with UX/RT eventually, and adding an extra trap into the VMM on every IPC would likely add a fair bit of overhead).

4 8

whether seL4 support c++ code
by yadong.li 03 Dec '20

03 Dec '20

Hi， I have two questions about whether seL4 support C++: 1. When we create a component, whether the src file of component can be c++ style file like **.cxx, or **.cpp ? I found it will print “camkes.environment.c : undefined reference to run” error when compile 2. If our app code write by c++, how can I use it in seL4 environment as native component？Is there some example ？ Thank you very much.

3 2