[herd] Event Register Semantics

[RaghavRoy145]

Adds semantics for the event register instructions: WFE, SEV, SEVL

Summary

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. A new Constant.EventReg of string symbolic kind is introduced, initialised to 0 at test start in test_herd.ml. An Access.EVREG access kind is added so reads/writes to these locations can be distinguished from ordinary memory.

SEVL: a single write_loc of 1 to the current thread's event register.
SEV: iterates over test.start_points, emitting one write_loc 1 per thread's event register in parallel.
WFE: a bounded loop (wfe_loop 3) non-deterministically branches on the value read.

Tests

Not added

[diaolo01]

Thanks for this!
I'm confused by EventReg being modelled as a symbolic location and as a register. Architecturally, it is register, but software cannot access it through direct reads/writes. My current preference would be to model it as register state, while making sure it is not reachable through the ordinary architectural register access paths such as MRS/MSR.

[diaolo01]

Since the architectural behaviour is to read the Event Register, then either clear or continue waiting depending on that value, I think this should be restructured so the choice is made from the read's result.

[RaghavRoy145]

I did try a choiceT approach, and the problem I had was the edges between WFE events depend on which combinator we use (choiceT vs altT):

altT with seq_mem (current implementation): produces iico_order between successive reads and between the final read and write. This is seems correct since the data from the read doesn't flow to the next read or to the write (which always writes 0).

choiceT: produces iico_data throughout, since the value must flow through the condition check.

Which edges are preferred?

[diaolo01]

Thanks, this is helpful. I’m fairly convinced the edges we want here are order edges rather than data edges. I’m still uncomfortable with the current altT encoding though, because it duplicates the EVREG read across the two paths. I can’t yet fully justify that objection in terms of the graph relations, but it does not feel like the right abstraction: architecturally this is a single read followed by a guarded choice rather than two separate guarded reads.

[diaolo01]

I also found in the Arm ARM that: "The Event Register for the PE executing the Exception return instruction is set." This needs to be reflected in the ERET semantics.

[RaghavRoy145]

Thanks for this! I'm confused by EventReg being modelled as a symbolic location and as a register. Architecturally, it is register, but software cannot access it through direct reads/writes. My current preference would be to model it as register state, while making sure it is not reachable through the ordinary architectural register access paths such as MRS/MSR.

Thanks for the reviews!

Registers as they are currenlty implemented don't seem to allow writes from remote threads, and I get the following warning when I try this:

Ambiguous po for register 1:Event: (eeid=g action=W1:Eventq=1) and (eeid=i action=W1:Eventq=0) are not ordered.

A work-around for this is perhaps to have the local thread (to which the event register being written to belongs) write to its own register after SEV reads a 0 on the remote thread's event register, which doesn't sound faithful to the implementation where SEV acts like a broadcast write.

So for now I have implemented this as a global memory location. Unless it is worthwhile to create a type of a register that allows remote writes.

It could also be that I am missing something and using registers in a way where SEV can work correctly is already possible.

[RaghavRoy145]

I also found in the Arm ARM that: "The Event Register for the PE executing the Exception return instruction is set." This needs to be reflected in the ERET semantics.

This is interesting, this is perhaps an example of a "spurious" update, so the thread is woken up without an SEV, thanks for catching this!

For now I am going to implement it as a parallel write alongside the ELR read, unsure if this the right way to do it.

fun () ->
      (set_ev ii.A.proc 1 ii >>| read_reg_ord AArch64.elr_el1 ii)
      >>= fun ((), v) -> eret_to_addr v

[diaolo01]

Thanks, that makes sense. I understand that the current registers are not able to take cross threaded writes. However, I don't think modelling Event Registers as symbolic locations is the right abstraction. Architecturally, it's a hidden per-PE register, which is neither ordinary memory nor software accessible register. It feels like this needs to be a separate category of state/location that does not currently exist: something register-like and per-PE, but whose location still includes the target PE so that remote writes are possible.

[diaolo01]

This is interesting, this is perhaps an example of a "spurious" update, so the thread is woken up without an SEV, thanks for catching this!

I don’t think “spurious” is the right term here. The Arm ARM explicitly lists exception return as a cause that sets the Event Register, so this is an architected update. Modelling it alongside ERET makes sense.