> Isolation is half the battle when dealing with issues such as these.

having had to deal with race conditions between processes running at opposite side of a continent, color me unimpressed.

That's a sign of a very poor architecture, see also: the fallacies of distributed systems.

Do you mean that each driver is forced to be single-threaded, somehow? Or just that the drivers are isolated, so they can have as many race conditions as they like, but the microkernel will keep running?

Because I don't see the advantage here. So what if my filesystem driver is isolated, a race condition in there is still going to corrupt all my data and I'm not going to be cheered up by the fact that the kernel can keep on ticking.

That's one way of looking at it.

Another is to think of this as layers of essential services: kernel, memory management, networking services, file services and so on. For a layer to be reliable the layers below it have to be reliable too. Isolating the layers in processes allows for faster resolution of where a problem originates which in turn will help to solve it.

And being able to identify the source of a problem allows for several other options: restart the process, proper identification of a longer term resolution because of the ability to log the error much closer to where it originated.

These are not silver bullets but structural approaches acknowledging the fact that software over a certain level of complexity is going to be faulty.

In my opinion the only system that gets this right is Erlang. (not the language, but the whole system)

I take your point about Erlang, and its systems for restarting/replacing failed code & processes, but I don't see how this eliminates race conditions or their consequences.

One problem here is that it's not always a simple layer on layer order of dependencies, they can work both ways. Take swapping/paging for example. It can't be isolated as a separate driver or service. The kernel relies upon it, and so do processes, and yet the service itself relies upon filesystems, a separate layer again. A race condition in the swap system (like one of the bugs found by the tool in question) would break multiple layers, or a race in the filesystem could cause the swap system to fail. There is no real isolation here that saves an OS from failures.

It's not 'magic', but will eliminate a whole swath of possibilities.

One reason why race conditions in monolithic kernels are very common is due to the requirement that code is re-entrant because of multi-threaded execution of the kernel itself. In a micro kernel situation the multi-threading can be avoided because you have enough processes to spread the cpu cores over to have a number of them active at the same time without having two or more of them active within the same process.

> Another is to think of this as layers of essential services: kernel, memory management, networking services, file services and so on. For a layer to be reliable the layers below it have to be reliable too. Isolating the layers in processes allows for faster resolution of where a problem originates which in turn will help to solve it.

is there any reason to believe that most (or even a just considerable part) of race conditions in a kernel are cross module?

Not necessarily, but the effects of a race condition (for instance: a privilege escalation) would be limited to the process the race was found in. That would substantially limited the potential for damage.