152 comments

[ 2.8 ms ] story [ 232 ms ] thread
[flagged]
This is quite harsh for a repo explicitly created to experiment with non-Unix OS ideas. It is an experiment, it doesn't have to e useful.

Personally, I enjoy when people post things like this as it helps me learn.

See also:

- Experimental

- OS

Ain't no body going to use your OS generally speaking.

This is so cool.

Particularly enjoyed:

    In Fomos, an app is really just a function. There is nothing else ! This is a huge claim. An executable for a Unix or Windows OS is extremely complex compared to a freestanding function.
I can't even begin to imagine how cool a kernel would be written this way.

Correct me if I'm wrong, but I think this is how smalltalk/squeak works?

I hope the author continues with this project. File system, task manager, safe memory stacks, nice resource sharing, ...

... and of course, running DOOM as a minimum proof of concept requirement! /s.

What’s the difference in practice compared to every other OS where app is just a “int main() { … }” function?
Make two apps A and B with their respective main() functions. Add some function foo() to app A. Now try to call A's foo() from B's main(). How many hoops do you need to jump through in every other OS to do this?
The amount of (wonderfully) horrible doors this opens is awesome.
None, because this exists outside the scope of an operating system. This is the domain of an executable/linkage format and language compiler.
Maybe the complexity lies in that possessive qualifier "A's foo()" - if this foo() can manipulate the callee state in some other virtual memory domain then it might not be sufficient to link against it in B's application.
Not many hoops, why?

    /* Create function pointer of appropriate type, initialised. */
    int(*foo)(int, int) = NULL;
    
    int main()
    {
        void * ha;
        
        if ((ha = dlopen("A", RTLD_LAZY|RTLD_NODELETE)) != NULL) {
            foo = dlsym(ha, "foo");
            dlclose(ha);
        }
        
        /* if "foo" is non-NULL you can call it now. */
        
        ...
If you control the development of both A and B apps, then not so many. But generally you are not expected to load symbols from another application, you are expected to either use various IPC mechanisms or load symbols from a shared library instead of touching another application at all.
I'd suggest reading the linked readme, it does a great job explaining the differences. In other operating systems apps do dynamic linking & syscalls. Those don't exist in Fomos.
In a regular OS there would be a bunch of implicit things provided by the OS that the app can access, while in this OS those things are explicit in the context.

But I don’t think that’s really that significant… you could, e.g., enumerate all the implicit things the OS provides, express them in a structure, and now you’ve got your explicit context. The “fomos” context is only as simple as it is because the OS provides a small number of simple things. Expand those to full OS capabilities and the context will get full OS complex.

The odd thing about this “OS” is that a running app is just the start function called repeatedly in a loop. This makes one app call a single coherent slice of app execution. That’s kind of interesting, but makes this pretty limited. E.g., it looks like apps are entirely cooperative. It’s maybe more of a cooperative execution environment.

Maybe it would be good for some embedded uses?

My takeaway was that compared to a dynamically linked binary, you don't need to literally patch it to get the correct addresses.

So you get the benefits of simplicity of a static binary and the size benefit of a dynamically linked binary.

Well that's the way I understood it anyway.

> What’s the difference in practice compared to every other OS where app is just a “int main() { … }” function?

Your premise is wrong: in, say, Windows or GNU/Linux an application is, say, a PE/COFF or ELF executable, both non-trivial file formats. The int main(...) function in C is just a very leaky abstraction of all this.

As opposed to what? Code that can be directly loaded into memory with no headers? That's how .COM files worked.

There is no such thing as "program is just a function" unless it's compiled with the OS, like on some microcontrollers. For programs residing on storage, the OS needs a way to load them into memory along with its resources which means it needs to read some kind of format, even if it's trivial.

But you can separate the file format of the executable from the loading process, i.e. implement "doing what the OS loader does" on your own. This way, you can define your completely own executable format instead of being forced to use the one that your OS wants you to use, or even decide that it doesn't have to be a file format (e.g. stream the data from a network stream).
I think you're making a wrong assumption about how this OS works, its programs are still loaded from ELF executables, the parser is here: https://github.com/Ruddle/Fomos/blob/91cf732f173a01cdec3df43...

The "app is a function" distinction is simply about the `Context` struct passed it, otherwise it loads and runs executables as expected (load ELf memory segments in, jump to entrypoint)

Edit: I guess I'd also add that on Linux or other OSs it's possible to construct and run process completely from memory with no on-disk executable file. JIT compilers do effectively this, the produce the executable code completely in memory and run it.

> I guess I'd also add that on Linux or other OSs it's possible to construct and run process completely from memory with no on-disk executable file.

This is rather likely true. But since writing such code is much harder than, say, writing FizzBuzz, I assume that somewhere in the OS code, a "wrong" abstraction is used which makes this task far too complicated.

Why do you assume it's complicated? It's not hard, it's actually very straight forward. The hard part is generating the executable code in the first place (if you're not reading it out of an executable file).

