Skip to content

Commit 1ab51cf

Browse files
raghavRaghavRoy145
raghav
authored and
RaghavRoy145
committed
Adds semantics for the event register instructions: WFE, SEV, SEVL
The three instructions interact with event registers as follows: SEVL: Send Event Local. Sets the current PE's event register to 1. SEV: Send Event. Sets every PE's event register to 1 (broadcast wake-up). WFE: Wait For Event. If the event register is 1, clear it and fall through. If it is 0, wait until some other PE issues SEV before clearing and continuing. The event register is modelled as a per-thread symbolic memory location
1 parent e9e74e8 commit 1ab51cf

16 files changed

Lines changed: 137 additions & 27 deletions

‎herd/AArch64Arch_herd.ml‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
103103
| I_SWP _| I_SWPBH _| I_SXTW _| I_TLBI _ | I_AT _ | I_UBFM _
104104
| I_UDF _| I_UNSEAL _ | I_ADDSUBEXT _ | I_ABS _ | I_REV _ | I_EXTR _
105105
| I_MOPL _ | I_MOP _
106+
| I_WFE | I_SEV | I_SEVL
106107
| I_WHILELT _ | I_WHILELE _ | I_WHILELO _ | I_WHILELS _
107108
| I_UADDV _
108109
| I_LD1SP _ | I_LD2SP _ | I_LD3SP _ | I_LD4SP _
@@ -290,7 +291,8 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
290291
| I_CASBH (v,_,_,_,_) | I_SWPBH (v,_,_,_,_)
291292
| I_LDOPBH (_,v,_,_,_,_) | I_STOPBH (_,v,_,_,_) ->
292293
Some (bh_to_sz v)
293-
| I_NOP|I_B _|I_BR _|I_BC (_, _)|I_CBZ (_, _, _)
294+
| I_NOP | I_WFE | I_SEV | I_SEVL
295+
| I_B _|I_BR _|I_BC (_, _)|I_CBZ (_, _, _)
294296
| I_CBNZ (_, _, _)|I_BL _|I_BLR _|I_RET _|I_ERET| I_SVC _ | I_LDAR (_, _, _, _)
295297
| I_TBNZ(_,_,_,_) | I_TBZ (_,_,_,_) | I_MOVZ (_,_,_,_) | I_MOVK(_,_,_,_)
296298
| I_MOVN _
@@ -350,6 +352,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
350352
| I_FENCE _
351353
| I_IC _|I_DC _|I_TLBI _ | I_AT _
352354
| I_NOP|I_TBZ _|I_TBNZ _
355+
| I_WFE | I_SEV | I_SEVL
353356
| I_BL _ | I_BLR _ | I_RET _ | I_ERET | I_SVC _ | I_UDF _
354357
| I_ST1SP _ | I_ST2SP _ | I_ST3SP _ | I_ST4SP _
355358
| I_ST1SPT _ | I_CTERM _
@@ -450,7 +453,8 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
450453
| I_LDARBH (bh,(XX|AX),_,_) -> MachSize.Ld (bh_to_sz bh)
451454
| I_STXR _|I_STXRBH _ | I_STXP _ -> MachSize.St
452455
| I_LDAR (_, (AA|AQ), _, _)|I_LDARBH (_, (AA|AQ), _, _)
453-
| I_NOP|I_B _|I_BR _|I_BC _|I_CBZ _|I_CBNZ _
456+
| I_NOP | I_WFE | I_SEV | I_SEVL
457+
|I_B _|I_BR _|I_BC _|I_CBZ _|I_CBNZ _
454458
| I_TBNZ _|I_TBZ _|I_BL _|I_BLR _|I_RET _|I_ERET | I_SVC _
455459
| I_UBFM _ | I_SBFM _
456460
| I_LDR _|I_LDRSW _|I_LDRS _|I_LDUR _|I_LD1 _|I_LDAP1 _

‎herd/AArch64Sem.ml‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -560,6 +560,16 @@ module Make
560560
if mixed then fun _sz -> write_reg
561561
else write_reg_sz
562562

563+
(* Create a symbolic event register for a given proc id `proc_id` *)
564+
let ev_loc proc_id =
565+
A.Location_global (V.Val (Constant.mk_ev_reg (Printf.sprintf "%d" proc_id)))
566+
567+
(* Write to the event register of a given proc id `proc_id`, a given value `v` *)
568+
let set_ev proc_id v ii =
569+
M.write_loc
570+
(mk_write quad Annot.N aexp Access.VIR (V.intToV v))
571+
(ev_loc proc_id) ii
572+
563573
(* Emit commit event *)
564574
let commit_bcc ii = M.mk_singleton_es (Act.Commit (Act.Bcc,None)) ii
565575
and commit_pred_txt txt ii =
@@ -3644,12 +3654,40 @@ Arguments:
36443654
let nextSet = B.nextSetT
36453655
(* And now, just forget about >>! *)
36463656
let [@warning "-32"](>>!) (_:unit) (_:unit) = ()
3657+
let ev_loc proc_id =
3658+
A.Location_global (V.Val (Constant.mk_ev_reg (Printf.sprintf "%d" proc_id)))
36473659

36483660
let do_build_semantics test inst ii =
36493661
let open AArch64Base in
36503662
match inst with
36513663
| I_NOP ->(* Instructions nop and branch below do not generate events, use a placeholder *)
36523664
!(M.mk_singleton_es (Act.NoAction) ii)
3665+
(* Event Register Instructions *)
3666+
| I_WFE ->
3667+
let loc = ev_loc ii.A.proc in
3668+
let read_ev = M.read_loc Port.No (mk_read quad Annot.N aexp) loc ii in
3669+
let rec wfe_loop n =
3670+
if n <= 0 then M.zeroT
3671+
else
3672+
M.altT
3673+
(* Read 1: clear and proceed *)
3674+
(M.seq_mem
3675+
(read_ev >>= fun v -> M.eqT v (V.intToV 1))
3676+
(set_ev ii.A.proc 0 ii)
3677+
>>= fun ((), ()) -> M.unitT ())
3678+
(* Read 0: loop *)
3679+
(M.seq_mem
3680+
(read_ev >>= fun v -> M.eqT v (V.intToV 0))
3681+
(wfe_loop (n-1))
3682+
>>= fun ((), ()) -> M.unitT ())
3683+
in
3684+
!(wfe_loop 3)
3685+
| I_SEV ->
3686+
let all_procs = List.map (fun (p, _, _) -> p) test.Test_herd.start_points in
3687+
let writes = List.map (fun p -> set_ev p 1 ii) all_procs in
3688+
!!!(List.fold_right (>>::) writes (M.unitT []) >>| M.unitT ())
3689+
| I_SEVL ->
3690+
!(set_ev ii.A.proc 1 ii)
36533691
(* Branches *)
36543692
| I_B l ->
36553693
M.mk_singleton_es (Act.NoAction) ii

‎herd/archExtra_herd.ml‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -495,16 +495,19 @@ module Make(C:Config) (I:I) : S with module I = I
495495
(* | (System (TAG,s1),System (TAG,s2)) *)
496496
-> Misc.string_eq s1 s2
497497
(* One id allowed, the other on forbidden, does not match *)
498-
| (Virtual _,(System ((PTE|TLB|PTE2),_)|Physical _|TagAddr _))
499-
| ((TagAddr _|Physical _|System ((PTE|TLB|PTE2),_)),Virtual _)
498+
| (Virtual _,(System ((PTE|TLB|PTE2),_)|Physical _|TagAddr _|EventReg _))
499+
| ((TagAddr _|Physical _|System ((PTE|TLB|PTE2),_)|EventReg _),Virtual _)
500500
| (System (PTE,_),System ((TLB|PTE2),_))
501501
| (System ((TLB|PTE2),_),System (PTE,_))
502-
| ((Physical _|TagAddr _),System (PTE,_))
503-
| (System (PTE,_),(TagAddr _|Physical _))
502+
| ((Physical _|TagAddr _|EventReg _),System (PTE,_))
503+
| (System (PTE,_),(TagAddr _|Physical _|EventReg _))
504+
| (EventReg _, (System _|Physical _|TagAddr _))
505+
| ((System _|Physical _|TagAddr _), EventReg _)
504506
-> false
505507
(* Both forbidden, failure *)
506508
| (TagAddr _|Physical _|System ((TLB|PTE2),_)),
507509
(TagAddr _|Physical _|System ((TLB|PTE2),_))
510+
| (EventReg _),(EventReg _)
508511
->
509512
Warn.fatal
510513
"Illegal id (%s or %s) in fault"
@@ -860,6 +863,11 @@ module Make(C:Config) (I:I) : S with module I = I
860863
(pp_location loc)
861864
| Location_global (I.V.Val (Symbolic (Virtual _|Physical _)))
862865
| Location_reg _ -> reg_default_value
866+
| Location_global (I.V.Val (Symbolic (EventReg _)))
867+
->
868+
Warn.user_error
869+
"No default value defined for location %s\n"
870+
(pp_location loc)
863871

864872
let get_of_val st a = State.safe_find I.V.zero (Location_global a) st
865873

‎herd/machAction.ml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ end = struct
9797
let open Constant in
9898
function
9999
| A.Location_reg _ -> REG
100-
| A.Location_global (V.Val (Symbolic (Virtual _))|V.Var _)
100+
| A.Location_global (V.Val (Symbolic (Virtual _|EventReg _))|V.Var _)
101101
-> Access.VIR
102102
| A.Location_global (V.Val (Symbolic ((System ((PTE|PTE2),_))))) as loc
103103
->
@@ -277,6 +277,9 @@ end = struct
277277
| _ -> false
278278
end
279279
| _ -> false
280+
let is_evreg a = match a with
281+
| Access (_, A.Location_global (A.V.Val (Constant.Symbolic (Constant.EventReg _))), _, _, _, _, _) -> true
282+
| _ -> false
280283
let is_pt_data = function
281284
| Access (_,A.Location_global (A.V.Val c),_,_,_,_,Access.PTE DISide.Data) ->
282285
Constant.is_pt c
@@ -559,6 +562,7 @@ end = struct
559562
in
560563
("T",is_tag)::
561564
("TLBI",is_inv)::
565+
("EVREG",is_evreg)::
562566
("no-loc", fun a -> Misc.is_none (location_of a))::
563567
(if kvm then
564568
fun k ->

‎herd/semExtra.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -302,6 +302,7 @@ module Make(C:Config) (A:Arch_herd.S) (Act:Action.S with module A = A)
302302
* (2) to ensure is_non_mixed_offset works with that *)
303303
| Physical (s,o) -> is_non_mixed_offset test s o
304304
| TagAddr _
305+
| EventReg _
305306
| System ((PTE|PTE2|TLB),_) -> true
306307

