Linearizability

Up till this point in the book, we've avoided dipping into the formal terms for specifying concurrent systems, because while they are very useful for discussing ideas and reasoning, they can be difficult to learn absent some context. Now that we have context, it's time.

How do we decide whether a concurrent algorithm is correct? How, if we're game for the algorithm, do we analyze an implementation and reason about it's correctness? To this point, we've used techniques to demonstrate fitness-for-purpose of an implementation through randomized and repeat testing as well as simulation, in the case of helgrind. We will continue to do so. In fact, if that's all we did, demonstrating fitness-for-purpose of implementations, then we'd be in pretty good condition. The working programmer will find themselves inventing more often than not, taking an algorithm and adapting it—as was seen in the previous chapter's discussion of hopper—to fit some novel domain. It's easy enough to do this...