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.