diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 71cb949541..ac13fa22bc 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -1971,7 +1971,6 @@ module Make let read_rs = read_reg_data sz rs ii and write_rs v = write_reg_sz sz rs v ii in let noret = match rs with | AArch64.ZR -> true | _ -> false in - let is_phy ac = Access.is_physical ac in let branch a = let cond = Printf.sprintf "[%s]==%d:%s" (V.pp_v a) ii.A.proc (A.pp_reg rs) in commit_pred_txt (Some cond) ii in @@ -1980,7 +1979,7 @@ module Make let read_mem a = if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii else do_read_mem_ret sz an aexp ac a ii in - M.aarch64_cas_no (is_phy ac) ma read_rs write_rs read_mem branch M.neqT + M.aarch64_cas_no (Access.is_physical ac) ma read_rs write_rs read_mem branch M.neqT in let mop_fail_with_wb ac ma _ = (* CAS fails, there is an Explicit Write Effect writing back *) @@ -1989,7 +1988,7 @@ module Make if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii else rmw_amo_read sz rmw ac a ii and write_mem a v = rmw_amo_write sz rmw ac a v ii in - M.aarch64_cas_no_with_writeback (is_phy ac) ma read_rs write_rs + M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs write_rs read_mem write_mem branch M.neqT in let mop_success ac ma mv = @@ -2001,27 +2000,28 @@ module Make if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii else rmw_amo_read sz rmw ac a ii and write_mem a v = rmw_amo_write sz rmw ac a v ii in - M.aarch64_cas_ok (is_phy ac) ma read_rs read_rt write_rs + M.aarch64_cas_ok (Access.is_physical ac) ma read_rs read_rt write_rs read_mem write_mem branch M.eqT in M.altT ( (* CAS succeeds and generates an Explicit Write Effect *) (* there must be an update to the dirty bit of the TTD *) - lift_memop rn Dir.W true memtag mop_success - (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii + lift_memop rn Dir.W true memtag mop_success (to_perms "rw" sz) + (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii )( (* CAS fails *) M.altT ( (* CAS generates an Explicit Write Effect *) (* there must be an update to the dirty bit of the TTD *) - lift_memop rn Dir.W true memtag mop_fail_with_wb - (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii + lift_memop rn Dir.W true memtag mop_fail_with_wb (to_perms "rw" sz) + (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii )( (* CAS does not generate an Explicit Write Effect *) (* It is IMPLEMENTATION SPECIFIC if there is an update to *) (* the dirty bit of the TTD *) (* Note: the combination of dir=Dir.R and updatedb=true *) (* triggers an alternative in check_ptw *) - lift_memop rn Dir.R true memtag mop_fail_no_wb (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii + lift_memop rn Dir.R true memtag mop_fail_no_wb (to_perms "rw" sz) + (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii ) ) @@ -2037,37 +2037,77 @@ module Make let cond = Printf.sprintf "[%s]=={%d:%s,%d:%s}" (V.pp_v a) ii.A.proc (A.pp_reg rs1) ii.A.proc (A.pp_reg rs1) in commit_pred_txt (Some cond) ii in - lift_memop rn Dir.W true memtag - (fun ac ma _ -> - let is_phy = Access.is_physical ac in - M.altT - (let read_mem a = do_read_mem_ret sz an aexp ac a ii + let neqp (v1,v2) (x1,x2) = + M.op Op.Eq v1 x1 >>| M.op Op.Eq v2 x2 + >>= fun (b1,b2) -> M.op Op.And b1 b2 + >>= M.eqT V.zero + and eqp (v1,v2) (x1,x2) = + M.eqT v1 x1 >>| M.eqT v2 x2 + >>= fun _ -> M.unitT () in + let mop_fail_no_wb ac ma _ = + (* CASP fails, there are no Explicit Write Effects *) + let read_mem a = do_read_mem_ret sz an aexp ac a ii >>| (add_size a sz >>= fun a -> do_read_mem_ret sz an aexp ac a ii) in - let neqp (v1,v2) (x1,x2) = - M.op Op.Eq v1 x1 >>| M.op Op.Eq v2 x2 - >>= fun (b1,b2) -> M.op Op.And b1 b2 - >>= M.eqT V.zero in - M.aarch64_cas_no is_phy ma read_rs write_rs read_mem branch neqp) - (let read_rt = read_reg_data sz rt1 ii + M.aarch64_cas_no (Access.is_physical ac) ma read_rs + write_rs read_mem branch neqp + in + let mop_fail_with_wb ac ma _ = + (* CASP fails, there are Explicit Write Effects writing back *) + (* the value that is already in memory *) + let read_mem a = do_read_mem_ret sz an aexp ac a ii + >>| (add_size a sz + >>= fun a -> do_read_mem_ret sz an aexp ac a ii) + and write_mem a (v1,v2) = + rmw_amo_write sz rmw ac a v1 ii + >>| (add_size a sz >>= fun a2 -> + rmw_amo_write sz rmw ac a2 v2 ii) + >>= fun _ -> M.unitT () in + M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs + write_rs read_mem write_mem branch neqp + in + let mop_success ac ma _ = + (* CASP succeeds, there are Explicit Write Effects *) + let read_rt = read_reg_data sz rt1 ii >>| read_reg_data sz rt2 ii - and read_mem a = rmw_amo_read sz rmw ac a ii + and read_mem a = rmw_amo_read sz rmw ac a ii >>| (add_size a sz >>= fun a -> rmw_amo_read sz rmw ac a ii) - and write_mem a (v1,v2) = - rmw_amo_write sz rmw ac a v1 ii - >>| (add_size a sz >>= fun a2 -> - rmw_amo_write sz rmw ac a2 v2 ii) - >>= fun _ -> M.unitT () - and eqp (v1,v2) (x1,x2) = - M.eqT v1 x1 >>| M.eqT v2 x2 - >>= fun _ -> M.unitT () in - M.aarch64_cas_ok is_phy ma read_rs read_rt write_rs - read_mem write_mem branch eqp)) - (to_perms "rw" sz) - (read_reg_ord rn ii) - (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii) - an ii + and write_mem a (v1,v2) = + rmw_amo_write sz rmw ac a v1 ii + >>| (add_size a sz >>= fun a2 -> + rmw_amo_write sz rmw ac a2 v2 ii) + >>= fun _ -> M.unitT () in + M.aarch64_cas_ok (Access.is_physical ac) ma read_rs + read_rt write_rs read_mem write_mem branch eqp + in + M.altT ( + (* CASP succeeds and generates Explicit Write Effects *) + (* there must be an update to the dirty bit of the TTD *) + lift_memop rn Dir.W true memtag mop_success + (to_perms "rw" sz) (read_reg_ord rn ii) + (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii) + an ii + )( (* CASP fails *) + M.altT ( + (* CASP generates Explicit Write Effects *) + (* there must be an update to the dirty bit of the TTD *) + lift_memop rn Dir.W true memtag mop_fail_with_wb + (to_perms "rw" sz) (read_reg_ord rn ii) + (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii) + an ii + )( + (* CASP does not generate Explicit Write Effects *) + (* It is IMPLEMENTATION SPECIFIC if there is an update to *) + (* the dirty bit of the TTD *) + (* Note: the combination of dir=Dir.R and updatedb=true *) + (* triggers an alternative in check_ptw *) + lift_memop rn Dir.R true memtag mop_fail_no_wb + (to_perms "rw" sz) (read_reg_ord rn ii) + (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii) + an ii + ) + ) (* Temporary morello variation of CAS *) let cas_morello sz rmw rs rt rn ii = diff --git a/herd/tests/instructions/AArch64/A242.litmus.expected b/herd/tests/instructions/AArch64/A242.litmus.expected index 3b325822a8..656b629aa7 100644 --- a/herd/tests/instructions/AArch64/A242.litmus.expected +++ b/herd/tests/instructions/AArch64/A242.litmus.expected @@ -3,8 +3,8 @@ States 1 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 36 Negative: 0 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2) -Observation A242 Always 16 0 +Observation A242 Always 36 0 Hash=a53545f0a258acc581288f0aa9b5c936 diff --git a/herd/tests/instructions/AArch64/A243.litmus.expected b/herd/tests/instructions/AArch64/A243.litmus.expected index 1c58842cbb..d14ebc4f37 100644 --- a/herd/tests/instructions/AArch64/A243.litmus.expected +++ b/herd/tests/instructions/AArch64/A243.litmus.expected @@ -3,8 +3,8 @@ States 1 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 36 Negative: 0 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2) -Observation A243 Always 16 0 +Observation A243 Always 36 0 Hash=450d6bea2cb06cb6a4eec6037dcb6802 diff --git a/herd/tests/instructions/AArch64/A244.litmus.expected b/herd/tests/instructions/AArch64/A244.litmus.expected index 80bf037ee5..644f0a4b5c 100644 --- a/herd/tests/instructions/AArch64/A244.litmus.expected +++ b/herd/tests/instructions/AArch64/A244.litmus.expected @@ -3,8 +3,8 @@ States 1 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 36 Negative: 0 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2) -Observation A244 Always 16 0 +Observation A244 Always 36 0 Hash=f5f65af42b0b1c4ef91a867eb4c84a3c diff --git a/herd/tests/instructions/AArch64/A245.litmus.expected b/herd/tests/instructions/AArch64/A245.litmus.expected index 1c52bbb647..f402cafe89 100644 --- a/herd/tests/instructions/AArch64/A245.litmus.expected +++ b/herd/tests/instructions/AArch64/A245.litmus.expected @@ -3,8 +3,8 @@ States 1 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 36 Negative: 0 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2) -Observation A245 Always 16 0 +Observation A245 Always 36 0 Hash=51b29db6588f853cf4e04fe2a1242893 diff --git a/herd/tests/instructions/AArch64/A246.litmus.expected b/herd/tests/instructions/AArch64/A246.litmus.expected index 8f7b3f8f3f..29d411f03c 100644 --- a/herd/tests/instructions/AArch64/A246.litmus.expected +++ b/herd/tests/instructions/AArch64/A246.litmus.expected @@ -3,8 +3,8 @@ States 1 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 36 Negative: 0 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2) -Observation A246 Always 16 0 +Observation A246 Always 36 0 Hash=dfcdd105748ed1fb63dad2657811b691 diff --git a/herd/tests/instructions/AArch64/L056.litmus.expected b/herd/tests/instructions/AArch64/L056.litmus.expected index ae161e7392..41000755f0 100644 --- a/herd/tests/instructions/AArch64/L056.litmus.expected +++ b/herd/tests/instructions/AArch64/L056.litmus.expected @@ -4,8 +4,8 @@ States 2 1:X0=1; 1:X1=0; x={1,0}; Ok Witnesses -Positive: 4 Negative: 0 +Positive: 6 Negative: 0 Condition forall (x={1,0} \/ x={1,2}) -Observation L056 Always 4 0 +Observation L056 Always 6 0 Hash=56239ea29c96ee505c91efa59ac63a18 diff --git a/herd/tests/instructions/AArch64/L057.litmus.expected b/herd/tests/instructions/AArch64/L057.litmus.expected index 7a35d4d581..4a44a6c99f 100644 --- a/herd/tests/instructions/AArch64/L057.litmus.expected +++ b/herd/tests/instructions/AArch64/L057.litmus.expected @@ -4,8 +4,8 @@ States 2 1:X0=0; 1:X1=1; x={0,1}; Ok Witnesses -Positive: 4 Negative: 0 +Positive: 6 Negative: 0 Condition forall (x={0,1} \/ x={2,1}) -Observation L057 Always 4 0 +Observation L057 Always 6 0 Hash=57ac32621316eec60874e7e2c863b043