Mark Gritter (markgritter) wrote,
Mark Gritter
markgritter

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.
Tags: algorithm, software
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments