Search results for "developer hangout" - Devel

Re: Reminder seL4 developer hangout

by Gerwin Klein

The next one will flip time zones again, so don't worry if you miss this one. Cheers, Gerwin > On 31 May 2022, at 10:02, Isaac Beckett <isaactbeckett(a)gmail.com> wrote: > > Oh boy, 3AM! I hope to make it, but if I sound tired, that’s why. > >> Date: Mon, 30 May 2022 00:08:16 +0000 >> From: Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> >> Subject: [seL4] Reminder seL4 developer hangout >> To: "devel(a)sel4.systems" <devel(a)sel4.systems> >> Message-ID: <MEAPR01MB44693624005ED9CB8CFDD3A7DEDD9(a)MEAPR01MB4469.aus >> prd01.prod.outlook.com> >> Content-Type: text/plain; charset="iso-8859-1" >> >> Hi all >> >> A friendly reminder that the seL4 developer hangout is on again this week: >> >> Wed, Jun 1, 7am (UTC), Topics: (open) >> >> * Sydney: Wed, Jun 1, 5pm >> * Central Europe: Wed, Jun 1, 9am >> * US Pacific Time: Wed, Jun 1, 12 midnight >> >> Zoom link: https://unsw.zoom.us/j/82640784431 >> >> cheers >> Birg >> >> >> >> --- >> >> Dr. Birgit Brecknell >> >> Project Officer >> >> Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> >> >> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> >> >> 0433 880 571 >> >> >> >> Mon 9am-5pm >> >> Wed 9am-12pm >> >> Fri 9am-5pm > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

2 years, 10 months

Re: Reminder seL4 developer hangout

by Gerwin Klein

Hey Stewart, sure, everybody is welcome! Cheers, Gerwin > On 22 Mar 2022, at 4:16 pm, sjwebb(a)student.unimelb.edu.au wrote: > > Hi Birgit, > > I am a University of Melbourne student working on an seL4 project for my Computer Science Masters under Toby Murray. > > Mind if I join the hangout? It would perhaps help a lot for me to speak to some other people who have worked with seL4. > > My masters research project is one nicked from Gernot a few years back, looking into mapping an object-capability programming language onto seL4's capability system. > > Cheers, > Stewart > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

3 years

Re: Reminder seL4 developer hangout/video call

by Gernot Heiser

Wed 07:00 UTC (Wed 17:00 EAST) is actually the time of the AGM according to my calendar. Gernot > On 4 Apr 2022, at 14:56, Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> wrote: > > Hi all > > A friendly reminder that the seL4 developer hangout is on this week: > > Wed, Apr 6, 7am (UTC), Topics: (open) > > * Sydney: Wed, Apr 6, 5pm > * Central Europe: Wed, Apr 6, 9am > * US Pacific Time: Wed, Apr 6, 12 midnight > > (There are too many time zones in the world to cite them all :-)) > > Zoom link: https://unsw.zoom.us/j/82640784431 > > Cheers, > Birg > > > > --- > > Dr. Birgit Brecknell > > Project Officer > > Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> > > seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> > > 0433 880 571 > > > > Mon 9am-5pm > > Wed 9am-12pm > > Fri 9am-5pm > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

3 years

High-throughput asyncrhonous driver API?

by Andrew Warkentin

I remember talk in one of the developer hangouts I was in about a proof of concept for a high-throughput asynchronous driver layer for seL4 (presumably based on notifications). Has code for this been released anywhere? I'm going to be starting on my own IPC transport layer and I want to include asynchronous message passing as an option.

2 years, 6 months

Re: Reminder seL4 developer hangout

by Nataliya Korovkina

Hi all, I'd like to offer a short topic: status of Github repositories of Core Platform as well as repositories of seL4 with sel4CP support. The reason I'm asking is I'm looking to add Ultra96v2 support to sel4cp. I have added the board to sel4cp (locally), but the point is that the current seL4 branch "sel4cp-core-support" is behind the seL4 mainline, so I locally applied patches with Ultr96V2 support to the branch. Eventually, all works fine, and I don't mind having a better understanding of which repositories it's reasonable to contribute. Best, Nataliya On Sun, Feb 19, 2023 at 6:10 PM Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> wrote: > > Hi all > > A friendly reminder that the seL4 developer hangout is on again this week: > > Tue, Feb 21, 9pm (UTC), Topics: (open) > > * Sydney: Wed, Feb 22, 8am > * Central Europe: Tue, Feb 21, 10pm > * US Pacific Time: Tue, Feb 21, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > cheers > Birg > > > > --- > > Dr. Birgit Brecknell > > Project Officer > > Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> > > seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> > > 0433 880 571 > > > > Mon 9am-5pm > > Wed 9am-12pm > > Fri 9am-5pm > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

