Google Is Uncovering Hundreds of Race Conditions Within the Linux Kernel

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

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.

https://www.cs.colorado.edu/~kena/classes/5828/s12/presentat...

https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-li...

Here's the main competition evaluating them so you can see criteria and current state-of-the-art:

https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_V...

The provers do something similar but with more manual effort and logic-based approach. Frama-C and SPARK Ada are interesting in that they use programmer annotations plus supporting functions (eg ghost code). These are converted into logical representation (eg facts about the program), fed into logic solvers with properties intended to be proved, and success/failure maybe tells you something. Like with static analyzers, you get the results without running the program. A recent, great addition is that, if proof is too hard, the condition you didn't prove can be turned into a runtime check. You could even do that by default only proving the ones that dragged performance down too much. Flexible.

The best methods are a mix. I've always advocated mixing static analyzers, dynamic analysis, fuzzing etc since each technique might spot something the other will miss. They also cover for implementation bugs each might have. That adding runtime analysis can improve effectiveness does not negate my original claim that static, non-runtime analysis of C code can tell you a lot about it and/or find a ton of bugs. I also agreed with one point you made about it not conveying enough information: these clever tools pull it off despite C lacking design attributes that would make that easier. SPARK Ada is a great example of a language designed for low-level, efficient coding and easy verification. Although, gotta give credit to Frama-C people for improving things on C side.

Refcounting in Rust is still faster than refcounting in ObjC or Swift (because Rust can avoid using atomics or increasing counts in many cases), but people who use Rust tend to insist on zero overhead, and a truly flexible zero-overhead solution can't be verified statically.

However, it is possible to leak, e.g. if you use a reference-counted type and create a cycle. There's also Box::leak() that does what it says (it's useful for singleton-like things).

This is different from Rust's guarantees about memory and thread safety, which you can't break without `unsafe`.

Edit: (or go double the speed limit if you must but please stop creating stops)

> In the UK, in 2009, it was revealed that the Department for Transport had previously discouraged green waves as they reduced fuel usage, and thus less revenue was raised from fuel taxes.

Ugh...

There is this thing called the "waiting time paradox" [0] (or more generally the "inspection paradox") that suggests a surprising thing, the average time between discrete events observed by many other randomly interspersed observation is the same as the average time between events. This should be surprising, because it suggests that many more people experience times LONGER than the average wait to balance out people who experience a shorter wait because they were randomly closer to the event.

This happens because longer intervals, when they do exist, get a larger proportion of the random observations than the shorter intervals between events. More precisely and generically, when the quantity being observed affects the observer, the observations will be distorted by the quantity in question and have to be normalized.

In the case of a green wave, those rare times when someone waits too long on a green because they were looking at their phone or a naked person in a nearby window and create slowdowns and stalls in the pipeline? Those moments are longer, so there is a longer window where you could experience them.

This actually comes up a lot in observations of things in nature. Imagine if instead of light flips or bus arrivals we were observing clicks on a geiger counter and you'll realize how fundamental this is to experiencing the world.

tl;dr: The Green Wave only works in averages and it can be correct even as your experience of it never working is also correct. :)

[0]: https://jakevdp.github.io/blog/2018/09/13/waiting-time-parad...

Imagine a translucent checker board of blue and black squares overlaid on top of a map of roads. You can see the color of the squares but you can also see the roads underneath them.

If a light falls on a blue square, make its principal north/south direction Red at t=0 and it’s principal east/west direction green. For black squares do the opposite.

Calculate how long it would take cars to travel through each square unimpeded. It helps if this time is roughly the same regardless of direction. It also helps if the squares are roughly large enough that it takes roughly one light phase worth of time to travel through it. Call that time N.

At t=N, switch the lights to the opposite color, so now north/southbound traffic gets green lights on blue squares, and east/west gets red. Black squares get the opposite.

What you’ll see if you imagine yourself as a car driving through this, is that as you enter a black square as it turns green, the green lights will stay green until you enter the nearest blue square, at which point the phase shifts and now the blue square gets green lights as you drive through it.

This works in both directions, with both north and south bound traffic.

Now, this falls apart when roads are diagonal, although it’s mitigated if diagonal roads have higher speed limits. It also means if you make a turn, you’re in the wrong light cycle, but it will correct itself after the next red light.

It also doesn’t work well at all if you have left turn arrows complicating your light cycles, so you’ll need to have something like a Michigan Left and the requisite wide medians to make this work.

It’s not as ideal as I described in real life, but the basic principle works.

You can use it to refer to any race, but in reality the race you are referring to is only subjective to the user. The server is generally processing all requests in the order they are received.

A race condition usually is referring to a multithreaded system where the threads interfere with each other, causing undesired effects.

Relaxing "race condition" to refer to all causality... is such a loose definition as to give it no meaning at all.

Of course both things could be true...

Some people argue that the Earth is flat. That doesn't mean they have a good point.

The morons you're referencing probably think cars should all go back to drum brakes and bias-ply tires so people think more about brake fade and tire grip. It's an idiotic argument. Disc brakes on bikes are better in every way, except weight (they add about 1 pound, maybe). Reducing performance available to a cyclist doesn't make any sense at all; you never know when you're going to need to stop suddenly in the real world.

Fair point. As the old saying goes "looser is faster". The risk, of course, is that you wind up in the wall with your velocity = 0. :-)