Errata for

A Better x86 Memory Model: x86-TSO (Extended Version). Technical
Report UCAM-CL-TR-745. Scott Owens, Susmit Sarkar, and Peter Sewell.


2009-04-21: The initial and final state constraints for n8 were
buggy; the test should have been:

  {x = 0; y = 0; P0:EAX = 1}      ;
                                  ;
        P0       |       P1       ;
    xchg [x], EAX| mov [y], 1     ;
    mov EBX, [y] | mov EDX, [x]   ;
                                  ;
  exists (P0:EBX = 0 /\ P1:EDX=0) ;

We've not observed that final result in practice.  Thanks to Neal Glew
for pointing this out.