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

    From Fernando Oleo / Irvise@irvise_ml@irvise.xyz to comp.lang.ada on Thu Oct 3 19:38:31 2024
    From Newsgroup: comp.lang.ada

    [[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
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Thu Oct 3 22:12:00 2024
    From Newsgroup: comp.lang.ada

    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?
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Fri Oct 4 11:28:27 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Fernando Oleo / Irvise@irvise_ml@irvise.xyz to comp.lang.ada on Fri Oct 4 18:56:58 2024
    From Newsgroup: comp.lang.ada

    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
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Kevin Chadwick@kc-usenet@chadwicks.me.uk to comp.lang.ada on Fri Oct 4 19:52:12 2024
    From Newsgroup: comp.lang.ada

    [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
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Fri Oct 4 20:04:55 2024
    From Newsgroup: comp.lang.ada

    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. ;)
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Fri Oct 4 20:05:39 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Fri Oct 4 23:19:09 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sat Oct 5 08:11:12 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Sat Oct 5 11:47:41 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From DrPi@314@drpi.fr to comp.lang.ada on Sat Oct 5 18:24:39 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Sat Oct 5 17:27:44 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sat Oct 5 23:08:16 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sat Oct 5 23:10:42 2024
    From Newsgroup: comp.lang.ada

    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.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From DrPi@314@drpi.fr to comp.lang.ada on Sun Oct 6 15:53:25 2024
    From Newsgroup: comp.lang.ada

    Le 06/10/2024 à 01:10, Lawrence D'Oliveiro a écrit :
    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.
    MacOS-X is a hybrid kernel. Half way betwwen micro-kernel and monolithic kernel.


    You should try QNX.

    Was that used in any high-performance situation?
    Sure. QNX is designed for hard real time.


    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.
    Yes, they exist but they are some sort of exception.
    Look at linux kernel release logs like this one https://www.cnx-software.com/2024/09/16/linux-6-11-release-notable-changes-arm-risc-v-and-mips-architectures/
    Most of the log content is about drivers.
    And when time comes to debugging a kernel driver...
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From DrPi@314@drpi.fr to comp.lang.ada on Sun Oct 6 16:19:29 2024
    From Newsgroup: comp.lang.ada

    Le 06/10/2024 à 15:53, DrPi a écrit :
    Le 06/10/2024 à 01:10, Lawrence D'Oliveiro a écrit :
    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.
    Oh, I forgot, Minix (which is a micro-kernel OS) is embedded is every
    Intel x86 processor.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Sun Oct 6 20:46:16 2024
    From Newsgroup: comp.lang.ada

    On 06/10/2024 14:53, DrPi wrote:
    Le 06/10/2024 à 01:10, Lawrence D'Oliveiro a écrit :
    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.
    MacOS-X is a hybrid kernel. Half way betwwen micro-kernel and monolithic kernel.

    MacOS uses Mach which is well known for being a terrible implementation
    of the microkernel, that's why it's a hybrid, same reason NT got changed
    into a hybrid too.


    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sun Oct 6 21:25:38 2024
    From Newsgroup: comp.lang.ada

    On Sun, 6 Oct 2024 15:53:25 +0200, DrPi wrote:

    Le 06/10/2024 à 01:10, Lawrence D'Oliveiro a écrit :

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

    You should try QNX.

    Was that used in any high-performance situation?

    Sure. QNX is designed for hard real time.

    Not the same thing. “Hard real time” does not imply “high performance”.
    Ask the folks working on the very subject of this thread.

    Is the QNX “microkernel” similar in style to the old Amiga “microkernel”?
    That is, instead of copying message buffers around, it just passed around pointers to those message buffers? That would give you speed, but
    sacrifice much of the robustness that a microkernel is supposed to offer.

    Linux has supported loadable modules for maybe 30 years now.

    Yes, they exist but they are some sort of exception.

    No they are not. They typically make up the majority of the kernel.
    Looking at my current kernel, the base kernel file is less than 10MB in
    size, whereas the directory containing loadable modules for that kernel is about 10× that.

    Of course, this is your choice; some prefer to build all the options they
    need into a single monolithic image, for faster loading. Linux is all
    about having the choice.

    And when time comes to debugging a kernel driver...

    Hurd should have found that easy to do, if microkernels really make things easy to do. But it didn’t.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sun Oct 6 21:30:30 2024
    From Newsgroup: comp.lang.ada

    On Sun, 6 Oct 2024 20:46:16 +0100, Luke A. Guest wrote:

    MacOS uses Mach which is well known for being a terrible implementation
    of the microkernel, that's why it's a hybrid, same reason NT got changed
    into a hybrid too.

    And yet they are both still outperformed by Linux on the same hardware.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Mon Oct 7 00:02:34 2024
    From Newsgroup: comp.lang.ada

    On 06/10/2024 22:30, Lawrence D'Oliveiro wrote:
    On Sun, 6 Oct 2024 20:46:16 +0100, Luke A. Guest wrote:

    MacOS uses Mach which is well known for being a terrible implementation
    of the microkernel, that's why it's a hybrid, same reason NT got changed
    into a hybrid too.

    And yet they are both still outperformed by Linux on the same hardware.

    What's your point? I said Mach is the worst example of a microkernel,
    it's been proven, decades ago.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Sun Oct 6 23:48:34 2024
    From Newsgroup: comp.lang.ada

    On Mon, 7 Oct 2024 00:02:34 +0100, Luke A. Guest wrote:

    On 06/10/2024 22:30, Lawrence D'Oliveiro wrote:

    On Sun, 6 Oct 2024 20:46:16 +0100, Luke A. Guest wrote:

    MacOS uses Mach which is well known for being a terrible
    implementation of the microkernel, that's why it's a hybrid, same
    reason NT got changed into a hybrid too.

    And yet they are both still outperformed by Linux on the same hardware.

    What's your point? I said Mach is the worst example of a microkernel,
    it's been proven, decades ago.

    So where is there a better one? It’s long been established that
    microkernel performance is terrible, and the theoretical reliability advantages have failed to materialize. What reason is there left to use
    them? None.

    After 40 or more years trying to tout the idea, it’s time to give up.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Mon Oct 7 09:21:26 2024
    From Newsgroup: comp.lang.ada

    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:
    On Mon, 7 Oct 2024 00:02:34 +0100, Luke A. Guest wrote:

    On 06/10/2024 22:30, Lawrence D'Oliveiro wrote:

    On Sun, 6 Oct 2024 20:46:16 +0100, Luke A. Guest wrote:

    MacOS uses Mach which is well known for being a terrible
    implementation of the microkernel, that's why it's a hybrid, same
    reason NT got changed into a hybrid too.

    And yet they are both still outperformed by Linux on the same hardware.

    What's your point? I said Mach is the worst example of a microkernel,
    it's been proven, decades ago.

    So where is there a better one? It’s long been established that
    microkernel performance is terrible, and the theoretical reliability advantages have failed to materialize. What reason is there left to use
    them? None.

    After 40 or more years trying to tout the idea, it’s time to give up.

    I already said, L4. But you don't want to listen you just want to slag
    off something you don't or won't understand and bang on about Linux,
    which was always meant to be a server OS, not a desktop one.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Mon Oct 7 09:22:48 2024
    From Newsgroup: comp.lang.ada

    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:

    After 40 or more years trying to tout the idea, it’s time to give up.

    Why are you wanging on about this on an Ada group? Try this on alt.os.development.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Chris Townley@news@cct-net.co.uk to comp.lang.ada on Mon Oct 7 11:25:52 2024
    From Newsgroup: comp.lang.ada

    On 07/10/2024 09:22, Luke A. Guest wrote:
    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:

    After 40 or more years trying to tout the idea, it’s time to give up.

    Why are you wanging on about this on an Ada group? Try this on alt.os.development.

    He is just trolling!
    --
    Chris

    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Mon Oct 7 15:13:09 2024
    From Newsgroup: comp.lang.ada

    On 07/10/2024 11:25, Chris Townley wrote:
    On 07/10/2024 09:22, Luke A. Guest wrote:
    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:

    After 40 or more years trying to tout the idea, it’s time to give up.

    Why are you wanging on about this on an Ada group? Try this on
    alt.os.development.

    He is just trolling!


    I know. I just I'd point him in the right direction and see if he dare
    go there.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From =?UTF-8?Q?Niocl=C3=A1s=C3=A1n_Caile=C3=A1n_de_Ghlost=C3=A9ir?=@Master_Fontaine_is_dishonest@Strand_in_London.Gov.UK to comp.lang.ada on Mon Oct 7 17:56:31 2024
    From Newsgroup: comp.lang.ada

    On Sun, 6 Oct 2024, Lawrence D'Oliveiro wrote:
    "On Sun, 6 Oct 2024 16:19:29 +0200, DrPi wrote:

    Oh, I forgot, Minix (which is a micro-kernel OS) is embedded is every
    Intel x86 processor.

    Bad example. <https://www.theregister.com/2018/08/29/intel_jtag_flaw/>
    "


    Hello.

    I wrote in "Four gigabytes of RAM but "Not enough core" during
    installation" in news:g77u2n$mfs$1@aioe.org in news:comp.os.minix 16
    years ago in 2008:
    "Dear all,
    On a computer with four gigabytes of RAM, I booted
    Minix_IDE-3.1.2a.iso which reported
    "[..]
    Physical memory: total 6196 KB, system 5700 KB, free 496 KB.
    [..]
    /etc/rc: /bin/service: Not enough core
    [..]"
    for the standard >= 16 MB RAM installation option,
    and it reported a total of less than 2000 KB for
    the 8192 KB RAM installation option, again moaning
    "Not enough core".

    Do you have any suggestions?

    With kind regards,
    Nick Paul Colin Gloster"
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Luke A. Guest@laguest@archeia.com to comp.lang.ada on Mon Oct 7 21:47:18 2024
    From Newsgroup: comp.lang.ada

    On 07/10/2024 21:30, Lawrence D'Oliveiro wrote:
    On Mon, 7 Oct 2024 09:21:26 +0100, Luke A. Guest wrote:

    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:

    After 40 or more years trying to tout the idea, it’s time to give up.

    I already said, L4.

    The one that Hurd has been trying to use, without success.

    Has anybody else made production use of it?

    I already said in another message, about L3.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Lawrence D'Oliveiro@ldo@nz.invalid to comp.lang.ada on Fri Oct 11 23:25:56 2024
    From Newsgroup: comp.lang.ada

    On Mon, 7 Oct 2024 21:47:18 +0100, Luke A. Guest wrote:

    On 07/10/2024 21:30, Lawrence D'Oliveiro wrote:

    On Mon, 7 Oct 2024 09:21:26 +0100, Luke A. Guest wrote:

    On 07/10/2024 00:48, Lawrence D'Oliveiro wrote:

    After 40 or more years trying to tout the idea, it’s time to give up. >>>
    I already said, L4.

    The one that Hurd has been trying to use, without success.

    Has anybody else made production use of it?

    I already said in another message, about L3.

    This is L4 we’re talking about, not L3.
    --- Synchronet 3.20a-Linux NewsLink 1.114