# Snark, Chord, and Trust in Algorithms

DevFeed: [Snark, Chord, and Trust in Algorithms](<https://devfeed.tech/articles/snark-chord-and-trust-in-algorithms-12453.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2014/03/08/model-checking.html>)

Author: Marc Brooker

Published: 2014-03-08T00:00:00Z

Content type: opinion

Language: en

Sources: [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog.md>), [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog-2.md>)

Topics: [Algorithms, Complexity](<https://devfeed.tech/topics/algorithms-complexity.md>), [Software Engineering](<https://devfeed.tech/topics/software-engineering.md>), [Programming](<https://devfeed.tech/topics/programming.md>), [Code](<https://devfeed.tech/topics/code.md>)

Tags: [algorithms](<https://devfeed.tech/tags/algorithms.md>), [bugs](<https://devfeed.tech/tags/bugs.md>), [code](<https://devfeed.tech/tags/code.md>), [software-engineering](<https://devfeed.tech/tags/software-engineering.md>)

## AI overview

The article examines why reputable authors, journals, institutions, clear pseudocode, and informal proofs are not sufficient grounds for trusting an algorithm. It uses the broken Snark and Chord algorithms to show how subtle safety flaws can survive publication and widespread respect, and discusses model checking as a way to find such errors.

## Source excerpt

Snark, Chord, and Trust in Algorithms Good journals, well-known authors and informal proofs are not sufficient. Mars Code, in February's CACM, is a very interesting look from the outside at some of the software engineering practices that helped make the Mars Science Laboratory mission successful. The authors cover a lot of ground in the article, from code reviews to coding standards to model extraction and model checking. While writing about model checking, they tell the story of Snark, a non-blocking deque algorithm. The Snark paper looks great. The algorithm is presented clearly, including both clear text descriptions and blocks of C-like pseudocode. It's published in a well-respected journal, LNCS. It dedicates four and a half of its fifteen pages to a well-structured and clearly written sketch proof of the correctness of the algorithm, with clear diagrams explaining some of the tricky cases. It's got Guy Steele on the author list. It's from Sun. As far as my is this paper likely to be trustworthy? heuristics go, this one doesn't raise many suspicions. Unfortunately, Snark is broken. Not subtly broken on an obscure liveness measure, but fundamentally broken in that it's unsafe. In DCAS is not a Silver Bullet for Nonblocking Algorithm Design, Doherty et al lay out two bugs in the Snark algorithm. It's worth noting, though, that et al in this case includes most of the authors of the original paper. The paper explains the bugs well, and it's interesting how subtly 30 lines of code can be broken. It's well worth reading, especially if you are interested in non-blocking algorithms. Later, Leslie Lamport used the same bugs as a test of the PlusCal language. In Checking a Multithreaded Algorithm with +CAL he explains how he model checked the original and fixed Snark algorithms using TLC. Snark is not an isolated example either. Another great example is Chord. The hits are similar: top authors, top journal, good institution, and a detailed sketch proof. In Chord's case,