Students' Revelations about ImNotSure and Static Analysis

A small note on students reacting to ImNotSure.


ImNotSure (the tool name changed for ethical purposes) is a static analysis tool for Java concurrency. Its purpose is to let programmers express a policy of concurrency in a Java program and then check if this policy is violated by the source code (hopefully not). 

In simple terms, an example of policy might be, "no more than one thread should operate a pointer to this class field at any time."

ImNotSure could definitely have been better in terms of documentation and user interaction. What it also lacks is a good basic tutorial that would explain the basic conceptual model of ImNotSure specification. Let me try to do so in two sentences: 

You put data items (class fields, instances, and method return values) into regions and declare what references should be unique and what regions should be protected by which locks. You specify how methods may be called with respect to locks.

After verification is completed, ImNotSure shows its clumsy multi-view UI. Since it's an Eclipse plugin, no usability ambitions can be satisfied, ever.

Another issue with ImNotSure is that its users are so much weirded out by its warnings and errors that they proceed with trial and error, looking to remove warnings by tweaks in code and the ImNotSure spec. This is, I think, a disaster in managing user workflow. 

Finally, ImNotSure exposes users to way too much information at a time. A person drowns in warnings, modeling problems, suggestions, recommendations, correctly implemented things, and so on. Reducing the number of false positive -- or at least their visibility -- would make this tool more bearable. 

--

Having served as a teaching assistant in one CMU course on object-oriented programming, I had a charming experience of making undergrads do what I honestly couldn't do or understand. Making ImNotSure install and run was a pain, and nobody could get rid of all warnings even in a small-sized program (mostly because these were completely obscure). It was quite a sorrowful experience for many students.

I collected several feedback statements about how students liked ImNotSure. Keep this in mind before giving ImNotSure assignment -- perhaps a detailed lecture on the tool might be a good idea. So, students' revelations about ImNotSure:

I found ImNotSure to be very unhelpful.

ImNotSure didn’t really help me understand my concurrency bugs too much.

There were many moments when I was simply adding annotations because it told me to, without quite understanding what was going on. I was simply doing it to prevent its warnings.

Almost invaraibly, these errors were because my annotations had somehow failed to please the mighty ImNotSure gods.

I do sort of wish that I understood those ignored [ones sanctioned to be fine by course staff] bugs more, but glad we didn’t

have to fix them.

ImNotSure really didn't help me “understand” the concurrency bugs.   

I guess ImNotSure isn’t incredibly popular.

To be quite honest, I found usingImNotSure  to be more of a chore and not as much of a learning experience as I feel it was intended to be.   

When there were no errors, I rejoiced and thought I could move on with my life.

Alas, the naivete and innocence of youth!

And my favorite one:

At this point, “Region” and “Unique” are two words that have caused me more mental anguish than I think “Segmentation fault” ever will.

A couple of more positive opinions:

[- Why is ImNotSure useful?] - Because some concurrency bugs are a bitch.

The only thing that made ImNotSure hard was the lack of concise and clear examples.

P.S. To be fair, negative judgements constituted only half of the feedback. But that's a lot!