Skip to content

Commit 29371d1

Browse files
marangetmaranget
committed
[herd] Attempt to limit the number of spurious AF updates
We attempt to identify the value stored by writes to page table entries. When this value has the AF flag set, there is no need to emit a spurious update. For a precise detection of this situation the stored value is now retrieved by anticipation.
1 parent 3004dae commit 29371d1

File tree

1 file changed

+77
-56
lines changed

1 file changed

+77
-56
lines changed

‎herd/AArch64Sem.ml‎

Lines changed: 77 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -1058,14 +1058,15 @@ module Make
10581058
check_cond cond)
10591059
end in
10601060
if pte2 then mvirt
1061-
else
1062-
M.op1 Op.IsVirtual a_virt >>= fun cond ->
1063-
M.choiceT cond mvirt
1061+
else begin
1062+
let mdirect =
10641063
(* Non-virtual accesses are disallowed from EL0.
10651064
For instance, user code cannot access the page table. *)
1066-
(if is_el0 then mk_pte_fault a_virt ma dir an ii
1067-
else mdirect)
1068-
1065+
if is_el0 then mk_pte_fault a_virt ma dir an ii
1066+
else mdirect in
1067+
M.op1 Op.IsVirtual a_virt >>= fun cond ->
1068+
M.choiceT cond mvirt mdirect
1069+
end
10691070
(* Read memory, return value read *)
10701071
let do_read_mem_ret sz an anexp ac a ii =
10711072
let m a =
@@ -1385,23 +1386,37 @@ module Make
13851386

13861387
let some_ha = dirty.DirtyBit.some_ha || dirty.DirtyBit.some_hd
13871388

1388-
let fire_spurious_af dir a m =
1389-
if
1389+
let can_be_pt v =
1390+
match V.as_constant v with
1391+
| None -> true
1392+
| Some c -> Constant.is_pt c
1393+
1394+
let can_af0 _tag v =
1395+
pte2 ||
1396+
(match V.as_constant v with
1397+
| Some (Constant.PteVal p) -> p.AArch64PteVal.af = 0
1398+
| _ -> true)
1399+
1400+
let fire_spurious_af tag v dir a m =
1401+
let do_fire =
13901402
some_ha &&
1391-
(let v = C.variant Variant.PhantomOnLoad in
1392-
match dir with Dir.W -> not v | Dir.R -> v)
1403+
(let b = C.variant Variant.PhantomOnLoad in
1404+
match dir with
1405+
| Dir.W -> not b && can_be_pt a && can_af0 tag v
1406+
| Dir.R -> b) in
1407+
if do_fire
13931408
then
13941409
(m >>|
13951410
M.altT (test_and_set_af_succeeds a E.IdSpurious) (M.unitT ())) >>=
13961411
fun (r,_) -> M.unitT r
13971412
else m
13981413

1399-
let lift_kvm dir updatedb mop ma an ii mphy =
1414+
let lift_kvm tag v dir updatedb mop ma an ii mphy =
14001415
let mfault ma a ft = emit_fault a ma dir an ft None ii in
14011416
let maccess a ma =
14021417
check_ptw ii.AArch64.proc dir updatedb false a ma an ii
14031418
((let m = mop Access.PTE ma in
1404-
fire_spurious_af dir a m) >>= M.ignore >>= B.next1T)
1419+
fire_spurious_af (tag^"1") v dir a m) >>= M.ignore >>= B.next1T)
14051420
mphy
14061421
mfault in
14071422
M.delay_kont "6" ma (
@@ -1415,7 +1430,7 @@ module Make
14151430
mop ac ma >>= M.ignore >>= B.next1T
14161431
)
14171432

