Lambda the Ultimate

The correctness of typestate properties in a multithreaded program often depends on the assumption of certain concurrency invariants. However, standard typestate analysis and concurrency analysis are disjoint in that the former is unable to understand threading effects and the latter does not take typestate properties into consideration. We combine these two previously separate approaches and develop a novel typestate-driven concurrency analysis for detecting race conditions and atomicity violations. Our analysis is based on a reformulation of typestate systems in which state transitions of a shared variable are controlled by the locking state of that variable. By combining typestate checking with lockset analysis, we can selectively transfer the typestate to a transient state to simulate the thread interference effect, thus uncovering a new class of typestate errors directly related to low-level or high-level data races. Such a concurrency bug is more likely to be harmful, compared with those found by existing concurrency checkers, because there exists a concrete evidence that it may eventually lead to a typestate error as well. We have implemented a race and atomicity checker for C/C++ programs by extending a NULL pointer dereference analysis. To support large legacy code, our approach does not require a priori annotations; instead, it automatically infers the lock/data guardianship relation and variable correlations. We have applied the toolset to check a future version of the Windows operating system, finding many concurrency errors that cannot be discovered by previous tools.

Typestates extend the ordinary types by recoding the state of objects and allowing the safety violations that stem from operations being invoked on objects that are in the wrong state.

In an email to the BitC developer mailing list Jonathon Shapiro announced that he is wrapping up development on BitC.

Some of you will have noticed that I have been conspicuously silent over the
last three or four weeks. I have spent much of that time airborne, or in
interviews at Google, Microsoft, and DARPA.

After a fair bit of soul-searching, I have decided to accept a fairly senior
position at Microsoft associated with the Midori project. The current plan
has me starting there at the beginning of August.

This means, among other issues, that we will be wrapping up the BitC
project. While I will be trying hard to get all of the planned features for
the initial release completed before I depart, that may not turn out to be
possible. I have asked Microsoft if we can keep the various web sites alive
for archival access and the mailing list, but I should also ask if there is
anyone out there who would be interested to assume more active stewardship
of the BitC project. I emphasize that unless management at Microsoft
concludes otherwise, I will no longer be able to participate actively in
these discussions. Also, in the event that MS does not permit archival
maintainence, would somebody be willing to take over hosting the content?

I have also asked MS for permission to publish papers about BitC on my own
time. They granted this permission to Swaroop, and I see no reason that they
should decline this, but my position there is a bit more sensitive and they
may see issues that I do not.

In the meantime, I need to get back to packing and hacking.

Best regards,

Jonathan

Best of luck shap! And best of luck BitC!