FYI: microkernel.info community site

[Jakub Jermář]

Hello,

just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.

Thanks,
Jakub

[1] http://microkernel.info
[2] http://unikernel.org/projects/
[3] https://github.com/jermar/microkernel.info

[Gernot Heiser]

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

Gernot

Post by Jakub Jermář
Hello,
just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.
I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.
Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.
Thanks,
Jakub
[1] http://microkernel.info
[2] http://unikernel.org/projects/
[3] https://github.com/jermar/microkernel.info
_______________________________________________
Devel mailing list
https://sel4.systems/lists/listinfo/devel

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

[Alexander Senier]

Hi Gernot,

when analyzing the statement carefully, you'll find that it's indeed
true. The seL4 source was *open-sourced* in July 2014 whereas the Muen
source was released in August 2013.

But of cause you're right, we're not talking about the same properties here.

Cheers,
Alex

Post by Gernot Heiser
Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “
We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

--
Dipl.-Inf. Alexander Senier
Scientific Assistant

TU Dresden
Faculty of Computer Science
Institute of System Architecture
Chair of Privacy and Data Security
01062 Dresden

Tel.: [phone]
Fax : [phone]

[Gernot Heiser]

Post by Alexander Senier
when analyzing the statement carefully, you'll find that it's indeed
true. The seL4 source was *open-sourced* in July 2014 whereas the Muen
source was released in August 2013.
But of cause you're right, we're not talking about the same properties here.

… and even the above is at best of historical relevance.

Gernot

[Martin Stein]

Hi Jakub,

I really like the idea and implementation of this website. Having a
place that provides an overview of the Microkernel movement as a whole
may help to lower the barriers for outstanding people to get in touch
with it. Maybe it also helps to keep events like the FOSDEM devroom going.

Cheers,
Martin

Post by Jakub Jermář
Hello,
just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.
I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.
Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.
Thanks,
Jakub
[1] http://microkernel.info
[2] http://unikernel.org/projects/
[3] https://github.com/jermar/microkernel.info
------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785111&iu=/4140
_______________________________________________
genode-main mailing list
https://lists.sourceforge.net/lists/listinfo/genode-main

[Vasily A. Sartakov]

Greetings

this is a good initiative, I like it.

Also, it seems to me, the content of the site can be enhanced by getting-started matherials of relevant projects, or (I prefer), MOOC project about microkernels with basics, history, architectures and examples based on different projects. Also, the final (graduate) practice of this project could be participation in GSOC or just resolving important issues in bug trackers. In my opinion, such course should be sufficient to turn any systems-friendly developer (student) to microkernel practitioner/developer/enthusiast capable to solve engineering issues of open source projects.

Several years ago we recorded some lectures bout the L4Re and Genode (Thanks Bjoerd, Norman, Udo):

https://www.youtube.com/channel/UCwBjjt60Mmp9X3N71mba3GQ

And of course there are many addition materials in any other projects, so, I do not think that it will be complicated to make joint course.

Finaly, about the diffusion of microkernels, I think it is important to see how all (and other) projects can be used to solv actual issues, thus, examples of application could also enchance the content (and impact) of the site.

Post by Jakub Jermář
just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.
I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.
Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.

--
Vasily A. Sartakov
***@ksyslabs.org

[Jakub Jermář]

Hi Vasily,

Post by Vasily A. Sartakov
this is a good initiative, I like it.
Also, it seems to me, the content of the site can be enhanced by getting-started matherials of relevant projects, or (I prefer), MOOC project about microkernels with basics, history, architectures and examples based on different projects. Also, the final (graduate) practice of this project could be participation in GSOC or just resolving important issues in bug trackers. In my opinion, such course should be sufficient to turn any systems-friendly developer (student) to microkernel practitioner/developer/enthusiast capable to solve engineering issues of open source projects.
https://www.youtube.com/channel/UCwBjjt60Mmp9X3N71mba3GQ
And of course there are many addition materials in any other projects, so, I do not think that it will be complicated to make joint course.
Finaly, about the diffusion of microkernels, I think it is important to see how all (and other) projects can be used to solv actual issues, thus, examples of application could also enchance the content (and impact) of the site.

Yes, the site can be definitely enhanced to contain more useful stuff
such as tutorials, papers, blog entries and microkernel news. It could
also serve as a basis for a prospective microkernel umbrella
organization for the various summer of code programs and also the
Microkernel devroom at FOSDEM in order to maximize chances of being
accepted.