2 years, 1 month

Re: seL4 developer hangout/video call

by Gerwin Klein

There is no recording, but I'm planning to put together a high-level summary and post that next week. Cheers, Gerwin > On 5 Nov 2021, at 14:48, Jimmy Brush via Devel <devel(a)sel4.systems> wrote: > > Will recordings or notes from these meetings be made available? > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

3 years, 5 months

Re: Reminder seL4 developer hangout/video call

by Gerwin Klein

Yes, they clash. The audience apart from June, you, and me is distinct, though, so it shouldn't really be a problem. Cheers, Gerwin > On 4 Apr 2022, at 16:11, Gernot Heiser <gernot(a)unsw.edu.au> wrote: > > Wed 07:00 UTC (Wed 17:00 EAST) is actually the time of the AGM according to my calendar. > > Gernot > >> On 4 Apr 2022, at 14:56, Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> wrote: >> >> Hi all >> >> A friendly reminder that the seL4 developer hangout is on this week: >> >> Wed, Apr 6, 7am (UTC), Topics: (open) >> >> * Sydney: Wed, Apr 6, 5pm >> * Central Europe: Wed, Apr 6, 9am >> * US Pacific Time: Wed, Apr 6, 12 midnight >> >> (There are too many time zones in the world to cite them all :-)) >> >> Zoom link: https://unsw.zoom.us/j/82640784431 >> >> Cheers, >> Birg >> >> >> >> --- >> >> Dr. Birgit Brecknell >> >> Project Officer >> >> Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> >> >> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> >> >> 0433 880 571 >> >> >> >> Mon 9am-5pm >> >> Wed 9am-12pm >> >> Fri 9am-5pm >> >> _______________________________________________ >> Devel mailing list -- devel(a)sel4.systems >> To unsubscribe send an email to devel-leave(a)sel4.systems > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems

3 years

OpenPower/PowerPC/ppc64le port: major concerns and obstacles

by Isaac Beckett

Hello seL4 devel! Recently I was on the developer hangout meeting and brought up a ppc port. Interest seemed low, and some even called ppc a “niche” architecture which seems unfair. There was also the much more concrete concerns of funding and overall maintenance. I believe an PPC port would be very valuable, and I plan to do a whole essay/write up of some sort, but I am also not the most familiar with the technical challenges, and could use more information on those. I do think there is definitely people who would want to run seL4 on PowerPC platforms. PowerPC is one of the few ISAs that has existing, modern hardware without closed-source binary blobs, which I believe pose a real threat to the trustworthiness of the hardware seL4 is currently capable of running on.

3 years

Re: OpenPower/PowerPC/ppc64le port: major concerns and obstacles

by William ML Leslie

On Wed, 6 Apr 2022 at 13:44, Isaac Beckett <isaactbeckett(a)gmail.com> wrote: > Hello seL4 devel! Recently I was on the developer hangout meeting and > brought up a ppc port. Interest seemed low, and some even called ppc a > “niche” architecture which seems unfair. > > There was also the much more concrete concerns of funding and overall > maintenance. I believe an PPC port would be very valuable, and I plan to do > a whole essay/write up of some sort, but I am also not the most familiar > with the technical challenges, and could use more information on those. > I won't be online tonight, but I +1'd you then and I'll +1 you now. What sort of powerpc hardware are people using and able to develop for? I really only know of game consoles, and with the exception of the PS3, these tend to be so locked down that people don't seem to port other operating systems to them. I know that Raptor Talos workstations are quite nice and not so expensive when you compare them with the current state of RISC-V systems that are actually usable as desktops, but they are still out of reach of many hobbyists. IIRC someone (Gerwin?) recently did a breakdown of the costs of a port to a new architecture, including costs of verification. I guess the challenge is finding someone for whom that cost is well worth it. -- William ML Leslie

3 years

Re: seL4 vs QNX and Linux benchmarks

by Bob Trower

