I was dissatisfied with Linux and FreeBSD, seL4 seems much more robust, in terms of system reliability and security. (seL4 is not an OS, but a framework to build an OS on top.)
Then I was dissatisfied with all the crap in the x86 ISA (bucket of modes, 4 rings, many deprecated features, insecure SMM and zillions of feature flags), the mostly failures of RISC and the over complexity of many versions and variants of ARM (but it’s nice that it’s available as IP).
It seems there ought to be an architecture that can make writing OSes easier and more secure:
- handle task/context switching much faster than x86
- IPC (zero-copy both register and page borrowing, maybe copy if source page is locked or if async.) This enables L4-fast CSP in the ISA.
- resource limits / counters
- memory page allocation
- capabilities management
- transparent page compression and encryption
- OS bookkeeping (kernel-specified privileged data: per task/core/etc.)
in addition to the usual suspects (MMU, FPU, SIMD, etc.):
- virtual memory
- paging (including possible unprivileged page-fault handler)
- hypervisor (VM lifecycle)
- interrupts / faults / exceptions
- TLB
- tiers of caches / cache coherency protocol
- memory controller
- standard I/O controllers
- clock throttling w/ spread-spectrum and thermal management
- micropower standby
- JTAG
- at least one system-wide atomic operation (compare&swap or ainc/adec)
much more rigidly, faster and less clunkily that most OS gunk tends to be. Not CISC overload, but healthy facilitation of fast AND secure OS and user-mode program constructs that are batteries-included.
Also, SystemVerilog looks doable (I’m reading the whole IEEE spec for SV2012) and there’s always MOSIS should a Kickstarter be in order to make actual ASIC dev kits. EDA looks manageable but there’s a definite learning curve to testing, verification, behavioral design, RTL and DRC.
Plus, opaque firmware blobs and chips aren’t conducive to trusting the end-to-end security of the supply chain of a finished product. End customers are almost praying that some fab hasn’t slipped in malicious microcode or RTL changes or the parts stuffers didn’t insert a backdoor into unsecured firmware.