Don't trust published algorithms, even bearing proofs
I found this blog post interesting http://brooker.co.za/blog/2014/03/08/model-checking.html both because it discussed flaws in Chord (and I can't even start to name all the other research projects based on Chord or Chord-like designs from my time as a PhD student) as well as a DCAS-based data structure, Snark. Both algorithms were published by very respected professionals, and the publications included proofs of correctness.
The linked paper from 2004 (DCAS is not a Silver Bullet for Nonblocking Algorithm Design) talks a bit about Michael Greenwald's work which I got to hear about when I joined Cheriton's research group. I remember tagging along to a talk he gave at Intel trying to convince them of the benefit of DCAS.
I have played around a lot with the Alloy tool (http://alloy.mit.edu/alloy/) and even used it for some Tintri designs. (Maybe that could be a Minnebar talk...) But model-checking is no silver bullet either. It can tell you about failure cases but not guarantee success.
The linked paper from 2004 (DCAS is not a Silver Bullet for Nonblocking Algorithm Design) talks a bit about Michael Greenwald's work which I got to hear about when I joined Cheriton's research group. I remember tagging along to a talk he gave at Intel trying to convince them of the benefit of DCAS.
I have played around a lot with the Alloy tool (http://alloy.mit.edu/alloy/) and even used it for some Tintri designs. (Maybe that could be a Minnebar talk...) But model-checking is no silver bullet either. It can tell you about failure cases but not guarantee success.