1418-
let lift_memtag_phy dir mop ma an ii mphy =
1433+
let lift_memtag_phy v dir mop ma an ii mphy =
14191434
let checked_op mpte_d a_virt =
14201435
let mok mpte_t =
14211436
let ma = M.para_bind_output_right mpte_t (fun _ -> mpte_d) in
@@ -1448,7 +1463,7 @@ module Make
14481463
M.delay_kont "tag_ptw" ma @@ fun a ma ->
14491464
let mdirect =
14501465
let m = mop Access.PTE ma in
1451-
fire_spurious_af dir a m >>= M.ignore >>= B.next1T in
1466+
fire_spurious_af "2" v dir a m >>= M.ignore >>= B.next1T in
14521467
check_ptw ii.AArch64.proc Dir.R false true a ma an ii
14531468
mdirect
14541469
cond_check_tag
@@ -1545,36 +1560,42 @@ Arguments:
15451560
- an: Annotation for the event structure.
15461561
- ii: Instruction metadata.
15471562
*)
1548-
let lift_memop rA dir updatedb checked mop perms ma mv an ii =
1563+
let lift_memop ?(tag="") rA dir updatedb checked mop perms ma mv an ii =
15491564
if morello then
15501565
lift_morello mop perms ma mv dir an ii
15511566
else
1552-
let mop = apply_mv mop mv in
1553-
if kvm then
1554-
let mphy ma a_virt =
1555-
let ma = get_oa a_virt ma in
1556-
if pte2 then
1557-
M.op1 Op.IsVirtual a_virt >>= fun c ->
1558-
M.choiceT c
1559-
(mop Access.PHY ma)
1560-
(fire_spurious_af dir a_virt (mop Access.PHY_PTE ma))
1561-
>>= M.ignore >>= B.next1T
1562-
else
1563-
mop Access.PHY ma
1564-
>>= M.ignore >>= B.next1T in
1565-
let mphy =
1566-
if checked then lift_memtag_phy dir mop ma an ii mphy
1567-
else mphy
1568-
in
1569-
let m = lift_kvm dir updatedb mop ma an ii mphy in
1567+
(match dir with
1568+
| Dir.W ->
1569+
M.delay_kont "MV" mv
1570+
| _ ->
1571+
fun f -> f V.zero mv)
1572+
(fun v mv ->
1573+
let mop = apply_mv mop mv in
1574+
if kvm then
1575+
let mphy ma a_virt =
1576+
let ma = get_oa a_virt ma in
1577+
if pte2 then
1578+
M.op1 Op.IsVirtual a_virt >>= fun c ->
1579+
M.choiceT c
1580+
(mop Access.PHY ma)
1581+
(fire_spurious_af "3" v dir a_virt (mop Access.PHY_PTE ma))
1582+
>>= M.ignore >>= B.next1T
1583+
else
1584+
mop Access.PHY ma
1585+
>>= M.ignore >>= B.next1T in
1586+
let mphy =
1587+
if checked then lift_memtag_phy v dir mop ma an ii mphy
1588+
else mphy
1589+
in
1590+
let m = lift_kvm tag v dir updatedb mop ma an ii mphy in
15701591
(* M.short will add an iico_data only if memtag is enabled *)
1571-
M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m
1572-
else if pac then
1573-
lift_pac_virt mop ma dir an ii
1574-
else if checked then
1575-
lift_memtag_virt mop ma dir an ii
1576-
else
1577-
mop Access.VIR ma >>= M.ignore >>= B.next1T
1592+
M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m
1593+
else if pac then
1594+
lift_pac_virt mop ma dir an ii
1595+
else if checked then
1596+
lift_memtag_virt mop ma dir an ii
1597+
else
1598+
mop Access.VIR ma >>= M.ignore >>= B.next1T)
15781599

