L4 went GPL

If it doesn't fit anywhere else, drop it in here. (not to be used as a chat/nonsense section)

Moderator: Moderator Team

Post Reply
alexei
Posts: 137
Joined: Wed Oct 19, 2005 5:29 pm

L4 went GPL

Post by alexei »

L4 went GPL, see http://sel4.systems/
Would it kill Linux kernel?
Shouldn't Wine project make a fork to run on L4 directly?
User avatar
Konata
Posts: 391
Joined: Sun Apr 20, 2014 8:54 pm

Re: L4 went GPL

Post by Konata »

Nothing will kill Linux, it's now a giant hulking parasite in the IT world along with Windows and Java. And quite frankly I'm fine with that, nothing Enterprise is good, it's nice to have a quarantining system so you can simply avoid it and all it's aliments, like Systemd.

Though if you mean if it can be a suitable replacement for GNU/Linux if you don't feel like installing that bloated writhing mass of hastily-written spaghetti C on your computer, that's another story.
In my experience people don't care about how well it functions, they more or less care if it can just run programs and drivers (understandably, an OS is basically a fancy calculator without those).
Now this is where a contradiction comes in, which I humorously like to call the OS/2 Problem. If it has no programs, nobody wants to use it. If it supports another OS's API/ABI, nobody would still use it because they can use the one they use now, or simply use the popular thing. The best option you could go for is porting a lot of software to it, then you'd at least get some userbase which could then carry advertizing it on their shoulders as well. I think FreeBSD is a good example of this. Though it also has a Linux compatibility layer so I guess that doesn't hurt either.

As for L4 itself, it doesn't seem like they even want to be a major runner. They just look like they want to do research, and I really doubt it has any sort of ports system or compatibility layers. Maybe if someone takes it and ports/writes some software for it to turn it into a fully featured OS (much easier said than done, of course) then it could have a chance. I can't seem to find a lot of information on their website, but I don't think they have much of any drivers or software, or even a userland.

Though, I know it's got some Haskell in it, and my very knowledgeable friend just so happened to be trying to write a Haskell OS over FreeBSD, maybe they'll be interested in this. Funny I knew a Haskell microkernel existed but I totally forgot what it was.
erkinalp
Posts: 861
Joined: Sat Dec 20, 2008 5:55 pm
Location: Izmir, TR

Re: L4 went GPL

Post by erkinalp »

There are some well-behavior assumptions in the proof. Should they have used worst-case assumptions throughout the proof, I would use it.
-uses Ubuntu+GNOME 3 GNU/Linux
-likes Free (as in freedom) and Open Source Detergents
-favors open source of Windows 10 under GPL2
Webunny
Posts: 1201
Joined: Sat Apr 28, 2012 1:30 pm

Re: L4 went GPL

Post by Webunny »

alexei wrote:L4 went GPL, see http://sel4.systems/
Would it kill Linux kernel?
Shouldn't Wine project make a fork to run on L4 directly?
Maybe they can use it as base for HURD II now. :geek:
vasily72
Posts: 10
Joined: Wed Oct 23, 2013 12:11 pm

Re: L4 went GPL

Post by vasily72 »

Wow! :shock: I knew about Singularity but until now I didn't know there are other projects like that. I think this is what you call a cutting edge technology. Formally prooved systems are unavoidable future, and existance of L4 and Singularity makes Windows, Unix, ROS ultimately outdated.
Konata wrote:In my experience people don't care about how well it functions, they more or less care if it can just run programs and drivers
Well, people are getting tired of endless bugs, viruses, goverment approved backdoors etc. They want a truly reliable system. L4 could be a solution. ROS wont :).
erkinalp wrote:There are some well-behavior assumptions in the proof. Should they have used worst-case assumptions throughout the proof, I would use it.
Still it's most reliable system ever existed. I think future development would do all remaining hardcore proofs.
Z98
Release Engineer
Posts: 3379
Joined: Tue May 02, 2006 8:16 pm
Contact:

Re: L4 went GPL

Post by Z98 »

