Although a significant fraction of the programming languages community works on detecting race conditions in multi-threaded software, I haven’t been able to get very excited about this. Certainly race-free programs have some nice properties, but race freedom is neither a necessary nor sufficient condition for concurrency correctness. This research area doesn’t feel to me like it is fundamental, but rather an evolutionary stage that has already worn out its welcome.
What I’d like to see — both as a developer and as a researcher — is a much more concrete link between concurrency control and program correctness. For example, in invariant-based synchronization, we specify the invariants that must hold over concurrent data structures and then use partially automated methods to derive locking solutions that guarantee that the invariants are maintained. Coarse-grained solutions are easy to find, and of course fine-grained solutions require more work. The scarcity of papers on this kind of idea has surprised me for a while now. I predict that ideas similar to invariant-based synchronization will become a popular area of research when people get over races and transactions, probably in the 2015-2020 time frame.
3 responses to “Wanted: Invariant-Based Synchronization”
So work on it now!
I agree, but it is the same situation that we have seen in “verification vs. synthesis”. Of course, it is desirable to derive correct programs automatically, rather than proving their correctness a posteriori. Anyway, understanding verification is a prerequisite for understanding synthesis (or in this case, invariant-based synchronization), which may explain the progress in synthesis methods we have seen over recent years. Now that race-freedom is well-understood, I believe that it is only a matter of time until interest in this topic grows. Hm, calls for a POPL paper. 🙂
Hi Robby- I can think of some people who have the tools and the technical know-how to take a good shot at this. But I’m not one of them.