Re: Unikernel / Ada

[Adrian-Ken Rueegsegger <ken@codelabs.ch>]

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