I am wondering if machine learning can use used to solve these problems. I have heard that Google uses a machine learning to auto find the bugs and raise merge request against them. Someone from Google can confirm.
You can even have race conditions in hardware. Multi-threading or distributed software are excellent recipes for the introduction of race conditions, sometimes so subtle that the code looks good and the only proof that there is something bad going on is the once-in-a-fortnight system lockup.
#Sarcasm
In a - properly implemented - micro kernel you will have each of those drivers isolated in its own user process, and if there is an issue (memory corruption, crash, logic error or race condition) the possibility of its effects spreading is limited.
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.
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.
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)
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.
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.
is there any reason to believe that most (or even a just considerable part) of race conditions in a kernel are cross module?
Less facetiously, some micro kernels have been proven formally correct. You need a small code to prove formally correct.
And even on an intuitive level, if the code is small I can "hold" it all in my head - at least really grock it in a way you can 1E6 loc.
Would also be cool for auto-complete suggestions. I'm thinking more along the lines of extracting larger patterns than for loops, such as stubbing out classes that follow a projects existing style. For example, adding an auth check at the start of a web request handler if that's what it sees elsewhere.