Do barriers in empty loops count as barriers for outer code or not?

As @mattwala remarks here, barrier insertion is subtly incorrect in the case of empty loops.

I'd argue the only correct way out of this is to emit a "spare" barrier before or after the loop (any reason to prefer one over the other?) unless we can prove that the loop is nonempty. The most likely source of such a proof would be a user-supplied assumption.