Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Fernando Oleo / Irvise]

[[Original post can be found in 
https://forum.ada-lang.io/t/ironclad-the-hard-real-time-capable-posix-like-kernel-written-in-spark-ada-received-an-nlnet-grant/1281]]

Dear community,

it fills me with joy to announce that Streaksu, the developer of 
Ironclad [1] has been given a grant from the nlnet foundation [2], 
announcement here [3].

If you would like to learn more about Ironclad and the Gloire 
distribution, Streaksu presented the project during AEiC 2024. You can 
find the slides and video here [4].

If you are interested in Ironclad/Gloire, you can check the git repos 
from the main webpage, join the Matrix/Element chatroom or maybe even 
sponsor Streaksu over at his liberapay page [5].

I am very happy to see that Streaksu applied for a grant and was 
accepted. This is what I want to see more of in the community. People 
creating very cool projects that they enjoy working on. Then promoting 
them and seeing if they can make the development of such projects a 
little bit more sustainable for themselves. This also disproves that 
“Ada projects” are not liked or as seen as old by foundations or other 
funding groups.

I am very happy for Streaksu and I hope to test Ironclad in a RISC-V 
board soon!

[1] https://ironclad.nongnu.org/
[2] https://nlnet.nl/
[3] https://nlnet.nl/news/2024/20241003-announcing-Core-call.html
[4] https://www.ada-europe.org/conference2024/adadev.html
[5] https://liberapay.com/streaksu/

Best regards and happy hacking!
Fer

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Thu, 3 Oct 2024 19:38:31 +0200, Fernando Oleo / Irvise wrote:

> [1] https://ironclad.nongnu.org/

It’s not microkernel-based, is it?

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Luke A. Guest]

On 03/10/2024 23:12, Lawrence D'Oliveiro wrote:
> On Thu, 3 Oct 2024 19:38:31 +0200, Fernando Oleo / Irvise wrote:
> 
>> [1] https://ironclad.nongnu.org/
> 
> It’s not microkernel-based, is it?

That's something I intend to work on soon.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Fernando Oleo / Irvise]

On 10/4/24 00:12, Lawrence D'Oliveiro wrote:
> On Thu, 3 Oct 2024 19:38:31 +0200, Fernando Oleo / Irvise wrote:
> 
>> [1] https://ironclad.nongnu.org/
> 
> It’s not microkernel-based, is it?

AFAIK, no. It is POSIX-based/like. It is able to run quite a few *NIX 
applications. You can check the Gloire distribution [1] to test it out :)

If you are interested in microkernels written in Ada, see [2]

[1] https://github.com/Ironclad-Project/Gloire
[2] https://github.com/ohenley/awesome-ada?tab=readme-ov-file#os-and-kernels

Best regards,
Fer

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Kevin Chadwick]

>> [1] https://ironclad.nongnu.org/
>
>It’s not microkernel-based, is it?

Isn't it true that monolithic kernels become more attractive when Cs
 problens are removed with micro kernels swapping problems for new problems?

-- 
Regards, Kc

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Fri, 4 Oct 2024 18:56:58 +0200, Fernando Oleo / Irvise wrote:

> On 10/4/24 00:12, Lawrence D'Oliveiro wrote:
>>
>> On Thu, 3 Oct 2024 19:38:31 +0200, Fernando Oleo / Irvise wrote:
>> 
>>> [1] https://ironclad.nongnu.org/
>> 
>> It’s not microkernel-based, is it?
> 
> AFAIK, no. It is POSIX-based/like.

Pleased to hear that. ;)

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Fri, 4 Oct 2024 19:52:12 -0000 (UTC), Kevin Chadwick wrote:

> Isn't it true that monolithic kernels become more attractive when Cs
> problens are removed with micro kernels swapping problems for new
> problems?

The microkernel proponents still seem to think there is a point to their 
idea, even after decades of real-world experience to the contrary.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Luke A. Guest]

On 04/10/2024 21:05, Lawrence D'Oliveiro wrote:
> On Fri, 4 Oct 2024 19:52:12 -0000 (UTC), Kevin Chadwick wrote:
> 
>> Isn't it true that monolithic kernels become more attractive when Cs
>> problens are removed with micro kernels swapping problems for new
>> problems?
> 
> The microkernel proponents still seem to think there is a point to their
> idea, even after decades of real-world experience to the contrary.

L4 have years of sticking a middle finger up at that.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Paul Rubin]