307308
(* Exported labels:

‎herd/test_herd.ml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,7 @@ module Make(A:Arch_herd.S) =
8787
| Physical (name, _) -> StringSet.add name acc
8888
| TagAddr (_, name, _) -> StringSet.add name acc
8989
| System (_, name) -> StringSet.add name acc
90+
| EventReg name -> StringSet.add name acc
9091
end
9192
| PteVal p ->
9293
let open ParsedPteVal in
@@ -259,6 +260,15 @@ module Make(A:Arch_herd.S) =
259260
fun addr -> IntMap.safe_find Label.Set.empty addr instr2labels in
260261
let type_env = A.build_type_env init in
261262
let init_state = A.build_state type_env init in
263+
(* Initialize event registers for each thread *)
264+
let init_state =
265+
List.fold_left
266+
(fun env (proc, _, _) ->
267+
let loc = A.Location_global
268+
(A.V.cstToV (Constant.mk_ev_reg (string_of_int proc))) in
269+
let v = A.V.intToV 0 in
270+
A.state_add env loc v)
271+
init_state starts in
262272
let flocs,ffaults = LocationsItem.locs_and_faults locs in
263273
let displayed =
264274
let flocs = A.RLocSet.of_list flocs in

‎jingle/AArch64Arch_jingle.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@ include Arch.MakeArch(struct
300300
end in
301301

302302
function
303-
| (I_FENCE _|I_NOP|I_RET None|I_ERET|I_SVC _|I_UDF _) as i -> unitT i
303+
| (I_FENCE _|I_NOP|I_WFE|I_SEV|I_SEVL|I_RET None|I_ERET|I_SVC _|I_UDF _) as i -> unitT i
304304
| I_B l ->
305305
find_lab l >! fun l -> I_B l
306306
| I_BR r ->

‎lib/AArch64Base.ml‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1354,6 +1354,10 @@ let pp_imm n = "#" ^ string_of_int n
13541354

13551355
type 'k kinstruction =
13561356
| I_NOP
1357+
(* Event Register Instructions *)
1358+
| I_SEV
1359+
| I_SEVL
1360+
| I_WFE
13571361
(* Branches *)
13581362
| I_B of lbl | I_BR of reg
13591363
| I_BC of condition * lbl
@@ -2105,6 +2109,10 @@ let do_pp_instruction m =
21052109

21062110
fun i -> match i with
21072111
| I_NOP -> "NOP"
2112+
(* Event Register Instructions *)
2113+
| I_WFE -> "WFE"
2114+
| I_SEV -> "SEV"
2115+
| I_SEVL -> "SEVL"
21082116
(* Branches *)
21092117
| I_B lbl ->
21102118
sprintf "B %s" (pp_label lbl)
@@ -2617,7 +2625,7 @@ let fold_regs (f_regs,f_sregs) =
26172625

26182626
fun c ins -> match ins with
26192627
| I_NOP | I_B _ | I_BC _ | I_BL _ | I_FENCE _ | I_RET None | I_ERET | I_SVC _
2620-
| I_UDF _ | I_SMSTART (None) | I_SMSTOP (None)
2628+
| I_UDF _ | I_SMSTART (None) | I_SMSTOP (None) | I_WFE | I_SEV | I_SEVL
26212629
-> c
26222630
| I_CBZ (_,r,_) | I_CBNZ (_,r,_) | I_BLR r | I_BR r | I_RET (Some r)
26232631
| I_MOVZ (_,r,_,_) | I_MOVN (_,r,_,_) | I_MOVK (_,r,_,_)
@@ -2761,7 +2769,11 @@ let map_regs f_reg f_symb =
27612769

27622770
fun ins -> match ins with
27632771
| I_NOP
2764-
(* Branches *)
2772+
(* Event Register Instructions *)
2773+
| I_WFE
2774+
| I_SEV
2775+
| I_SEVL
2776+
(* Branches *)
27652777
| I_B _
27662778
| I_BC _
27672779
| I_FENCE _
@@ -3142,6 +3154,7 @@ let get_next =
31423154
-> tgt_cons Label.Next lbl
31433155
| I_BLR _|I_BR _|I_RET _ |I_ERET -> [Label.Any]
31443156
| I_NOP
3157+
| I_WFE | I_SEV | I_SEVL
31453158
| I_LDR _
31463159
| I_LDRSW _
31473160
| I_LDRS _
@@ -3558,6 +3571,9 @@ module PseudoI = struct
35583571

35593572
let parsed_tr i = match i with
35603573
| I_NOP
3574+
| I_WFE
3575+
| I_SEV
3576+
| I_SEVL
35613577
| I_B _
35623578
| I_BR _
35633579
| I_BC _
@@ -3757,6 +3773,9 @@ module PseudoI = struct
37573773
| I_ST4 _ | I_STZ2G _
37583774
-> 4
37593775
| I_NOP
3776+
| I_WFE
3777+
| I_SEV
3778+
| I_SEVL
37603779
| I_B _ | I_BR _
37613780
| I_BL _ | I_BLR _
37623781
| I_RET _

‎lib/AArch64Lexer.mll‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,10 @@ let check_name name =
3434
if O.debug then Printf.eprintf "Check: '%s'\n" name ;
3535
match name with
3636
| "nop"|"NOP" -> NOP
37+
(* Event Register Instructions *)
38+
| "wfe"|"WFE" -> WFE
39+
| "sev"|"SEV" -> SEV
40+
| "sevl"|"SEVL" -> SEVL
3741
(* Hints are NOPS in AArch64 *)
3842
| "hint"|"HINT" -> HINT
3943
(* Halt instructions are used by Debug mode, not needed here - NOP *)

‎lib/AArch64Parser.mly‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ let check_op3 op e =
9090

9191
/* Instructions */
9292
%token NOP HINT HLT
93+
%token WFE SEV SEVL
9394
%token TOK_B BR CBZ CBNZ TBZ TBNZ
9495
%token TOK_EQ TOK_NE TOK_GE TOK_GT TOK_LE TOK_LT
9596
%token TOK_CS TOK_CC TOK_MI TOK_PL TOK_VS TOK_VC TOK_HI TOK_LS TOK_AL
@@ -660,6 +661,10 @@ instr:
660661
| NOP { I_NOP }
661662
| HINT NUM { I_NOP }
662663
| HLT NUM { I_NOP }
664+
/* Event Register Instructions */
665+
| WFE { I_WFE }
666+
| SEV { I_SEV }
667+
| SEVL { I_SEVL }
663668
/* Branch */
664669
| TOK_B label_addr { I_B $2 }
665670
| BR xreg { I_BR $2 }

0 commit comments

Comments
 (0)