Unikernel / Ada

Unikernel / Ada

[volkert]

Some time ago read some Papers on the MirageOS (https://mirage.io/), a library operating system. The model works in short (simplified): The application sources  (in case of Mirage in OCaml) are compiled / linked together with all its depending "library os" sources into one fully standalone binary (unikernal). This  binary is then deployed directly f.e. on a Xen Hypervisor. No complex OS involved. small, efficient, more secure, fast to boot, 

https://mirage.io/wiki/overview-of-mirage

I find this model interesting for GNAT. Maybe there are already some ideas  around?

Volkert

Re: Unikernel / Ada

[Randy Brukardt]

That sort of thing was done a lot, especially in the early days of Ada.

Rational, for instance, had a bare-machine version of their compiler (the 
executable ran directly on the hardware with no outside kernel).

Indeed, all of the MS-DOS compilers could have been considered the same, as 
MS-DOS didn't provide much other than I/O support. Everything else (tasking, 
exceptions, storage pools, etc.) was in the Ada runtime. We used to sell an 
embedded kit that included the runtime source and tools for tailoring it to 
run in a bare machine environment.

For the most part, those things have disappeared, because of lack of demand. 
That's probably because modern software needs so much more I/O (you can't 
live with just an RS232 serial connection anymore) that some sort of I/O 
kernel is needed at a minimum. (I don't think I would want to start writing 
TCP/IP socket stacks :-). And with the rise of multi-core systems, CPU setup 
and management is gotten pretty hairy as well. That drives customers to 
using that kernel for everything.

My personal tendency is to use the target system for as little as possible 
(I don't have to trust -- or understand -- things I don't use!), but my 
understanding is (a) I'm unusual, and (b) I don't have customer pressure to 
do otherwise. The (b) factor is surely the most important, and that could 
change at any time.

Using Xen as the kernel is an interesting idea, but of course it changes it 
from a "hypervisor" to "just another kernel" which is running programs 
packaged individually. It's almost a full circle (and doesn't surprise me, 
because people are always trying to get rid of layers, and there aren't many 
new ideas out there).

                                    Randy.

<volkert@komponentenwerkstatt.de> wrote in message 
news:7023af9f-7429-448d-b290-03e0c32772f7@googlegroups.com...
Some time ago read some Papers on the MirageOS (https://mirage.io/), a 
library operating system. The model works in short (simplified): The 
application sources  (in case of Mirage in OCaml) are compiled / linked 
together with all its depending "library os" sources into one fully 
standalone binary (unikernal). This  binary is then deployed directly f.e. 
on a Xen Hypervisor. No complex OS involved. small, efficient, more secure, 
fast to boot,

https://mirage.io/wiki/overview-of-mirage

I find this model interesting for GNAT. Maybe there are already some ideas 
around?

Volkert

Re: Unikernel / Ada

[Niklas Holsti]

On 17-03-01 23:20 , Randy Brukardt wrote:
> That sort of thing was done a lot, especially in the early days of Ada.
>
> Rational, for instance, had a bare-machine version of their compiler (the
> executable ran directly on the hardware with no outside kernel).
>
> Indeed, all of the MS-DOS compilers could have been considered the same, as
> MS-DOS didn't provide much other than I/O support. Everything else (tasking,
> exceptions, storage pools, etc.) was in the Ada runtime. We used to sell an
> embedded kit that included the runtime source and tools for tailoring it to
> run in a bare machine environment.
>
> For the most part, those things have disappeared, because of lack of demand.

They are still the norm in my main domain -- on-board SW for satellites 
-- and I would expect also in any embedded SW on small machines, 
although Linux is making inroads.

AdaCore supplies a range of bare-board Run-Time Systems for GNAT Pro, 
from no-runtime through various levels of Ravenscar.

Having a standard Ada RTS (even if a subset) on the embedded target is 
very nice; it makes much of the SW portable between the target and the 
host workstations, with only a little HW simulation needed in the 
workstation environment.

> That's probably because modern software needs so much more I/O (you can't
> live with just an RS232 serial connection anymore) that some sort of I/O
> kernel is needed at a minimum.

