Memory Model For rs2

[mehnadnerd]

The current proposal states This instruction behaves as if there is a conditional branch dependent on rs2..., and mentions the syntactic dependency on rs1 is only preserved if the condition is met. This would seem to imply that there is a control dependency from rs2 to rd, but the text does not specify this.

[ptomsich]

@aswaterman Could you respond to this?

/assign @aswaterman

[aswaterman]

The stated equivalence to the branch-based sequence should answer this question.

[aswaterman]

Thinking about this some more, I believe it's technically true that the statement that "This instruction behaves as if there is a conditional branch dependent on rs2 [...]" suffices to indicate there's a control dependency on rs2. But it would probably be clearer to explicitly state it. @mehnadnerd can you prepare a PR that makes this clarification for both instructions?

[mehnadnerd]

I will do so--the additional thing I wanted to imply was that this is similar to the dependency on vl for vector instructions, where it will not apply additional ordering on future non-dependent stores. I will copy the wording from the vector specification.

[mehnadnerd]

https://github.com/riscv/riscv-zicond/pull/6

[ptomsich]

Thinking some more about this, I wonder if there is a control dependency (or it is only suggested by the equivalence of a branching structure).

Considering that these are unconditional arithmetic instructions, their true equivalence is either a lookup (as in the SAIL model) or the following arithmetic:

  czero.eqz rd, rs1, rs2 :=
     snez rmask, rs2
     neg rmask, rmask
     ori rd, rs1, rmask

Unless the slt*-family of instructions also has a control dependency, we should not claim one for czero.

[mehnadnerd]

There should be a control dependency, as opposed to a data dependency, to match the branch. If we wanted to match the slt family, we could make it DVT-invariant on rs2 (and always propagate the syntactic dependency on rs1) but that was explicitly decided against.

The term "control dependency" for operations like this, where there is an output register and no change in control flow, is currently underdefined, I have been talking with Andrew about it in the context of the V extension. The intent is that it will follow like other syntactic dependencies, but unlike address or data dependencies, will only be enforced to stores.

Since I copied the wording from the V extension, I don't think the lack of a formal definition of "control dependency" should block this extension, it can share the same formalisation.

[ptomsich]

There should be a control dependency, as opposed to a data dependency, to match the branch. If we wanted to match the slt family, we could make it DVT-invariant on rs2 (and always propagate the syntactic dependency on rs1) but that was explicitly decided against.

As far as I understand, the slt-family is also only DVT-invariant if the Zkt extension is present... but DVT should not affect the determination of whether there is a "control dependency".

The term "control dependency" for operations like this, where there is an output register and no change in control flow, is currently underdefined, I have been talking with Andrew about it in the context of the V extension. The intent is that it will follow like other syntactic dependencies, but unlike address or data dependencies, will only be enforced to stores.

"Control dependency" (at least in my reading) always implies that the "observable next program-counter" depends on the value. If an instruction unconditionally executes and advances to the same "next program-counter", we can only have a "data dependency". To make things more involved: the data-dependency may then feed into a control-dependency of a dependent branch — but that should be covered by the model for the dependent branch then, right?

I would suggest that we refine the wording/definition of "control dependency": the design of Zicond intentionally made its instructions unconditional (and the various discussions around the topic of control dependencies have arisen only from whether prediction of the output-value — and consequently the prediction of successive branches dependent on its output value — would be appropriate).

