From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Adrian-Ken Rueegsegger <ken@codelabs.ch>
Newsgroups: comp.lang.ada
Subject: Re: Unikernel / Ada
Date: Wed, 1 Mar 2017 22:39:24 +0100
Organization: A noiseless patient Spider
Message-ID: <o97eun$d6$1@dont-email.me>
References: <7023af9f-7429-448d-b290-03e0c32772f7@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 1 Mar 2017 21:37:27 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="04e39a1858aa707cbfe58f7ad1c331fb";
	logging-data="422"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19HEV8O/UxA6WTi7+dVDkmh"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Icedove/45.6.0
In-Reply-To: <7023af9f-7429-448d-b290-03e0c32772f7@googlegroups.com>
Cancel-Lock: sha1:wVY+eEYhC+J11q2PRUfaoOpvdJY=
Xref: news.eternal-september.org comp.lang.ada:33446
Date: 2017-03-01T22:39:24+01:00
List-Id: <comp.lang.ada>

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