In my domain the I/O is so special (typically MIL-1553 or SpaceWire 
transports, space-specific protocols) that a standard O/S I/O system 
would not be of much use.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Unikernel / Ada

[Simon Wright]

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

> AdaCore supplies a range of bare-board Run-Time Systems for GNAT Pro,
> from no-runtime through various levels of Ravenscar.

See https://github.com/AdaCore/embedded-runtimes for Ravenscar runtimes
for various ARM boards; there are small-footprint and full versions
('full' contains, for example, maths and exception support, but not
containers. Perhaps 'fuller' would be nearer the mark!).

Re: Unikernel / Ada

[Volkert]

A short quote from "Unikernels Beyond Containers to the Next Generation of Cloud-" Russell Pavlicek

"Unikernels promise small, secure, fast workloads, and people
are beginning to see that this new technology could help launch a
new phase in cloud computing. To put it simply, unikernels apply 
the established techniques of embedded programming to the datacenter."

BW,
Volkert


On Wednesday, March 1, 2017 at 10:20:13 PM UTC+1, Randy Brukardt wrote:
> That sort of thing was done a lot, especially in the early days of Ada.
> 
> Rational, for instance, had a bare-machine version of their compiler (the 
> executable ran directly on the hardware with no outside kernel).
> 
> Indeed, all of the MS-DOS compilers could have been considered the same, as 
> MS-DOS didn't provide much other than I/O support. Everything else (tasking, 
> exceptions, storage pools, etc.) was in the Ada runtime. We used to sell an 
> embedded kit that included the runtime source and tools for tailoring it to 
> run in a bare machine environment.
> 
> For the most part, those things have disappeared, because of lack of demand. 
> That's probably because modern software needs so much more I/O (you can't 
> live with just an RS232 serial connection anymore) that some sort of I/O 
> kernel is needed at a minimum. (I don't think I would want to start writing 
> TCP/IP socket stacks :-). And with the rise of multi-core systems, CPU setup 
> and management is gotten pretty hairy as well. That drives customers to 
> using that kernel for everything.
> 
> My personal tendency is to use the target system for as little as possible 
> (I don't have to trust -- or understand -- things I don't use!), but my 
> understanding is (a) I'm unusual, and (b) I don't have customer pressure to 
> do otherwise. The (b) factor is surely the most important, and that could 
> change at any time.
> 
> Using Xen as the kernel is an interesting idea, but of course it changes it 
> from a "hypervisor" to "just another kernel" which is running programs 
> packaged individually. It's almost a full circle (and doesn't surprise me, 
> because people are always trying to get rid of layers, and there aren't many 
> new ideas out there).
> 
>                                     Randy.
> 
> <volkert@komponentenwerkstatt.de> wrote in message 
> news:7023af9f-7429-448d-b290-03e0c32772f7@googlegroups.com...
> Some time ago read some Papers on the MirageOS (https://mirage.io/), a 
> library operating system. The model works in short (simplified): The 
> application sources  (in case of Mirage in OCaml) are compiled / linked 
> together with all its depending "library os" sources into one fully 
> standalone binary (unikernal). This  binary is then deployed directly f.e. 
> on a Xen Hypervisor. No complex OS involved. small, efficient, more secure, 
> fast to boot,
> 
> https://mirage.io/wiki/overview-of-mirage
> 
> I find this model interesting for GNAT. Maybe there are already some ideas 
> around?
> 
> Volkert

Re: Unikernel / Ada

[Adrian-Ken Rueegsegger]

Hi,

On 03/01/2017 07:52 PM, volkert@komponentenwerkstatt.de wrote:
> Some time ago read some Papers on the MirageOS (https://mirage.io/), a library operating system. The model works in short (simplified): The application sources  (in case of Mirage in OCaml) are compiled / linked together with all its depending "library os" sources into one fully standalone binary (unikernal). This  binary is then deployed directly f.e. on a Xen Hypervisor. No complex OS involved. small, efficient, more secure, fast to boot, 
> 
> https://mirage.io/wiki/overview-of-mirage
> 
> I find this model interesting for GNAT. Maybe there are already some ideas  around?

Funny you should mention MirageOS specifically. I have been toying
around with it over the past weekend and actually managed to run some
example scenarios as subjects on the Muen Separation Kernel [1]. I
posted a small teaser here [2].

Regarding Ada: we have published a few SPARK/Ada subjects that run
natively on Muen. Currently we only provide a zero-footprint runtime
which obviously restricts the language features one can use to write
native Ada/SPARK subjects. However, there is no inherent limitation, it
is simply a matter of extending the runtime.

Apropos of developing a TCP/IP stack from scratch: this might be of
interest [3].

Cheers,
Adrian

[1] - https://muen.sk
[2] - https://twitter.com/Kensan42/status/835941733359882240
[3] -
https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/ipstack

Re: Unikernel / Ada

[Dmitry A. Kazakov]

On 2017-03-01 22:39, Adrian-Ken Rueegsegger wrote:

> Apropos of developing a TCP/IP stack from scratch: this might be of
> interest [3].

Wow! Thanks for sharing the link.

> https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/ipstac

No plans for adding IGMP and PGM?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Unikernel / Ada

[Simon Wright]

Adrian-Ken Rueegsegger <ken@codelabs.ch> writes:

> https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/ipstack

The copyright/licensing status is odd; the README says (C) 2010,
AdaCore, but all the source says (C) 2010-2014, Free Software Foundation.
There's no visible license statement.

Re: Unikernel / Ada

[Volkert]

On Wednesday, March 1, 2017 at 10:39:25 PM UTC+1, Adrian-Ken Rueegsegger wrote:
> Hi,
> 
> On 03/01/2017 07:52 PM, volkert@komponentenwerkstatt.de wrote:
> > Some time ago read some Papers on the MirageOS (https://mirage.io/), a library operating system. The model works in short (simplified): The application sources  (in case of Mirage in OCaml) are compiled / linked together with all its depending "library os" sources into one fully standalone binary (unikernal). This  binary is then deployed directly f.e. on a Xen Hypervisor. No complex OS involved. small, efficient, more secure, fast to boot, 
> > 
> > https://mirage.io/wiki/overview-of-mirage
> > 
> > I find this model interesting for GNAT. Maybe there are already some ideas  around?
> 
> Funny you should mention MirageOS specifically. I have been toying
> around with it over the past weekend and actually managed to run some
> example scenarios as subjects on the Muen Separation Kernel [1]. I
> posted a small teaser here [2].
So a Mirage Unikernel runs on top of Muen.. Nice.

> Regarding Ada: we have published a few SPARK/Ada subjects that run
> natively on Muen. Currently we only provide a zero-footprint runtime
> which obviously restricts the language features one can use to write
> native Ada/SPARK subjects. However, there is no inherent limitation, it
> is simply a matter of extending the runtime.
> 
> Apropos of developing a TCP/IP stack from scratch: this might be of
> interest [3].
Interesting. In Mirage they create a set of basic "service from scratch (filesystem, network, DHCP, DNS, WebServer, Terminal). All in OCaml.

See:
https://github.com/mirage/mirage-skeleton
https://github.com/mirage/mirage

I thought this was always the idea of Safe/Secure Ada to create a full stack build on a "sound foundation". I think that is also a goal of Muen, for highly secure systems.     

Btw. the company behind MirageIO is now part of docker, see: http://unikernel.com


Volkert



 
> Cheers,
> Adrian
> 
> [1] - https://muen.sk
> [2] - https://twitter.com/Kensan42/status/835941733359882240
> [3] -
> https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/ipstack

Re: Unikernel / Ada

[Paul Rubin]

volkert@komponentenwerkstatt.de writes:
> https://mirage.io/wiki/overview-of-mirage
> I find this model interesting for GNAT. Maybe there are already some
> ideas around?

No idea about GNAT, but there are similar setups for Haskell (halvm.org)
and Erlang (ErlangOnXen.org).  There may be other things like that too.