I'm not really sure what you're looking for or expecting unless you want the OS to compile your code for you (which this OS doesn't do either).

>Correct me if I'm wrong, but I think this is how smalltalk/squeak works?

In Smalltalk those would be classes' methods rather than freestanding functions, but yes: all objects within the image directly send messages to each other, i.e. invoke each other's methods. Lisp machine operating systems are somewhat closer, since initially they had no object system and used freestanding functions calling each other, though later they became generic functions specialized to their arguments' classes.

Reminds me of TempleOS, where all programs run in the same address space. Is this the same concept here?
Ironically, there are so many pointers at this point that OSes often now do use a single address space for every program (with escape hatches in case you need aliasing).

Virtual memory and vtables are now more about access control than about managing the scarcity of pointers.

Can you provide any citations for this (extraordinary, if true) claim? My knowledge of operating systems (which is based on experience in designing toy ones, but also studying other operating systems) suggests this is not the case on at least windows, macOS and linux. Feel free to correct me if I am wrong however!
One thing that appears to me would be that you could still 'pipe' output from one command to another, BUT the data would not be copied from one part of the pipeline to another.

I would imagine it could greatly speed up composable things like that...

Well it would have to be for memory safety purposes, unless it would specifically be designed to allow siblings application to share the memo... Ugh that would lead to a very unsafe system and that would defeat the purpose of writing safer code in Rust!
Run old school classic MacOS.
Oh, no, you're right. That's classic MacOS development. It calls you for each event, and you can't block. It sucked.
It was fun sometimes to “recover” a crashed environment by going into the hardware interrupt console and forcing the program counter to the entry point address of the Finder and then hoping for the best with your corrupted machine state.
> *In Fomos, an app is really just a function. There is nothing else ! This is a huge claim.*

To me this just screams the curse of greenfield development, where the architects are yet to discover what led other OSes to require all things they missed.

My expectation: Either Fomos has no security boundaries, or the security boundary looks a lot like syscalls...
Would be interested to hear the plans for security in more detail.

But in general I think these types of experiments show that operating systems could be improved with greenfield designs.

Reminds me a tiny bit of Mirage OS. https://mirage.io/

It's a cool idea, was just thinking if a program is just a function, can I just replace any function with a malicious code acting as dependency of another function? Or how would I require a specific function through signature? I guess me as a developer working on Fomos, would have to declare fully qualified dependencies in a manifest and then be able to call by function name my dependencies in my code? But then what about versioning? Do I have to bundle in my app all my dependencies? But cool idea
I'm not following. How does program-as-a-function matter in this regard? Isn't it a question of security and permissions? In most operating systems, compilation, linking, and run-time libraries determine dependencies. (I don't know how much of this will differ in something like Fomos.)
Probably you're right, it's about the same thing as it is now. I was thinking in this terms: If a program A depends on a function D, this function is another program D, when I run program A, it looks for function D, now normally in compile time I have a full path to dependency, now instead a system has a set of functions running, let's say that one of those is function D, how do I ensure as a user that function D is not mimicking something it is not? And I guess it's the same of right now, just make sure to don't run malicious software, but I was also thinking that probably it could be much harder to track programs as functions reusable from other functions(apps)
The specific mechanisms are key to understanding. Your question prompted me to review the details of how system calls and linking works in Linux and think about it in a broader context.

Programming languages also have considerable variation when it comes to dependency management. There is a menu of options w.r.t. symbol lookup and dispatch, ranging from static to dynamic.

I’ve mostly been an application level developer. Something interesting about OS development is system function calls behave differently when called in different contexts (privilege levels, capabilities). One mechanism in play is dynamic dispatch. The end effect is that the underlying details of a system call can be quite different for different callers.

(The Unison language has some innovative ideas IMO.)

If you come across a good resource that covers these topics as a “design menu” across different OS styles and/or a historical look at security mitigations (as opposed to only a summary of what is used now in Linux), could you share it?

I'm not sure you can be an exokernel and cooperatively scheduled. The only thing an exokernel does enforce multiplextion boundaries on hardware resources. Yeah, it'll be six of one in a lot of IO bound workloads, but IO bound workloads aren't the only kind of CPU workloads.

And to be fair, exokernels are probably one of the least understood forms of kernel. I feel like professors/textbooks/papers are legally required to explain the concept poorly.

> In Fomos, an app is really just a function. There is nothing else ! This is a huge claim. An executable for a Unix or Windows OS is extremely complex compared to a freestanding function.

I'm curious what Fomos uses as a distinction between "process" and "executable."

On Linux a "process" is the virtual address space (containing the argv/envp pointers, stacks, heap, signal masks, file handle table, signal handlers, and executable memory) as with some in-kernel data (uid, gid, etc) that determine what resources it is using and what resources it is allowed to use.

An "executable" is a file that contains enough bits for a loader to populate that address space when the execve syscall is performed.

One of the distinctions is that you do not need an executable to make a process (eg, you can call clone3 or fork just fine and start mucking with your address space as a new process) and while the kernel uses ELF and much of the userspace uses the RTLD loader from GLIBC you don't need to use either of these things to make a process in a given executable format.

And finally, a statically linked executable without position independent code is "just a function" in the assembler sense, with just enough metadata to tell the kernel's loader that's what it is. But without ASLR to actually resolve symbols at runtime, it's vulnerable to a lot of buffer overflow attacks if the addresses of dependency functions are known (return to libc is one of those, but it's not unique).

I'm the first to point out the flaws in glibc and want an alternative to the Posix model of processes (particularly in the world where the distinction between processes, threads, and fibers is really fuzzy and that is clear even within Linux and Windows at the syscall level), but I'm curious what is going on in Fomos. Most of the complexity in "executables" in Unix is inherent (resolving symbols at runtime is hard, but also super useful, allowing arbitrary interpreters seems annoying, but is one of the strengths of Linux over Windows and MacOS, providing the kernel interface through stable syscalls is actually the super power of Linux and a dynamic context either through libc or a vtable to do the same thing is not that great, etc).

Thinking about it for a few more minutes, one thing that I think is the great mistake is a homogenization of executable formats (everything on Mac is Mach-O, everything on Windows is PE, everything on Linux is ELF, etc). There's no reason we can't have a diverse ecosystem of executable/linkage formats - and an OS with a dirt simple model for loading in code is a great place for that.
What would be gained by making more different formats? Also #!/bin stuff is executable in sense and the most files in Windows that have default application set.

Dirt simple model works until it doesn't. Without address space separation there is no safety between executables and cooperative scheduling is the same. Running faulty binary or simply bit flip in ram can crash the whole system instead of just that process.

I mean there's value in being able to grok it without having read "Linking and Loading" and we don't want an Asimov scenario (I can't remember if this is Foundation or the Last Question) where we just truck on assuming things work without understanding how they work. And there's a lot of arcane knowledge in executable formats buried in mailing lists and aging/dying engineers on how and why decisions about these formats were designed.

"How does loading work" has a simple answer: you map the executable into virtual memory and jump to the entry point. But the "why does XYZ format do this to achieve that" has a lot of nuance and design decisions - none of which are documented. Particularly things like RTLD, which is designed heavily around the design of glibc and ELF, while the designer of the next generation of AOT or JIT compiled languages for operating systems with capability based models for security might want to understand before they design the executable format and process model that may deviate from POSIX.

There's space for design and research there, and a platform that makes that easy has a lot of value. While I would encourage the designer of such a platform to read the literature and understand why certain things are done the way they are, it's valuable to question if those reasons are still valid and whether or not there's a better way.

> I can't remember if this is Foundation or the Last Question

Foundation. The Galactic Empire makes use of atomic energy and other technologies that were created in the distant past and the technicians can only (sometimes) repair but not create. 'The Last Question' has a question that remains unanswered throughout human history, which isn't quite the same thing.

> providing the kernel interface through stable syscalls is actually the super power of Linux

I thought that it was drivers? Linux isn't particularly unique for having a stable abi (and the utility of such a decision is highly questionable). The driver support however is extraordinary and undeniable.

Did you take a look on how Zircon (Fuchsia) is handling this? It is quite interesting.
This looks very interesting, but it wasn't clear to me how to run this, in particular, how the demo at the top of the README was run.

Does this repo build a standalone OS the runs on a bare machine, or does it run in a VM like QEMU, or is it a Rust application program that runs hosted on a conventional OS?

> The argument that a cooperative scheduling is doomed to fail is overblown. Apps are already very much cooperative. For proof, run a version of that on your nice preemptive system : [pathological example which creates tons of threads and files]

The example is just too contrived. On a preemptive OS, apps typically hang in ways that don't turn the whole thing cooperative (thread deadlock, infinite loop, etc.). Also, a preemptive system could kill an app if it creates too many threads, files, or uses too much RAM, long before it gets effectively cooperative. Our systems are just more permissive.

> [Sandboxing] comes free once you accept the premises.

and yet

> any app can casually check the ram of another app ^^. This is going to be a hard problem to solve.

So no, sandboxing doesn't come for free.

That said, it's a cool idea and I wish the author success!

In browser land, all open sites share the memory of the browser heap, and there’s no crosstalk at all. I think the way out of that particular issue is creating a closure around the function (application) that effectively acts like the application’s own context. What if an app could open an app? Or put another way, what if an app could be an OS to another app?
There’s no cross talk because you can’t peek / poke arbitrary pointers in javascript. But you can in Rust.

And even then, I think modern browsers still isolate each tab in a separate process just to be safe. I don’t think they share memory.

The example is even more contrived because it assumes all systems have terrible sandboxing like Windows and Linux.

Any system competently designed for robust sandboxing would have limits for all resources and reject requests when the limit is reached.

> Apps do not need a standard library, any OS functionality is given to the app through the Context.

Don't need I can follow. But some apps will have dependencies -- some might even be tantamount to a standard library in other OSes. The Context provides all that too?

> How do you sleep, or wait asynchronously ? Just return;

This is a bit strange. I would think async I/O in the style of io_uring would be fantastic but this kind of model seems to rule out anything like that. That’ll make it hard to get reasonable perf. It’s also strange to not support async as it’s a natural suspension point to hook into but you would have to give up a lot of the design where your application state has to be explicitly saved / loaded via disk if I’m not mistaken. Seems pricy. Hopefully can be extended to support async properly.

In a similar vein, I suspect networking may become difficult to do (at least efficiently) for similar reasons but I’m not certain.

If I had to guess, something like async IO would be implemented by updating the context with the IO request and returning, and then your function would be called when it is ready. The function appears to me to be the end of an event loop that receives an arbitrary state in the parameter, so it should be able to generalize to anything an event loop would do.

You give up the language-level support for coroutines and async, though...

Author here. Your guess is correct. An app is its own callback. It might be possible to write an small app-level executor to get back those sweet language-level support for async though.
Now add DOM and HTML parsing and you'll have a web browser
Can someone explain to me what FB in the Context does?

it's... an array of pixels? does that imply all apps must draw themselves?

or ask other apps to draw for them.
Sounds like it's a framebuffer, and yes the apps draw themselves.

Looking at the source code of the cursor app [0], we can see it draws the mouse cursor and skips the rest. The transparent console app [1] is doing something more complicated which I haven't tried to fully understand, but which definitely involves massaging pixels and even temporarily saves pixel data in ctx.store.b1 and ctx.store.b2 so it looks like some kind of double buffering.

  [0]: https://github.com/Ruddle/Fomos/blob/cba0460af59e63f46c7646f8a2f29d574ff0d722/app_cursor/src/main.rs#L75
  [1]: https://github.com/Ruddle/Fomos/blob/cba0460af59e63f46c7646f8a2f29d574ff0d722/app_console/src/main.rs#L384
> The transparent console app [1] is doing something more complicated which I haven't tried to fully understand, (..)

If apps draw themselves, and transparency is involved, this could need:

a) Save background which is overwritten ("damage areas" is a modern description, I think?).

b) Alpha blending - calculating a weighed average between background & what you're overwriting it with.

