Brendan wrote:I'm not sure, but I was thinking "hardware domains" were added so that the performance of single address space could be compared with the performance of multiple address spaces, and to allow "apples to apples" performance comparisons.
It's possible that they did it for that reason... it is a research project after all. However, the idea does seem generally useful IMO, "just in case"...
Brendan wrote:With every application in it's own hardware domain, you've got a micro-kernel again...
My original point was that it never stopped being a microkernel just because the isolation mechanism changed. But yes, with one SIP per domain it becomes like a conventional microkernel that uses hardware protection.
Brendan wrote:For overall performance difference, their macro-benchmarks are interesting. For the first test (compiling 165000 lines of code), full "micro-kernel" style hardware isolation performed better than software isolation with run-time tests.
Not surprising given that the test was mostly CPU-bound to one process. The fact that bounds checking isn't free has been known for a long time, but that's the price of avoiding problems like buffer overruns.
Brendan wrote:For the second test (reading 50000 files and doing nothing with the read data) they say software isolation had a far lower number of cycles, but the test itself would have been I/O bound and they don't say anything about total execution time (I'm guessing the total execution time of the second test depends on hard disk transfer times and little else).
My guess is that they were just trying to measure the IPC overhead.
Brendan wrote:The second test does show that the 80x86 TLB isn't very good, but people have been saying that for years - each TLB entry should be tagged with some form of address space identifier so that TLB entries don't need to be flushed during an address space switch. AFAIK other architectures do this, and strangely, AMD's hardware virtualisation also does this (but only for guest OSs).
Yes, these benchmarks would be really interesting on an architecture with a tagged TLB.
Brendan wrote:I have difficulty getting my head around the idea of a type-safe assembler - IMHO it'd be impossible to do while still calling it an assembler.
I probably should have said "assembly" not "assembler"... I'm thinking maybe they really meant machine code, since I see no reason to go from a binary representation of MSIL back to a textual representation of x86 code. Nevertheless, the acronymn they use is TAL (typed assembly language).
I'm sure I'm grossly oversimplifying, but here's how I imagine verification of typed assembly works. Each type defined in the program has a particular memory layout. The type information produced alongside the machine code describes all of these layouts and maps memory operands in the machine code to particular types. The verifier can then make sure that all memory accesses to each instance of a particular type do not stray outside the acceptible interpretation of its fields. Somehow it must also be able to tell when dynamic memory has been properly allocated by the garbage collector. I'm assuming it would be pretty straightforward to ensure that the stack is manipulated correctly.
Brendan wrote:Not sure if that's a fair comparison - you'd want to compare lines of code that need to be trusted.
That's what I'm saying -- you have to trust everything in the kernel in Windows (Linux too, although it doesn't include the GUI in there). The Singularity kernel is much, much smaller in comparison. I'm not sure how big the trusted code outside the kernel is, but I'm betting that discounting Bartok it's not that big, and the TAL verifier they come up with will probably be not much bigger than something like NASM (I would guess).
Brendan wrote:No - if the toolchain allows any form of unsafe operation to pass through undetected you're screwed (at least without the hardware protection domains where software isolation isn't used). As a very rough estimate, GCC plus GAS plus LD adds up to a fairly large amount of code (I'm not sure how the Bartok toolchain compares)...
Bartok is not exactly a full-blown compiler. It is an MSIL-to-x86 translator that also verifies the MSIL for type safety and does optimization. The output of Bartok is actually the only thing that needs to be verified in order for the software isolation to be guaranteed, and like I said, a verifier need not be that big. I really wish I could work on research like this... then I could give a firmer answer.