Are the flush statements all strong flushes? I assume this is the case,
since they use variable lists, but the use of pseudocode rather than
the more precise actual code made me a little unsure. It would be nice
to state this explicitly.
Adding to this confusion is the fact that there are implicit strong
flushes upon entering and exiting each atomic operation. So what is the point
of the "flush(b)" in thread 1, since it follows an atomic operation
on b, which already includes a strong flush on b upon exit? Isn't it
redundant? Again, that doesn't mean it is wrong, but it would be nice
to clarify that in the text.
The preceding text states "The atomic notation in the pseudocode in
the following two examples indicates that the accesses to a and b are
ATOMIC writes and captures". There are four atomic statements, so which
are writes and which are captures? And why captures instead of reads?