/tech/ - Technology★

what the fuck?

GNU/SEL4 when?

>>949641 (OP)

>high reliability and secure microkernel

>running on backdoored Intel and AMD processors

The only thing this matters to is the handful of people wanting to run seL4 on their x64 IoT device rather than Windows like everyone else.

It would have been better for them to formally verify the Multicore support, they should have recognized x64 as the low priority it is.

>>949692

I want that! Fuck Linux.

>>949707

Unortunately for you, pretty much nobody writes drivers or user space programs for L4, not even the L4 people. They use it as a hypervisor nowadays.

So if you were to use it on the desktop, you would probably be just recreating Qubes OS, but with seL4 replacing Xen. So you would still be using Linux.

Ideally, they would actually build an OS around seL4 itself, sort of like what MINIX is trying to do by porting NetBSD stuff.

I don't want to virtualize an entire OS for each fucking program and driver running.

>>949713

Still, Qubes with seL4 replacing Xen would be nice for the security assurances alone.

>>949714

This

>>949713

https://www.qubes-os.org/attachment/wiki/QubesArchitecture/arch-spec-0.3.pdf

Qubes poopood the idea back in 2010.

It seems the seL4 people have been looking into porting it though.

https://sel4.systems/pipermail/devel/2016-March/000760.html

>>949713

>nobody writes drivers or user space programs for L4

Then they should start doing so.

The only argument I remember for Linux was that it's "free" and "not as bad as Windows" while Windows has a microkernel and they have a shitkernel you have to recompile in order to add or remove functionality.

How about a proper kernel then?

>not even the L4 people.

Probably because the L4 people are writing L4.

>>949740

Yeah man i'm sure that their machine checked proof is wrong because of the license and code of conduct

>>949724

>Windows NT

>Microkernel

Maybe in 1993.

>>949713

You don't need drivers or a user space. Linus said Linux is an operating system. :^)

>>949769

Okay you're right it's actually hybrid

>>949836

It's about as monolithic as it can get at this point.

>>949836

K E R N E L S P A C E S C R O L L B A R S

>>949692

I've actually been looking into that. They got halfway through porting Hurd to L4/pistachio around 2004, but abandoned it because userspace capabilities weren't high-performance enough. Assuming pistachio and seL4 aren't very different from each other, it should be relatively simple to port Hurd/L4 to seL4.

>>949692

Nobody is investing their time making it happen now. It won't happen until somebody takes the time to make it happen.

>>949713

>sort of like what MINIX is trying to do by porting NetBSD stuff.

So the Minix guys are trying to make a crappy clone of OSX?

>>949692

>wanting GNUshit

90% of the problems with GNU/Linux stem from GNU. Why bother putting so much effort into porting all of the GNU software and its derivatives when you could start from scratch and achieve something better in a shorter time.

>>949714

>Still, Qubes with seL4 replacing Xen would be nice for the security assurances alone.

Or you could just create a good OS rather than trying to solve the problem of old software being shit by containerizing everything.

>>949768

This.

>>950038

All you need to do is port glibc to SLE4. There is hardly any other code in GNU that specifically relies on Linux.

>>950044

Yeah take this great very well designed formally verified system and port this massive pile of horribly bloated shit on top

>>951038

You know what I do not appreciate about glibc? The feature macros. It's unnecessary. If I am writing a program that uses strcasestr, it doesn't matter if it's compatible with any other program but the call to strcasestr. GNU/FSF etc. do this to make software developers forced into a situation to license their software with the GPL. It's garbage. I can write and have written a strcasestr function that doesn't need shitty GNU software.

I hope for a day that the only GPL'd software in a Linux is the kernel itself, and I hope that that day will lead to the Linux kernel to being relicensed to something that is not GPL.

>>951041

>retards crying about the GPL like it's legitimate

Is there anything more obnoxious?

>>951059

GPL restricts your freedom.

>>951041

>I hope that that day will lead to the Linux kernel to being relicensed to something that is not GPL.

AFAIK Linux does not require contributors to transfer copyright to Linus or the Linux Foundation, so there are tons of issues with relicensing. Each contributor with code in the kernel would have to be tracked down and would have to agree to the change. Or their portion of the code would have to be rewritten, probably in a clean-room manner.

You could fork the kernel and wait for all of what was written up to your fork become public domain. That'll probably be in the mid-2100s, depending on how long Linus and the other contributors live. Take your statins.

>>950038

>Or you could just create a good OS rather than trying to solve the problem of old software being shit by containerizing everything

You can't throw out old software every few years and expect to stay relevant.

Serious backwards compatibility is one of the things that make Windows the only usable Os for most people.

>>951041

Quite a few functions and macros in the Linux kernel are licensed under the GPL for the same reason, to force developers of kernel modules to license their code under the GPL. Insidiously many aren't, its only the more useful ones you would need later on in the development of whatever you were making.

>I hope for a day that the only GPL'd software in a Linux is the kernel itself

And I hope for the day when Linux becomes another one of the many relics of computing which are no longer used.

>>951059

The only thing the GPL protects against is good software ever being written.

>>951109

>You can't throw out old software every few years and expect to stay relevant.

Backwards compatibility is a relatively recent phenomenon in computing and even what we have today is far from perfect, with many programs from the 90's and mid 00's experiencing compatibility issues with modern OSs (or simply being broken such as with Mac programs that used endian-specific code when Apple switched from PPC to x86). But what end users and most programmers fail to see is the repercussions of demanding backwards compatibility.

What if I told you that CPUs could have an order of magnitude more compute for any given power consumption?