c) And maybe some kind of text-buffer -> bitmap conversion (if not done ahead of time).

Enough pixel massaging right there.

Does this mean that apps that don't want/need to be visual are still burdened with it?
The "sandbox" is just some compile time check. As soon as you play with raw pointers, everything breaks down.

A good experiment, but nothing useful. Maybe the author can generate some new ideas from this.

Fear of missing out system?
I'm glad I'm not the only one who read it like that.
So there is no "kernel space and user space"? Then how to protect apps, like prevent bad app read other app's user password with pointer calculation.
As per the readme, security is not implemented yet.
Well there is also that small issue that implementing security for this design is pretty much impossible without destroying performance and end result is quite standard operating system.

Polling style scheduling will just be so slow if calling each executable always involves context switch. And then cooperative scheduling isn't really possible if some process doesn't play nice.

i guess, that since each app is a function, each app only has access to the parameters it was called with.
The next logical step would be to only support wasm programs ;)
I’m terms of cooperative multitasking I suspect this is not the same as what we had in Classic MacOS in the sense that we now have a zillion cores, so presumably one or two non yielding processes don’t actually hold the whole system up.

I’d also assume that a function that is misbehaved (doesn’t return) could be terminated if the system runs out of cores.

My point is that cooperative multitasking doesn’t necessarily equate to poor performance. Time sharing was originally a way to distribute a huge monolithic CPU among multiple users. Now that single user, multi core CPUs are ubiquitous, it’s past time that we think about other ways to use them.