The situation seems to be common with other instructions, where data-prediction on the output could be used to predict a conditional branch (e.g. andi rd, rs1, #imm -> beqz/bnez).

I may be barking up an entirely wrong tree, though…

Since I copied the wording from the V extension, I don't think the lack of a formal definition of "control dependency" should block this extension, it can share the same formalisation.

[mehnadnerd]

The V extension has this sentence, which raises similar issues: "Instructions affected by the vector length register vl have a control dependency on vl, rather than a data dependency. Similarly, masked vector instructions have a control dependency on the source mask register, rather than a data dependency." The next program-counter does not depend on vl in this case, so the standard definition of "control dependency" cannot be used. I am working on creating a modification that is able to handle this case, I am tentatively calling it a "reconvergent control dependency" or "rcontrol dependency". It will need to be another type of syntactic dependency that is passed through operations, and we will need a PPO rule 11b that states ": b is a store, and b has a syntactic reconvergent control dependency on a". I think a similar expanded definition of a "control dependency" would be appropriate here. There are definitely some holes and work here, but I wanted to use the fact that we can copy from the V extension to kick that particular can down the road.

What I was trying to say with the DVT statements is that these conditional select statements are more like branches than bit manipulation. Not guaranteeing DVT was an example of how it was more similar to a branch, as is only propagating the syntactic dependency on rs1 if the condition passes.

[kdockser]

As mehnadnerd points out, these Zicond instructions are different from other instructions in that one of the operands (rs1) is not evaluated if the condition is true. For hardware, this means that the instruction can complete when the condition is true even if rs1 is not ready. Since the SAIL model is a Formal model, and not just a behavioral model, it's code should be changed to reflect the branch-like behavior of these instructions. This control dependency also needs to be indicated in any supplemental files for use in memory concurrency testing (e.g., RMEM and isla-axiomatic).

[ptomsich]

As mehnadnerd points out, these Zicond instructions are different from other instructions in that one of the operands (rs1) is not evaluated if the condition is true. For hardware, this means that the instruction can complete when the condition is true even if rs1 is not ready. Since the SAIL model is a Formal model, and not just a behavioral model, it's code should be changed to reflect the branch-like behavior of these instructions. This control dependency also needs to be indicated in any supplemental files for use in memory concurrency testing (e.g., RMEM and isla-axiomatic).

SAIL provides a formal model of the architecture, but you describe micro-architectural aspects in waiting (or not waiting) for the readiness of operands. That would require some sort of pipeline model (or at least readiness-constraints) to be expressed in the SAIL model.

As of today, the SAIL model can only model a branching behavior by updating the program-counter (something that is not an option here). SAIL always requires all architectural arguments to be ready (as they are parameters to the function call to EXECUTE).

[kdockser]

The conditional dependency is an architectural feature. The formal model must represent this as it is the golden specification and may be used for Formal verification with an implementation as well as for concurrency testing with the aid of other tools.

That said, it seems like the SAIL language is not able to handle such a conditional dependency at this time. It seems like this is a gap that should be addressed.

[mehnadnerd]

I agree with Ken's point that we need to model this properly in SAIL in order to properly match the semantics of this instruction. The current SAIL will not match the conditional dependency on rs1, which will be visible in the memory model. For czero.eqz, would let condition = X(rs2); result : xlenbits = if (condition == zeros()) then zeros() else X(rs1); X(rd) = result; work/be valid SAIL? We need to only read rs1 if the condition is met.

[mehnadnerd]

I've updated my proposed patch to have that conditional read. I am still working on the detailed memory model proposal, I expect to have a draft next week.

[mehnadnerd]

Here's my proposed addition to the memory model text. This would go into the memory model section. For Zicond itself, it would simply define rs2 as a reconvergent-control source. (Text in between the """ is for sentences that are intended to go directly into the memory model, the rest are explanatory).

Instruction I has destination register s. The associated memory operation of this is a.

Instruction J has source register r. The associated memory operation of this is b.

Instruction M has source register p and destination register q.

Instruction I is program-ordered before Instruction M, which is program-ordered before Instruction J.

Instructions can have three types of source registers: address, data, and (new!) reconvergent-control (rctrl). For example, loads have an address source register. Stores have both address and data source registers. Conditional zero operations have a reconvergent-control source register and a data source register.

A syntactic dependency means that it only depends on the syntax of the assembly, not its semantics. For example “xor rd, rs1, rs2”, even if rs1==rs2, so rd will always be zero, rd still has a syntactic dependency on rs1 and rs2.

A syntactic rctrl dependency is a syntactic dependency that goes through a rctrl source register or destination register.

"""

Instruction J has a syntactic rctrl dependency on instruction I via destination register s of I and source register r of J if either of the following hold:

a) s is the same as r, J has r as a rctrl-source, and no instruction program-ordered between I and J has r as a destination register

b) There is an instruction M program-ordered between I and J such that all of the following hold:

1. J has a syntactic rctrl dependency or syntactic dependency on M via destination register q and source register r

2. M has a syntactic rctrl dependency or syntactic dependency on I via destination register s and source register p

3. M carries a rctrl dependency from p to q

"""

"""

b (the memory operation associated with J) has a syntactic rctrl dependency on a (the memory operation associated with I) if

• r is an rctrl source register for J and J has a syntactic dependency or syntactic rctrl dependency on I via source register r

• r is an address source register for J and J has a syntactic rctrl dependency on I via source register r

• b is a store operation, r is a data source register for J, and J has a syntactic rctrl dependency on I via source register r

"""

Basically, this is the same definition as syntactic dependencies from the RISCV spec, except it is for things as a rctrl-source. The intent is that in a chain of dependencies, a single op where it is a rctrl source will make it an rctrl dependency.

"""

11b. b is a store, and b has a syntactic rctrl dependency on a

"""

[mehnadnerd]

@ptomsich were you going to accept my MR and close this issue? I thought that was what you were going to do based on our discussion.

[ptomsich]

Merged.

[aswaterman]

@mehnadnerd what’s next as far as defining these reconvergent control dependencies?

[mehnadnerd]

I haven't gotten a positive response from the memory model experts, I will try again.