People can have absolute reliability. Assuming they're willing to pay millions of dollars per license seat and have something with the functionality of DOS. Or maybe Windows 3.1 at the very most. Oh and you can't use any of the applications you use right now because they'd be incompatible. I don't see anyone falling over themselves to take that leap.
mrugiero
Posts: 482
Joined: Sun Feb 14, 2010 9:12 am

Re: L4 went GPL

Post by mrugiero »

Z98 wrote:People can have absolute reliability. Assuming they're willing to pay millions of dollars per license seat and have something with the functionality of DOS. Or maybe Windows 3.1 at the very most. Oh and you can't use any of the applications you use right now because they'd be incompatible. I don't see anyone falling over themselves to take that leap.
And even if they were compatible, they'd need to also be formally verified, otherwise it becomes unreliable.
erkinalp
Posts: 861
Joined: Sat Dec 20, 2008 5:55 pm
Location: Izmir, TR

Re: L4 went GPL

Post by erkinalp »

Well, people are getting tired of endless bugs, viruses, goverment approved backdoors etc. They want a truly reliable system. L4 could be a solution. ROS wont :).
Well, anyone can (dis)prove ReactOS' architecture too. And he will find many inconsistencies :) About backdoors, there cannot stay a backdoor in a FOSS OS(the first one finds will remove it).
-uses Ubuntu+GNOME 3 GNU/Linux
-likes Free (as in freedom) and Open Source Detergents
-favors open source of Windows 10 under GPL2
vasily72
Posts: 10
Joined: Wed Oct 23, 2013 12:11 pm

Re: L4 went GPL

Post by vasily72 »

Z98 wrote:People can have absolute reliability. Assuming they're willing to pay millions of dollars per license seat.
They don't have to pay. L4 is under GPL already :).
Z98 wrote:Something with the functionality of DOS.
At least you have a choice. You can use formally verified OS for critical operations (online banking for example) and traditional OS for everything else.
mrugiero wrote:And even if they were compatible, they'd need to also be formally verified, otherwise it becomes unreliable.
Yes, but I believe developing and verifing usermode application is much easier task. And you dont't have to write a huge lot of them. Actually you can have only one - web browser.
erkinalp wrote:About backdoors, there cannot stay a backdoor in a FOSS OS(the first one finds will remove it).
Not true, unfortunately.
Z98
Release Engineer
Posts: 3379
Joined: Tue May 02, 2006 8:16 pm
Contact:

Re: L4 went GPL

Post by Z98 »

vasily72 wrote:
Z98 wrote:People can have absolute reliability. Assuming they're willing to pay millions of dollars per license seat.
They don't have to pay. L4 is under GPL already :).
L4 is also basically useless without the rest of the software stack on top of it, none of which has actually been verified.
vasily72 wrote:
mrugiero wrote:And even if they were compatible, they'd need to also be formally verified, otherwise it becomes unreliable.
Yes, but I believe developing and verifing usermode application is much easier task.
No, no it's really not.
vasily72
Posts: 10
Joined: Wed Oct 23, 2013 12:11 pm

Re: L4 went GPL

Post by vasily72 »

Z98 wrote:L4 is also basically useless without the rest of the software stack on top of it, none of which has actually been verified.
OK. We already have a kernel. That's half of the work done. Now let them do the other half, write applications, and there would be total happiness :).

I just want to say that formal methods are absolute neccesity for software development. Companies should pay more attention to them instead of generating tons of bells and whistles (aka Metro UI).
Tonix
Posts: 89
Joined: Tue May 22, 2007 11:33 am

Re: L4 went GPL

Post by Tonix »

vasily72 wrote: OK. We already have a kernel. That's half of the work done. Now let them do the other half, write applications, and there would be total happiness :).
The Kernel is only a starting point... what you say i like "we have the control unit... let them build the car".


A system is not only kernel and apps, you need drivers.
without certified drivers a secure kernel does not exist.

an example:
A filesystem driver must protect user data from being readed/written without permission.
if a driver tell the kernel that all user have permission to read some data the kernel take this information as is
even if this is not true.

A kernel without drivers is useless.
Post Reply

Who is online

Users browsing this forum: No registered users and 16 guests