I’m really excited that this project exists.

Just adding to this:

> cooperative multitasking doesn’t necessarily equate to poor performance.

I meant to say “poor interactive performance”

The lack of context switches in this model is likely to actually improve performance. So now I’m curious what would happen if we turned the Linux timeslice up to something stupid like 10s :)

The lack of context switches comes largely from having no security... That's the context being switched, memory protection!
That doesn’t seem right to me. Of course a context switch includes the memory protection, but in a traditional OS there are also registers and other CPU state that need to be saved since a process can be interrupted just about anywhere.

I suppose that I’m idealising a bit here but ISTM that the structure of FOMOS means that the CPU state doesn’t need to be saved, so the context switch involves only memory protection, register resets, stack pointer reset and little else. You don’t even need to preserve the stack between invocations. And unlike preemptive multitasking, there seems to be little or no writing to memory needed, which would seem to obviate a bunch of contention. (Noting that it’s 30 years since I fiddled with operating systems at this level)

Frankly I find this really elegant and exciting.

The TLB flush is the only part of the context switch that's really slow, and it's the part that's needed for a security boundary.
Theseus OS has no context switches, while being even more secure than conventional OSes, all without any reliance on hardware-provided isolation.

  Theseus is a safe-language OS, in which everything runs in a single address space (SAS) and single privilege level (SPL). This includes everything from low-level kernel components to higher-level OS services, drivers, libraries, and more, all the way up to user applications. Protection and isolation are provided by means of compiler and language-ensured type safety and memory safety.