The topic of sel4 vs QNX performance came up in the developer hangout and I found the entire discussion perplexing for the following reasons: - not inconsequential, Gernot, who I presume is reasonably expert, was strongly of the opinion it was a non-issue. - marginal performance gains, even if possible, are not even remotely warranted at the cost of any security whatsoever. - some timing issues may be security critical and altering them could compromise the security of the kernel. - hardware capacity is vastly improved in speed as of 2024 by the time sel4 is fully productionized hardware capacity will most likely erase any differential in speed. - I do not find it hard to believe that sel4 is perfectly adequate as RTOS within its current architecture. - There does not seem to me to be any advantage in modifying access to the kernel and there are plenty of disadvantages. It's all downside. The OS is open source, so people are at liberty to modify as they please. They just can't call it sel4. - To me, the moniker 'sel4' is a promise and a guarantee and that promise cannot reasonably be kept by making special use-case exceptions. - QNX minimum requirements call for a greater than 1GHz processor here: https://www.qnx.com/developers/docs/6.5.0SP1.update/com.qnx.doc.momentics_i… - Say, for the sake of argument, there is a system call scenario whereby the kernel architecture is causing an unwarranted delay. That might be a defect and could be addressed as such. Finally, there is an old development rule of thumb that first you make it work before you look to optimize. I have been researching security since the late 1980s. I designed and wrote the secure network access system for a Canadian bank in the early 1990s. As it happens, I designed a security protocol twenty years ago that is in use by the Canadian mint to secure money. Since 1992, security has been an integral part of my ongoing research project into data packaging. Years ago I got permission to release code using Gutmann's cryptlib and I spent a great deal of time reviewing and learning from that code. I don't really hold myself out as an expert WRT security. However, I have much to say about it, and I do have some knowledge. I would not presume to question Gernot's judgment with respect to sel4 either security or otherwise. Gernot has expressed confidence in sel4 and that is good enough for me. On Thu, Apr 18, 2024 at 10:31 PM Gernot Heiser via Devel <devel(a)sel4.systems> wrote: > On 18 Apr 2024, at 23:55, Andrew Warkentin <andreww591(a)gmail.com> wrote: > > > > Somebody in the Zoom call the other day (IIRC it was Gernot) said that > > seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is > > somehow faster in a simple benchmarking experiment in which a client > > repeatedly sends messages to a bit-bucket server, using the TSC to > > determine timing. > > > > I'm running both QNX and seL4 under identical VirtualBox > > configurations with a single core. I'm using a QNX 6.3.1 x86-32 image > > i have in my collection (x86-64 support was only added in 7.0; this is > > the most recent image I have with dev tools installed). The seL4 > > version I'm using is from February 2022 and is built for x86-64 with > > MCS enabled (the priority of the threads is 255, and both the > > timeslice and budget are the initial thread default of 5 ms). > > > > My benchmark times a loop of 10000 RPCs; for QNX it's just using the > > regular read() function on /dev/null or a custom server that also acts > > like /dev/null but forces a copy of the message into a server-provided > > buffer, and for seL4 I'm directly calling Send()/Recv()/Reply(). I've > > also tested Linux's /dev/null, and QNX's implementation actually seems > > somewhat faster than it (for the system /dev/null; the custom server's > > best case seems only slightly worse than under Linux). > > > > Under QNX and Linux I'm running a C implementation of the benchmark > > and under seL4 I tried both C and Rust implementations (which have > > very similar performance). The messages on QNX and Linux are 100 > > bytes, and on seL4 they are 2 words, which should be hitting the fast > > path. > > > > Here are the best and worst cases I got: > > seL4: 0.114-0.136s > > QNX, custom null server: 0.006-0.063s > > QNX, system null server: 0.002-0.022s > > Linux: 0.004-0.005s > > > > Has anyone else benchmarked seL4 IPC against that of QNX and gotten > > better (or comparable) results for seL4, unlike what I got? Is > > synchronous IPC just less optimized under seL4 than QNX? > > I’m not completely sure what you’re actually measuring here (actually I’m > totally unsure > what your setup really is, I can’t make sense of the above description in > terms of > what the seL4 system is doing). > But measuring performance of a kernel inside a virtual machine is somewhat > pointless at best. > > In any case it seems clear that you’re *not* measuring raw seL4 IPC. > Your quoted cost of a round-trip on seL4 is say 120ms for 10,000 round > trips, > or 12µs for one round trip. You don’t specify the clock rate, but that > would be > somewhere between 12,000 and 50,000 cycles, when a round-trip IPC on x86 > with MCS is <900 cycles > > Note that using Send()/Recv()/Reply() is the wrong way to use seL4 IPC, see > https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/ > However, this will only be about a factor two slower than using the > correct Call()/ReplyWait() incantation. > > In fact, while it is in principle possible to outperform seL4 in IPC, it > is impossible to do so > by more than a few percent, as the seL4 IPC cost is only about 20% higher > than the > pure hardware cost of kernel trap, minimal state save+restore and > switching page tables. > This has been independently established in a peer-reviewed paper, see > https://dl.acm.org/doi/pdf/10.1145/3302424.3303946 > > Everything I’ve ever seen from QNX is that their IPC costs is many > thousands of cycles > (probably >10,000), and at least an order of magnitude slower than seL4’s. > > Gernot > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > -- Bob Trower --- From Gmail webmail account. ---

1 year

Devel search results for query "developer hangout"