This originally contained a major mistake. I’ve added an erratum, which I recommend reading (though it is somewhat scattered and poorly edited, as it is late here). Concurrency is hard!