"Luke A. Guest" <laguest@archeia.com> writes:
> L4 have years of sticking a middle finger up at that.

I also have to wonder whether hypervisors count as microkernels.
Everyone is using them now.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Fri, 4 Oct 2024 23:19:09 +0100, Luke A. Guest wrote:

> On 04/10/2024 21:05, Lawrence D'Oliveiro wrote:
>
>> The microkernel proponents still seem to think there is a point to
>> their idea, even after decades of real-world experience to the
>> contrary.
> 
> L4 have years of sticking a middle finger up at that.

L4 is supposedly being used as the basis of the GNU Hurd kernel. 
Development of that started around the same time as Linux. There are grown 
adults walking the Earth right now who weren’t even born at that time, 
many of them now using Linux for production work, and Hurd still isn’t 
ready for prime time.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Luke A. Guest]

On 05/10/2024 09:11, Lawrence D'Oliveiro wrote:
> On Fri, 4 Oct 2024 23:19:09 +0100, Luke A. Guest wrote:
> 
>> On 04/10/2024 21:05, Lawrence D'Oliveiro wrote:
>>
>>> The microkernel proponents still seem to think there is a point to
>>> their idea, even after decades of real-world experience to the
>>> contrary.
>>
>> L4 have years of sticking a middle finger up at that.
> 
> L4 is supposedly being used as the basis of the GNU Hurd kernel.
> Development of that started around the same time as Linux. There are grown
> adults walking the Earth right now who weren’t even born at that time,
> many of them now using Linux for production work, and Hurd still isn’t
> ready for prime time.

Hurd is never going to happen, because they keep starting, stopping, 
changing kernels, etc.

Anyway, I'm not really interested in yet another nix.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[DrPi]

Le 04/10/2024 à 22:05, Lawrence D'Oliveiro a écrit :
> On Fri, 4 Oct 2024 19:52:12 -0000 (UTC), Kevin Chadwick wrote:
> 
>> Isn't it true that monolithic kernels become more attractive when Cs
>> problens are removed with micro kernels swapping problems for new
>> problems?
> 
> The microkernel proponents still seem to think there is a point to their
> idea, even after decades of real-world experience to the contrary.
Any evidence of this assertion ?

You should try QNX.
My experience with QNX shows that it is far more stable than monolithic 
kernels since buggy drivers can't cause the kernel to panic.
Also, you don't have to recompile the kernel each time a driver needs to 
be recompiled.
I have many other arguments against monolithic kernels.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Luke A. Guest]

On 05/10/2024 17:24, DrPi wrote:
> Le 04/10/2024 à 22:05, Lawrence D'Oliveiro a écrit :
>> On Fri, 4 Oct 2024 19:52:12 -0000 (UTC), Kevin Chadwick wrote:
>>
>>> Isn't it true that monolithic kernels become more attractive when Cs
>>> problens are removed with micro kernels swapping problems for new
>>> problems?
>>
>> The microkernel proponents still seem to think there is a point to their
>> idea, even after decades of real-world experience to the contrary.
> Any evidence of this assertion ?
> 
> You should try QNX.
> My experience with QNX shows that it is far more stable than monolithic 
> kernels since buggy drivers can't cause the kernel to panic.
> Also, you don't have to recompile the kernel each time a driver needs to 
> be recompiled.
> I have many other arguments against monolithic kernels.

Yeah, QNX was solid. Had the source at one point.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Sat, 5 Oct 2024 11:47:41 +0100, Luke A. Guest wrote:

> Hurd is never going to happen, because they keep starting, stopping,
> changing kernels, etc.

Hurd is never going to happen, because they are trying to build it as a 
microkernel.

Re: Ironclad, the hard-Real Time capable POSIX-like kernel written in SPARK/Ada, received an nlnet grant

[Lawrence D'Oliveiro]

On Sat, 5 Oct 2024 18:24:39 +0200, DrPi wrote:

> Le 04/10/2024 à 22:05, Lawrence D'Oliveiro a écrit :
>
>> The microkernel proponents still seem to think there is a point to
>> their idea, even after decades of real-world experience to the
>> contrary.
>
> Any evidence of this assertion ?

Look around you, at what happened when people tried to use microkernels in 
real-world situations. I think Apple tried to use one in its “macOS” (née 
“OS X”), and performance suffered as a result.

> You should try QNX.

Was that used in any high-performance situation?

> Also, you don't have to recompile the kernel each time a driver needs to
> be recompiled.

Linux has supported loadable modules for maybe 30 years now.