https://www.theseus-os.com/Theseus/book/design/design.html
Yes, but Theseus doesn't run arbitrary binaries.
It got Wasm support recently, and extending this idea of emulators/interpreters, it can run any arbitrary binary in the future.
Wouldn't that be somewhat outside of Theseus' design and add overhead more akin to modern OSes? Theseus relies on Rust's type system (ownership/borrowing and otherwise) to ensure that all binaries have many verified properties; arbitrary WASM program can't hook into that, yes?
The vast majority of programs running on a user's computer today are already running in a VM (JS and WASM), and the number is only increasing. I do not know of any argument in behalf of running everything in a VM (even when it's not a requirement) from a cybersecurity perspective, but I suspect there may be one.

You're right, but maybe this is the way to go and the tradeoff to accept. After all, the ideas behind Theseus feel so obviously correct, alike to those of Nix.

So this is a bit like React on the OS level? Cool project, especially the cooperative scheduling part. Although I'm not sure why insist on a single function (if not for a "hold my beer" moment), because for any non-trivial program the single function will obviously act as the entry point of a state machine, where the state is stored in the context. I'm also not sure about redraws - is the window of a program redrawn every time the function runs?
Finally, someone that tries non-UNIX alternative concepts with their hobby OS...
Is it actually possible to implement security in this OS without a complete redesign and basically redoing what all other existing OS have already done?

