That reordering would be bad even with different locks because it can introduce deadlocks, as somebody has pointed out.

There must be some formal semantics reason which forbids it, and I think the reason boils down to the lock not being a single acquire load but instead a loop of acquire loads.

Unlock followed by lock is a store that is followed by a potentially infinite loop. If you move the store past the loop, and the loop happens to be or becomes infinite, then the effect of the store will never become visible, and that is an incorrect program transform because it'd be as-if you simply erased the store.

So you can probably move the store past any finite number of loads, but not past a potentially infinite loop.