For the record, plenty of big-iron SGI machines also survived the MIPS ISA's LL/SC without stronger forward progress guarantees.

The following observation is apparent from Derek's presentation, but I think it is worth calling out here for those who didn't make it through all 73 pages :-)

Consider the case of atomically incrementing a variable with level 2 or 3 forward progress guarantees:

loop:
lr.w x8, 0(x9)
addi x8, x8, 1
sc.w x8, x8, 0(x9)
bne x8, x0, loop

Suppose two harts execute this code sequence at the same time, and the address in question initially contains the value of zero.  In both harts, the lr.w will read zero which then gets incremented, so that the SC attempts to store the value 1 to memory.  Both harts are REQUIRED to successfully store the value of 1, but the correct result after both harts have executed the loop is 2.

As Derek points out in his presentation, attempts to fix this problem by some how pre-ordaining a winner break down in cases where the code sequence ends up not attempting to execute the sc.w instruction (which is a perfectly legal and valid thing for software to do).  Similarly, attempts to hide the existence of a loser by rolling the machine state back to prior to the loop may technically honor the forward progress guarantee (by never seeming to execute the atomic sequence), but actual forward progress is still not guaranteed, so it is just as "bad" for software as the weak guarantee.

Cheers,
Phil