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=-0.3 required=5.0 tests=BAYES_00,FREEMAIL_FROM, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!aioe.org!.POSTED!not-for-mail From: anon@att.net Newsgroups: comp.lang.ada Subject: Re: seL4 as base of an AdaOS with some Spark proofing? Date: Wed, 30 Jul 2014 17:58:33 +0000 (UTC) Organization: Aioe.org NNTP Server Message-ID: References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com> Reply-To: anon@att.net NNTP-Posting-Host: exXD8pwmwxAA4niMP+pd6w.user.speranza.aioe.org X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 X-Newsreader: IBM NewsReader/2 2.0 Xref: number.nntp.dca.giganews.com comp.lang.ada:188050 Date: 2014-07-30T17:58:33+00:00 List-Id: seL4 is just another subset of the L4 project, which has nothing to do with Ada or an AdaOS. Now, there are a number of Ada OS projects which core code are based on the L4 project, like MaRTE (last update uses GNAT 2009), RTERMS (2008), and OpenRavencar (based on GNAT 3.13). For Ada purest, to do a AdaOS, like the one I an working on, the entire code must be written in Ada with exceptions for macros for assembly code (using the Ada Machine_Code package) that extents Ada API to allow hardware instructions, such as the CPU's I/O instructions. And some of these macros instructions include code used to switch the processor from initial 8/16 bit 8086 state (power up/reset) to a 32-bit protected mode and then detects and if possible switch to 64-bit mode during the boot phase. The AdaOS should be able to handle both 32-bit/64-bit code and maybe a some trusted special case protected VM code. As for languages, the OS should have Ada as the primary languages. If a secondary language is desired then it's compiler must be written in Ada. This means that others projects like openGL should be written in Ada instead of just porting the project code to the new AdaOS after a C compiler is written in Ada and then binding the code to the AdaOS. The AdaOS, also should be a stand alone system that can work within a virtualization environments with some small limitations caused by the VM engine unless the VM is also, written in Ada and the AdaOS is the host OS. Then there's the compiler while GNAT is an OK compiler it will not work for the new OS, we need a compiler from the ground up written in Ada that can produce code for a number of OS including an AdaOS that does not depends on any host OS or a design implementation like GNU which is based on C/C++. That way the new Ada compiler could be easily ported to the new OS without any other language or groups involvement. But just having an AdaOS will not increase the usage of Ada. This might change if and only if the AdaOS was a complete and robust OS that could go against Microsoft Windows and Apple's OS X. But most people writing an AdaOS normally stop after they finish the initial kernel. Which mean an AdaOS will never become robust enough to even equal any OS used today. much less compete with those OS. In <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>, kug1977@web.de writes: >Hi,=20 > >NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BS= >D). seL4 is the world's first operating-system kernel with an end-to-end pr= >oof of implementation correctness and security enforcement and claims to be= > the world's most highly-assured OS. > >As seL4 is written in C and some ASM and the proofing was done with Haskell= >, I asked myself: Can we use this kernel as a base to develop a real AdaOS = >with Spark to proof it's correctness? seL4 is a real microkernel, so it's n= >ot like porting Linux or Mach to Ada.=20 > >L4 has Real-Time capabilities, a capability based security system, Task and= > Threads, high speed IPC, so it might fit everything from embedded to serve= >r. With Genode (http://genode.org/) there's a test environment with differe= >nt kernels (incl. L4) and a tool chain, so we must not start from scratch.= >=20 > >Doing an OS in Ada / Spark, might attract some people to use Ada instead of= > C. And having an OS written in Ada, seems not only my dream. :-) > >-kug1977