I am aware of two ways to enforce security for applications running on the same hardware:

(1) at runtime. All current platforms do this by isolating processes using virtual memory.

(2) at loadtime. The loader verifies that the code does not do arbitrary memory accesses. Usually enforced by only allowing bytecode with a limited instruction set (e.g., no pointer arithmetic) for a virtual machine (JVM, Smalltalk) instead of binaries containing arbitrary machine code.

The author of Fomos doesn't want context switching, memory isolation, etc. And Rust compilers don't produce bytecode. Is there another way?

Wild guess: you could have a single address space shared by all "programs" while using virtual memory to restreint visibility on which page is accessible at a certain time. Like, at runtime, resort on a segfault to check some types of security tokens the caller would to check they are allowed to access the page and make the call. No idea how practical this would be.
> which page is accessible at a certain time

Sounds like a context switch to me :) (at least for the MMU registers)

Theseus is an example of (2), in Rust, without bytecode. As far as I understand, done by enforcing no-unsafe etc rules in a blessed compiler, so basically source code becomes the equivalent of the byte code in your thinking. At a glance it's very similar to Midori, but the details of how it's done are quite different. In Theseus, drivers, applications etc are ELF objects, dynamically linked all together into one executable (which is also the kernel), with some neat tricks like hot upgrades.

https://github.com/theseus-os/Theseus

https://www.theseus-os.com/

Theseus is very cool, as are Singularity and Midori. I'm trying to think of how a general-purpose OS could incorporate ideas from these intralingual OSes while allowing other programming languages to be used, without sacrificing security. I haven't gotten anywhere yet because I'm inexperienced.
I think the Theseus design would accommodate this in 4 different ways:

1. native Rust modules

2. arbitrary code running in WASM sandbox

3. arbitrary code running in KVM virtualization, perhaps with a Linux kernel there to provide a backwards-compat ABI