15791600
(* Address translation instruction *)
15801601
let do_at op rd ii =
@@ -1601,7 +1622,7 @@ Arguments:
16011622
let maccess a ma =
16021623
check_ptw ii.AArch64.proc dir false false a ma Annot.N ii
16031624
((let m = mop Access.PTE ma in
1604-
fire_spurious_af dir a m) >>= M.ignore >>= B.next1T)
1625+
(* fire_spurious_af "4" v dir a *) m) >>= M.ignore >>= B.next1T)
16051626
mphy
16061627
mfault in
16071628
M.delay_kont "at::check_ptw" ma maccess
@@ -1614,7 +1635,7 @@ Arguments:
16141635
if memtag && C.mte_store_only then
16151636
ma >>= fun a -> loc_extract a
16161637
else ma in
1617-
lift_memop rA Dir.R false checked
1638+
lift_memop ~tag:"LD" rA Dir.R false checked
16181639
(fun ac ma _mv -> (* value fake here *)
16191640
let open Precision in
16201641
let memtag_sync =
@@ -1629,7 +1650,7 @@ Arguments:
16291650

16301651
(* Generic store *)
16311652
let do_str rA mop sz an ma mv ii =
1632-
lift_memop rA Dir.W true memtag
1653+
lift_memop ~tag:"ST" rA Dir.W true memtag
16331654
(fun ac ma mv ->
16341655
let open Precision in
16351656
let memtag_sync = memtag && C.mte_precision = Synchronous in
@@ -1914,12 +1935,12 @@ Arguments:
19141935

19151936
let str_simple sz rs rd m_ea ii =
19161937
do_str rd
1917-
(fun ac a _ ii ->
1918-
M.data_input_next
1919-
(read_reg_data_sz sz rs ii)
1920-
(fun v -> do_write_mem sz Annot.N aexp ac a v ii))
1938+
(fun ac a v ii ->
1939+
M.data_input_next
1940+
(M.unitT v)
1941+
(fun v -> do_write_mem sz Annot.N aexp ac a v ii))
19211942
sz Annot.N
1922-
m_ea (M.unitT V.zero) ii
1943+
m_ea (read_reg_data_sz sz rs ii) ii
19231944

19241945
let str sz rs rd e ii =
19251946
let open AArch64Base in
@@ -1933,14 +1954,14 @@ Arguments:
19331954
(read_reg_addr rd ii)
19341955
(fun a_virt ma ->
19351956
do_str rd
1936-
(fun ac a _ ii ->
1957+
(fun ac a v ii ->
19371958
M.add a_virt (V.intToV k) >>= fun b -> write_reg rd b ii
19381959
>>|
19391960
M.data_input_next
1940-
(read_reg_data_sz sz rs ii)
1961+
(M.unitT v)
19411962
(fun v -> do_write_mem sz Annot.N aexp ac a v ii))
19421963
sz Annot.N
1943-
ma (M.unitT V.zero) ii) in
1964+
ma (read_reg_data_sz sz rs ii) ii) in
19441965
if kvm then M.upOneRW (is_this_reg rd) m
19451966
else m
19461967
| Imm (k,PreIdx) ->
@@ -2037,9 +2058,9 @@ Arguments:
20372058
(write_reg ResAddr V.zero ii)
20382059
(fun v -> write_reg rr v ii)
20392060
(mw an ac))
2040-
(to_perms "w" sz)
2041-
(read_reg_addr rd ii)
2042-
ms an ii
2061+
(to_perms "w" sz)
2062+
(read_reg_addr rd ii)
2063+
ms an ii
20432064

20442065
let stxr sz t rr rs rd ii =
20452066
do_stxr
@@ -2113,7 +2134,7 @@ Arguments:
21132134
(* Dir.W would force check for dbm bit: *)
21142135
(* - if set then either update or not db bit per R_TXGHB *)
21152136
(* - if unset raise Permission fault *)
2116-
lift_memop rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
2137+
lift_memop ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
21172138
in
21182139
if do_wb then
21192140
do_action true checked ma
@@ -2154,7 +2175,7 @@ Arguments:
21542175
M.altT (
21552176
(* CAS succeeds and generates an Explicit Write Effect *)
21562177
(* there must be an update to the dirty bit of the TTD *)
2157-
lift_memop rn Dir.W true memtag mop_success (to_perms "rw" sz) ma mv an ii
2178+
lift_memop ~tag:"CAS" rn Dir.W true memtag mop_success (to_perms "rw" sz) ma mv an ii
21582179
)( (* CAS fails *)
21592180
M.altT (
21602181
(* CAS generates an Explicit Write Effect *)

0 commit comments

Comments
 (0)