Focusing on the web site's content for now, I've already merged PR's of
several people and am willing to continue within, including the creation
of a menu and subpages for the above content as soon as it appears.

Jakub

Post by Vasily A. Sartakov

Post by Jakub Jermář
just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.
I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.
Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.

--
Vasily A. Sartakov
_______________________________________________
Devel mailing list
https://sel4.systems/lists/listinfo/devel

[Martin Vahi]

I do not know anything about the XstratuM

http://www.xtratum.org/

I just found it, but it seems that unlike
Muen, it is under GPL version 2, not version 3,
which means that it can be used for aggregate
works that do not link to it without putting
the rest of the parts under GPL. Just like
the ordinary Linux kernel can be used for
running proprietary software without
affecting the license of the proprietary software.

The way I understand, the GPL v3 is infectious
even, when linking is not done.

The XstratuM seems to be some European Space Agency
project. I haven't studied the source, but at first
glance it seems to be written in C, not Ada, which
means that the de facto proprietary (GPL v3) AdaCore
Ada implementation, the only thoroughly maintained
Ada implementation (id est from commercial
development point of view Ada is de facto
proprietary programming language) a truly open,
non-proprietary language can be used. Add to that
the fact that formal verification tools for C and C++
tend to become more available,

http://frama-c.com/

http://mbeddr.com
https://github.com/mbeddr

the parties, who are not as loaded (with money)
as the military-industrial complex is, might also
have a chance.

Thank You for reading my letter. :-)

Regards,
***@softf1.com

[Adrian-Ken Rueegsegger]

Hi Martin,

Post by Martin Vahi
I just found it, but it seems that unlike
Muen, it is under GPL version 2, not version 3,
which means that it can be used for aggregate
works that do not link to it without putting
the rest of the parts under GPL. Just like
the ordinary Linux kernel can be used for
running proprietary software without
affecting the license of the proprietary software.

The license of the Muen kernel and the Muen toolchain is indeed GPLv3
but this does *not* cover components or subjects running on top of the
Muen Separation Kernel. A note clarifying the intent is part of the
projects COPYING file, see [1]. It is similar in spirit to the note in
the Linux COPYING file [2] but we made it very explicit in an attempt to
avoid any confusion.

Thus it is perfectly possible (and legal) to develop closed-source
software that runs as a component/subject on top of the Muen kernel. We
are also careful when choosing licenses for libraries that may be
re-used by other parties, e.g. the shared memory channel library
'libmuchannel' is licensed under BSD [3].

We chose the GPLv3 for the Muen project so the community can benefit
from development of the kernel and the toolchain.

Post by Martin Vahi
The XstratuM seems to be some European Space Agency
project. I haven't studied the source, but at first
glance it seems to be written in C, not Ada, which
means that the de facto proprietary (GPL v3) AdaCore
Ada implementation, the only thoroughly maintained
Ada implementation (id est from commercial
development point of view Ada is de facto
proprietary programming language) a truly open,
non-proprietary language can be used.

The Ada compiler GNAT is and has been part of GCC, which is distributed
by the Free Software Foundation, for quite some time [4]. To quote [5]:

The compiler is licensed under the terms of the GNU GPL 3+ with GCC
Runtime Library Exception.

So, I fail to see how you arrive at the conclusion that Ada is a "de
facto proprietary programming language".

Post by Martin Vahi
the parties, who are not as loaded (with money)
as the military-industrial complex is, might also
have a chance.

The home of the Muen Project is the University of Applied Sciences HSR
[6] in Rapperswil, Switzerland which is clearly not part of any
military-industrial complex ;)

Post by Martin Vahi
Thank You for reading my letter. :-)

Frankly, I was a bit surprised by your email, as we have discussed the
Muen license in a private email conversation several months ago where
you indicated that I was able to clarify the situation to your
satisfaction. If you have further questions about this topic feel free
to pick up our earlier conversation or ask questions on the Muen project
mailing list [7].

Cheers,
Adrian

[1] - http://git.codelabs.ch/?p=muen.git;a=blob;f=COPYING
[2] -
https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/COPYING
[3] -
http://git.codelabs.ch/?p=muen.git;a=blob;f=components/libmuchannel/COPYING
[4] - https://gcc.gnu.org/wiki/GNAT
[5] - https://en.wikipedia.org/wiki/GNAT#License
[6] - https://www.hsr.ch/
[7] - https://groups.google.com/group/muen-dev