diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index f9cc25fb5..a62e84c5f 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -115,52 +115,58 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   // This is checked during decoding.
   assert(width_bytes <= xlen_bytes);
 
-  if speculate_conditional () == false then {
-    /* should only happen in rmem
-     * rmem: allow SC to fail very early
-     */
-    X(rd) = zero_extend(0b1); RETIRE_SUCCESS
-  } else {
-    /* normal non-rmem case
-      * rmem: SC is allowed to succeed (but might fail later)
-      */
-    /* Get the address, X(rs1) (no offset).
-      * Extensions might perform additional checks on address validity.
-      */
-    match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
-      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
-      Ext_DataAddr_OK(vaddr) => {
-        if not(is_aligned(virtaddr_bits(vaddr), width))
-        then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
-        else {
-          match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
-                                                      * both result in a SAMO exception */
-            TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-            TR_Address(addr, _) => {
-              // Check reservation with physical address.
-              if not(match_reservation(physaddr_bits(addr))) then {
-                /* cannot happen in rmem */
-                X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
-              } else {
-                let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
-                match eares {
-                  MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-                  MemValue(_) => {
-                    let rs2_val = X(rs2);
-                    match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
-                      MemValue(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
-                      MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
-                      MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+  /* Get the address, X(rs1) (no offset).
+    * Extensions might perform additional checks on address validity.
+    */
+  let res : Retired = match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) => {
+      if not(is_aligned(virtaddr_bits(vaddr), width))
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else {
+        match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
+                                                    * both result in a SAMO exception */
+          TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+          TR_Address(addr, _) => {
+            // Explicitly do access checks first in case the memory does
+            // not exist or doesn't support LR/SC. Without this check we
+            // may get a spurious failure (see below) for LR/SC to memory
+            // that should cause an access fault.
+            let typ = Write(default_write_acc);
+            let priv = effectivePrivilege(typ, mstatus, cur_privilege);
+            match phys_access_check(typ, priv, pbmt, addr, width_bytes, true) {
+              Some(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+              None() => {
+                if not(speculate_conditional()) | not(match_reservation(physaddr_bits(addr))) then {
+                  // Spurious failure (this is allowed), or the reservation
+                  // address does not match.
+                  X(rd) = zero_extend(0b1); RETIRE_SUCCESS
+                } else {
+                  match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
+                    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                    MemValue(_) => {
+                      let rs2_val = X(rs2);
+                      match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
+                        MemValue(true)  => { X(rd) = zero_extend(0b0); RETIRE_SUCCESS },
+                        MemValue(false) => { X(rd) = zero_extend(0b1); RETIRE_SUCCESS },
+                        MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                      }
                     }
                   }
                 }
-              }
+              },
             }
           }
         }
       }
     }
-  }
+  };
+  // The spec says "Regardless of success or failure, executing an SC
+  // instruction invalidates any reservation held by this hart", however
+  // "failure" here does not include failure due to exceptions.
+  // See https://github.com/riscv/riscv-isa-manual/issues/1010
+  if res == RETIRE_SUCCESS then cancel_reservation();
+  res
 }
 
 mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)