[xorblurb]

This seems like an interesting book but a few points are dangerous, especially if it is used for teaching.

1. Concurrent access to a variable out of a critical section is qualified as not being dangerous. This actually can't be decided without knowing about the memory model you are considering, and both in the general case and in practical implementations (C++) this is UB.

2. This sentence is maybe only trying to be funny, but discouraging formal proofs in 2016 can very well end up borderline criminal (depending on the application): "The only alternative is to examine the code carefully and “prove” that it is correct. I put “prove” in quotation marks because I don’t mean, necessarily, that you have to write a formal proof (although there are zealots who encourage such lunacy)."

Especially if this is stated right after a rather simple algorithm.

I can absolutely not recommend a book about a critical topic, which contains that kind of defects.

[yebyen]

> in practical implementations (C++) this is UB.

Huh. I had heard of nasal demons before but I had never seen this abbreviation "UB"

TIL, UB and IB

https://stackoverflow.com/questions/2766731/what-exactly-do-...

[devnonymous]

> I can absolutely not recommend a book about a critical topic, which contains that kind of defects.

I think your definition of formal proofs is a bit different from Alan Downey's (who incidentally has also written an entire book on Complexity and the Philosophy of science[1]). Providing a formal proof for even a 'simple' algorithm is incredibly wasteful in the context of the example in which the statement is made. Perhaps you should read the book before calling out it's 'defects'.

[1] http://greenteapress.com/complexity/index.html

More of Alan's books at: http://greenteapress.com/

[carapace]

*Allen

[ptero]

Semaphore is a tool. Like any tool, to use it well you need to apply it correctly and know of its limitations (e.g., what are the guarantees it requires) and your environment (e.g., what the OS / library provides).

IMO the problems in actual software are almost always between the keyboard and the chair; one can write junk using any sync primitives. My 2c.

[ghthor]

I never understood what use a semaphore was until I tried my hand at implementing go like channels in swift. It's a very strange primitive that I don't think many people understand when it should be used.