4. one can compile the WASM+untrusted app into trustworthy machine code (still implementing the WASM sandboxing logic for the untrusted component); I recall Firefox did this with some image handling C++ code they didn't find trustworthy enough

I know the Theseus project is working toward WASM support.

How can you achieve any level of security and safety with un-trusted cooperative apps? Any app can get hold of the CPU for an indefinite amount of time, possibly stalling the kernel and other apps. There's a reason we are using OS-es with preemptive scheduling - any misbehaving app can be interrupted without compromising the rest of the system.
On smalltalk systems like squeak or Pharo, the user interrupts the execution of a thread when it hangs with a keyboard shortcut. And people don't run untrusted code in their "main" image, they would run it in a throw away VM. The same type of model could be used here using an hypervisor. This said, no one uses exclusively a Smalltalk system, it needs some infrastructure.
I remember Microsoft Research had a prototype OS written entirely in .NET some time in mid 2000s; IIRC they used pre-emptive multitasking, but didn't enforce memory protection. Instead, the compiler was a system service: only executables produced (and signed?) by the system compiler were allowed to run, and the compiler promised to enforce memory protection at build time. This made syscalls/IPC extremely cheap!

I think a slightly more fancy compiler could do something similar to "enforce" coop-multitasking: insert yield calls into the code where it deems necessary. While the halting problem is proven to be unsolvable for the general case, there still exists a class of programs where static analysis can prove that the program terminates (or yields). Only programs that can't be proven to yield/halt need to be treated in such fashion.

You can also just set up a watchdog timer to automatically interrupt a misbehaving program.

You might be thinking of Midori. Joe Duffy has written a lot about it on his blog: <https://joeduffyblog.com/2015/11/03/blogging-about-midori/>

They forked C#/.Net, taking the async concept to its extreme and changed the exception/error model, among other things.

There are several other OS projects based on Rust, relying on the memory-safety of the language for memory-protection. Personally, I think the most interesting of those might be Theseus: <https://github.com/theseus-os/Theseus>

Just thinking loud here, would it be an option to load the task to marshal the memory access and cooperative multitasking to something equivalent to llvm? Then multiple different compiler and languages could dock to that.

As long as all of them have to use an authorised llvm equivalent and that one can enforce memory access and cooperation that could look from the outside like a quite normal user experience with many programming languages available?

The second thing you described is common in user space green thread implementations in various languages. Pervasively using it in the entire OS is just taking to its logical conclusion.

For performance though, I don't think halting analysis is needed. Even if the compiler can prove a piece of code terminates, it doesn't help if the inserted yield points occur too infrequently. If a piece of code is calculating the Fibonacci sequence using the naïve way, you do not want the compiler to prove it terminates, because it will terminate too slowly.

A general-purpose OS has to be designed so you never have scenarios where code hangs or yields too infrequently. Best-effort insertion of yield points probably won't cut it. Cooperative multitasking in applications exists on a smaller scale with fewer untrusted qualities.
from-the-page

''' Exo-kernels are interesting, but it is mostly a theory. '''

is that _true_ ? what is the difference between exokernel, and hypervisor ?

A hypervisor is something that might run an exokernel or a more traditional OS. And an exokernel can be run on bare metal rather than a hypervisor.
Xen is considered a "bare-metal hypervisor" because you don't run it as a virtual machine on a Windows/Mac/Linux/etc. host OS. sel4, a very minimal microkernel, can be considered a hypervisor. To my understanding, bare-metal hypervisors and exokernels are quite similar, as they are both a thin layer multiplexing hardware resources and providing security. I have read that the Exokernel exposes more of the hardware to applications.
Apart from KUDOS for effort, this sentence sounds best for it:

...you've got to start with the customer experience and work backwards for the technology. You can't start with the technology and try to figure out where you're going to try to sell it....

So… we now need to consider CX for experiments?