summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorpjrm <pjrm@web>2008-09-22 05:44:55 +0000
committerGNU Hurd wiki engine <web-hurd@gnu.org>2008-09-22 05:44:55 +0000
commit3b44aa0aa790cc501f15308f4d5b86c97f0ab0b6 (patch)
tree89b02d4a1972d3afcecc65e11f2874c1366777bb
parentbb896d18594fe9f3176fe9b5cc12bd841794ffdd (diff)
Add link to L4 verification. (Feel free to move to a better page, e.g. up a level once it has some other text.)
-rw-r--r--hurd/ng/microkernelcoyotos.mdwn2
1 files changed, 1 insertions, 1 deletions
diff --git a/hurd/ng/microkernelcoyotos.mdwn b/hurd/ng/microkernelcoyotos.mdwn
index 40fd6e9d..e6b2fe8e 100644
--- a/hurd/ng/microkernelcoyotos.mdwn
+++ b/hurd/ng/microkernelcoyotos.mdwn
@@ -1,6 +1,6 @@
# <a name="The_Coyotos_microkernel"> The Coyotos microkernel </a>
-[Coyotos](http://www.coyotos.org/index.html) 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). It's main objectives are to correcte some shortcomings of EROS, demonstrate that an atomic kernel design scales well and to completely formally verify both the kernel and critical system components by writing them in a new language called bitc.
+[Coyotos](http://www.coyotos.org/index.html) 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. [See [l4.verified](http://nicta.com.au/research/projects/l4.verified) for work on formally verifying an L4 microkernel.]
Coyotos is an orthogonally persistent pure capability system. It uses continuation based unbuffered asynchronous IPC (actually it's synchronous IPC whith asynchronous syscalls).