Question

Would it be sensible to have a language that statically checks mutex correctness? Ie,

var m
var x guarded_by(m)

func f1() {
  lock(m)
  x = 42
  unlock(m)
}

func f2() {
  x = 42  // error, accessing x w/o holding its mutex
}

func f3() assumes_locked(m) {
  x = 42
}

func b1() {
  f3()  // error
}

func b2() {
  lock(m)
  f3()
  unlock(m)
}
  1. Is this possible? Ie, can correctness of mutex uses be statically verified with a few simple annotations like this?
  2. Is this sensible? Is there a reason this would be a bad idea?
  3. Are there any languages that have this built-in?
Was it helpful?

Solution

Static race condition detection

As delnan said in a comment, "mutex correctness" can mean a variety of things. From your comment, it sounds like you're talking about race condition detection, which is convenient for me, as this was the subject of my undergraduate thesis :-)¹ You want to know (1) if this is possible, (2) if this is sensible, and (3) if this is done. As with any static analysis (including lightweight type-or-effect-system–like ones such as this), the first two questions boil down to four things:

  1. Soundness: Does it allow any incorrect programs? If so, how many/which ones?
  2. Completeness: Does it rule out any correct programs? If so, how many/which ones?
  3. Usability: How is the programmer overhead? E.g., what annotations are required, are the error messages comprehensible, etc.?
  4. Goals: Where in the design space delimited by the above three constraints are we trying to end up?

Note that we can never get 100% accuracy for both 1 and 2, thanks to the halting problem (and its more general big sibling Rice's theorem). For example, most type systems² aim for soundness and usability (#1 and #3); that is, they aim to be be easy to use while allowing no type-unsafe programs, and try to rule out only unrealistic type-safe programs. (Their advocates, like me, would claim that they've generally succeeded at this goal.)

A simple lock-checking type system: RaceFreeJava

Your example seems like it's trying to maximize usability (#3): you've provided minimal annotations, which correspond to what you'd hope the programmer would have in mind anyway, and then want an analysis which checks them. The overall scheme sounds pretty similar to RaceFreeJava (Abadi et al., 2006). RaceFreeJava is an extension of Java where:

  • Classes can be parametrized by locks (called ghost locks);
  • Fields can have guarded_by annotations specifying which locks must protect them; and
  • Methods can have requires annotations specifying which locks must be held to call them.

As you may have surmised, the idea is that every field has an associated lock, which must be held every time the field is accessed; the analysis tracks which locks are held at every program point, and if a variable is accessed when its lock is not in the current lock set, an error is reported. This gets slightly subtler with ghost lock parameters; for instance, you can have

class RunningTotals<ghost Object m> {
  private int sum     = 0 guarded_by m;
  private int product = 1 guarded_by m;

  public void include(int x) requires m {
    sum     += x;
    product *= x;
  }

  public int getSum() requires m {
    return sum;
  }

  public int getProduct() requires m {
    return product;
  }
}

Now I can embed a RunningTotals object in some other object o and protect it with o's lock, which is handy; however, the analysis thens need to be careful about which lock m really is. Also, note that the methods in RunningTotals cannot synchronize on m, since m isn't in scope and is simply a type-level ghost; synchronization must be handled by the client. Similarly to how we can declare lock-parametrized classes, another feature of RaceFreeJava is the ability to declare thread_local classes; these classes are never allowed to be shared between threads, and consequently don't need to guard their fields with locks.

As you noted in a comment, figuring out if a program is correct with these annotations would, in general, be undecidable, particularly since Java allows you to synchronize on arbitrary expressions. RaceFreeJava restricts synchronization to final expressions, for sanity's sake; then, just as with all type-like annotations, it uses a conservative syntactic check for lock identity. Abadi et al. found that most correct programs could be successfully checked in this manner. Thus, they cleave strongly to soundness (indeed, the analysis is sound modulo some escape hatches they put in) and to usability, at the expense of completeness. In order to check usability – which strongly relates to completeness, since too many spurious warnings make a static analysis nigh-unusable – Abadi et al. also wrote a tool (rccjava) for checking these annotations and doing small amounts of annotation inference, and also used it to build a larger tool (Houdini/rcc) for performing even more inference. When evaluating these (Tables I–IV), they found real bugs without too many necessary annotations or spurious warnings. However, note that it's not perfect; there will be some valid Java programs that this analysis will complain about.

