[concurrency-interest] Ensuring the correctness of concurrent code

Chris Vest mr.chrisvest at gmail.com
Wed Sep 3 16:49:19 EDT 2014


I occasionally have to write code that does shared mutable memory concurrency, have high performance requirements, and needs a high degree of confidence in the correctness of the implementation.

So far I have tackled this by thinking hard and working hard. I’ve written hundreds of tests for tiny APIs, targeted and randomised alike, I’ve drawn up diagrams summarising all the state transitions, I’ve gone through the code to check every against said diagram, I’ve written documentation to specify all observable behaviours, and then written more tests for things I discovered while writing said documentation, sleep on it, wake up and write even more tests for new scenarios I’ve literally dreamt up. And so on…

This has worked well so far, though it takes a lot of effort and discipline. However, as the problems I try to solve get harder, and the optimisations I want to pull off gets more cunning, I feel like I’m approaching the limits of this “technique.”

So, how to other people approach this? How is the correctness of the j.u.c. implementations ensured, for instance?

I have begun studying TLA+ in the hope that the formal specifications might be helpful, but I’m not sure if that’s the right path. I haven’t studied proof techniques before. One worry I have with TLA+ is how to accurately represent the given memory model I’m working with, which has thus far been the JMM.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20140903/e5ea5ada/attachment.html>

More information about the Concurrency-interest mailing list