From 238c43499c4e08562024c3ef59e50aa365b5f1b2 Mon Sep 17 00:00:00 2001
From: Thomas Schwinge <thomas@schwinge.name>
Date: Tue, 7 Dec 2010 14:26:40 +0100
Subject: Some bits about L4 and Coyotos.

---
 microkernel/coyotos.mdwn | 30 ++++++++++++++++++++++++++++++
 microkernel/l4.mdwn      | 21 +++++++++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 microkernel/coyotos.mdwn
 create mode 100644 microkernel/l4.mdwn

(limited to 'microkernel')

diff --git a/microkernel/coyotos.mdwn b/microkernel/coyotos.mdwn
new file mode 100644
index 00000000..5ecea688
--- /dev/null
+++ b/microkernel/coyotos.mdwn
@@ -0,0 +1,30 @@
+[[!meta copyright="Copyright © 2006, 2007, 2008, 2010 Free Software Foundation,
+Inc."]]
+
+[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable
+id="license" text="Permission is granted to copy, distribute and/or modify this
+document under the terms of the GNU Free Documentation License, Version 1.2 or
+any later version published by the Free Software Foundation; with no Invariant
+Sections, no Front-Cover Texts, and no Back-Cover Texts.  A copy of the license
+is included in the section entitled [[GNU Free Documentation
+License|/fdl]]."]]"""]]
+
+[[!meta title="Coyotos"]]
+
+[*Coyotos*](http://www.coyotos.org/) is a microkernel and OS and the successor
+of [[EROS]], that itself is the successor of [[KeyKOS]].  A more complete
+history can be found [here](http://www.coyotos.org/history.html).  Its main
+objectives are to correcte some shortcomings of [[EROS]], demonstrate that an
+atomic kernel design scales well, and (eventually) to completely formally
+verify both the kernel and critical system components by writing them in a new
+language called [bitc](http://www.bitc-lang.org/).
+
+Coyotos is an orthogonally [[persistent|persistency]] pure [[capability]]
+system.  It uses [[continuation]]-based unbuffered asynchronous [[IPC]]
+(actually it's synchronous [[IPC]] with asynchronous [[system calls]]).
+
+TODO: explain these terms and (more important) their consequences on system
+design.
+
+The coyotos microkernel specification can be found
+[here](http://www.coyotos.org/docs/ukernel/spec.html).
diff --git a/microkernel/l4.mdwn b/microkernel/l4.mdwn
new file mode 100644
index 00000000..970407be
--- /dev/null
+++ b/microkernel/l4.mdwn
@@ -0,0 +1,21 @@
+[[!meta copyright="Copyright © 2004, 2006, 2007, 2008, 2010 Free Software
+Foundation, Inc."]]
+
+[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable
+id="license" text="Permission is granted to copy, distribute and/or modify this
+document under the terms of the GNU Free Documentation License, Version 1.2 or
+any later version published by the Free Software Foundation; with no Invariant
+Sections, no Front-Cover Texts, and no Back-Cover Texts.  A copy of the license
+is included in the section entitled [[GNU Free Documentation
+License|/fdl]]."]]"""]]
+
+The [*L4* microkernel](http://l4ka.org/) is an attempt to create a very small
+high performace core which provides basic memory management, task and context
+switching, and little else.
+
+[L4Ka Pistachio Home](http://l4ka.org/projects/pistachio/).
+
+See [l4.verified](http://nicta.com.au/research/projects/l4.verified) for work
+on formally verifying an L4 microkernel.
+
+There was a GNU/Hurd [[history/port_to_L4]], which is now stalled.
-- 
cgit v1.2.3