Other static race detectors

Because I have a natural tendency to be long-winded, and because (as I mentioned) I wrote my undergraduate thesis on this, I'll also talk about a few other analyses, but it sounds to me like RaceFreeJava is probably the most relevant. If you want to just skip ahead to the end, there's a summing-up after this section.

Another type-system–based analysis is that presented by Boyapati et al. (2002). This type system detects both race conditions and deadlocks, but using a different technique; it's based on ownership types, which track what threads are allowed to access what variables; variables can only be accessed if the locks on their owners are held. Again, methods can annotate needed accesses or needed locks. For checking deadlocks, Boyapati et al. also add the notion of lock levels, which place all the locks in a partial order. By ensuring that locks are always acquired in this order, deadlocks are automatically ruled out. Again, this algorithm is sound (although the proof is unfortunately omitted) but not complete, and tries to be usable. In order for this, they have to do extensive inference work, as writing down the annotations would be far too much work.

There are other analyses which aren't type systems. These have to model the execution of the program rather than just perform syntactic checks, and tend, as a rule, to be neither sound nor complete, but go all the way for usability by requiring no annotations (even if they allow them) and trying to report useful errors. RacerX (Engler and Ashcraft, 2003) does this, in a sense, by generating enough static information to approximate running a dynamic Lockset-type algorithm, such as that used by Eraser (Savage et al., 1997). This requires plenty of tuning, since approximating a run-time checker statically is not easy, and Lockset is already an approximation to the actual truth. RacerX also performs deadlock checking using a highly tuned constraint-propagation approach, where the constraints are lock orderings. Engler and Ashcraft managed to use RacerX to find some bugs in real operating systems, although they do get false positives and find benign races (Table 5).

One thing that RacerX doesn't handle, by design, is aliasing information: knowing when two references point to the same value. This is important for concurrent code; consider the following faux-C:

// Thread 1:
acquire(superman_lock);
*superman_bank_account += 100; // Saved Metropolis and got rewarded!
release(superman_lock);

// Thread 2:
acquire(clark_kent_lock);
*clark_kent_bank_account -= 100; // More bills...
release(clark_kent_lock);

Presuming that superman_lock and clark_kent_lock are distinct, knowing whether or not this code is safe requires knowing whether superman_bank_account is the same as clark_kent_bank_account. And that's a very difficult thing to figure out!

The Chord algorithm (Naik et al., 2006)³ is a different whole-program race detector which has an alias-detector as a key step; again, though, we run into Rice's theorem, and such an analysis cannot be both sound and complete. Chord tracks might-be-aliased information (equivalently, definitely-unaliased information), and so is unsound.

Summing up

So. You wanted to know three things: is your scheme (1) possible, (2) sensible, and (3) done in the real world? All of these analyses demonstrate that this is a perfectly sensible and possible idea; RaceFreeJava in particular demonstrates that the annotation ideas you had are pretty near a proven-sound type system. However, I don't know of any language that has this built in. I believe every paper I cited here did implement their algorithm, but I haven't looked at all to see if those tools are freely available, commercially available, bitrotted, under active development, or what. Certainly, however, real-world static analyses do exist; for instance, the Coverity's (commercial) static analyzer finds, among many other things, race conditions and deadlocks. They do come with downsides, namely the potential for spurious complaints about good code or no complaints about bad code, but that comes with the territory, and often isn't a big problem in practice.

Footnotes

¹ Well, dynamic race condition detection, anyway. This all means I'm cribbing from the related work section I wrote at the time, which is particularly convenient! It also means this might be missing particularly recent developments (I wrote the thesis in the 2011–2012 academic year). Relatedly, this means it's been a while since I thought about all of this, so it's possible there are egregiously missing citations or (hopefully small) mistakes above; if anybody notices such a thing, please let me know or just edit this post!

² Most sensible type systems, says the Haskell partisan :-) C doesn't care at all, for instance, and Java gets most of the way there but has to resort to dynamic checks thanks to things like downcasting and (*shudder*) array covariance.

³ Sorry about the ACM Digital Library link; I couldn't find a freely-available PDF version of this paper, but I did find a PostScript version.

Bibliography

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top