What if I told you that RAM could have an order of magnitude more throughput for any given number of PCB traces?

What if I told you that you could trust your operating system completely even though it might have some non-free/binary-blob components?

What if I told you that you could have an OS which was mathematically proven to be secure against attack?

Because we can do that now, but it would break backwards compatibility. It has forced a set of hardware and software paradigms upon computing and as a result has led us down a path of diminishing returns.

>Serious backwards compatibility is one of the things that make Windows the only usable Os for most people.

Many people only use Windows for things like Word, email, and internet. And to be honest I don't give a fuck about most computer users anyway.

>>951038

Did you know that GNU has a system that does things like that? It's called GNU Hurd.

>>949768

>lol it's proooved! XD

>you're wrong!

back to reddit friend

>What if I told you that you could trust your operating system completely even though it might have some non-free/binary-blob components?

do you mean the blobs would be unprivileged and can't access side channels, or are you just retarded?

>>951041

Why? What's so wrong about the BSD systems?

>>951130

BLOBs can be constructed such that they can be proven to only do certain things without access to the source code.

>>951125

>Because we can do that now, but it would break backwards compatibility. It has forced a set of hardware and software paradigms upon computing and as a result has led us down a path of diminishing returns.

They don't do it because of the 60 million line problem.

https://www.openhub.net/p/chrome/analyses/latest/languages_summary

https://www.openhub.net/p/firefox/analyses/latest/languages_summary

https://www.openhub.net/p/gcc/analyses/latest/languages_summary

https://www.openhub.net/p/gnome/analyses/latest/languages_summary

https://www.openhub.net/p/linux/analyses/latest/languages_summary

First of all, memory for PCs (and soon for workstations)
runs for about $30/MB, and 8 additional MB take care of both
X and GNU Emacs.

In addition, I won't say much about X, which I dislike,
although if I'm not mistaken most of the bloat has occurred
because of vendor requests.  X 10 was much leaner, and
provided more than sufficient functionality as far as I'm
concerned.

With respect to Emacs, may I remind you that the original
version ran on ITS on a PDP-10, whose address space was 1
moby, i.e. 256 thousand 36-bit words (that's a little over 1
Mbyte).  It had plenty of space to contain many large files,
and the actual program was a not-too-large fraction of that
space.

>>951130

The main attraction of seL4 is the strict isolation of programs it provides, the kernel is formally proven to only allow programs to access memory regions they have been allocated (either memory allocated specifically for that program or memory allocated as a shared buffer between it and another program).

Say you have two programs and a DMA capable peripheral device

>Program A which is a user application

>Program B which is a GPU driver

>Device C which is a GPU capable of self hosted DMA

You also have four memory regions managed by seL4

>Memory regions 1 and 2 which are large and exclusively allocated to A and B respectively (1 can only be accessed by A and 2 can only be accessed by B)

>Memory region 3 which is small and able to be accessed by A and B

>Memory region 4 which represents C and can be accessed by B

The IOMMU on the processor is configured to not allow C to access anything other than 3, from the perspective of C the only memory in the system is 3.

When A wants to have C display something it writes data to the shared memory region 3 and informs B that there is something to display. B then looks at the data in 3 and informs C what it needs to do by sending a message to it by writing to 4. C, having received instructions from B, uses its DMA engines to access 3 and copy the data to itself and then do what it needs to do to display what A wanted on the screen.

Why it doesn't matter if B is a binary blob is because it has no privileges, unlike with monolithic and hybrid kernel architectures which have device drivers run in privileged mode (and can therefore access any region of memory it wishes) it can only access what it needs in order to perform its task of controlling the GPU. To complement this the IOMMU is setup to only allow C to access the memory it needs, B can't use the DMA engines of C to bypass the restrictions imposed on it by seL4 (this isn't something which is practical in monolithic and hybrid kernel architectures).

>>951298

And whats really frustrating with the Linux kernel is that much of that code is there to provide backwards compatibility to hardware and software from 20 years ago, there is also code bloat because its all written in C rather than languages which have native support for things like OO. If a group of developers were to rewite Linux in C++ and only support current generation hardware then I suspect the result would be somewhere around 4 million lines of code.

>>951398

install gentoo

>>951125

>Backwards compatibility is a relatively recent phenomenon

I guess counting 20 years as "recent" is very convenient, so you can pretend Linux is a recent project and still hope it will go somewhere.

>But what end users and most programmers fail to see is the repercussions of demanding backwards compatibility.

And what ivory tower devs fail to see is the repercussion of breaking backwards compatibility: people lose the reasons they had to use your stuff.

>And to be honest I don't give a fuck about most computer users anyway.

And this is why you'll never accomplish anything.

>>951518

Breaking backwards compatibility isn't a big problem for those of us who believe in software freedom. Whatever a developer chooses for a specific program, the user will always have the freedom to change it to fit as required for the user.

HOLY SHIT HOW DID I MISS THIS???

Hopefully Genode gets into a more usable state. I wanna get off this monolithic kernel train, and Fuchsia is looking to be just as botneted as everything else Jewgle puts out.

>>951865

And then users will bitch forever when the freedom to change it means sitting down for 3 months of skilled development time.

>>962180

The act of designing software is a sophisticated task and this is normal for all software. For some reason, people are able to wait many months to order a builder to build a house or a car producer to build a car; if you tell a user that it will take months to modify software, then that's too much for that user.

>>962585

It's not just months though--it's years. Only recently have I gotten KDE Plasma with Wayland to work soundly. And, btrfs is still garbage.

>>949641 (OP)

>it's another thread shilling DOA bullshit

Refer to >>964707