From 8ca00a2729ed477183afeeb1ad20b5a0fc23dc82 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 25 Sep 2017 12:28:26 +0100
Subject: x86: always perform write for cmpxchg by writing back original value
 if comparison fails. This is specified in manual and also helps RMEM with
 locked writes.

---
 x86/x64.sail | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/x86/x64.sail b/x86/x64.sail
index 2f6f07ed..dfa92fd3 100644
--- a/x86/x64.sail
+++ b/x86/x64.sail
@@ -628,8 +628,12 @@ function clause execute (CMPXCHG (locked, sz,r,n)) =
     write_binop (locked, sz, Cmp, val_acc, val_dst, src); 
     if val_acc == val_dst then
       wEA(locked, dst) := EA (false, src)
-    else
+    else {
       wEA(false, acc) := val_dst;
+      (* write back the original value in dst so that we always
+         perform locked write after locked read *)
+      wEA(locked, dst) := val_dst;
+    }
   }
 
 (* ==========================================================================
-- 
cgit v1.2.3