A.7Known Issues: Mixed-Size RSW

Part I Linux boot: optional Vol. I (Unprivileged) pp. 626–627 · ~2 min read

The appendix closes with honesty: one known family of tests where RVWMO’s two formalizations (the axiomatic herd model and the operational model of Appendix B) disagree — mixed-size RSW variants, where loads of different widths partially overlap.

Mixed-size RSW (Table 94, simplified)Initially: x = 0; y = doubleword at s1 (words y0, y1)

Hart 0

  1. li t1, 1
  2. (a) lw a0,0(s0)
  3. (b) fence rw,rw
  4. (c) sw t1,0(s1)

Hart 1

  1. (d) ld a1,0(s1)
  2. (e) lw a2,4(s1)
  3. xor a3,a2,a2
  4. add s0,s0,a3
  5. (f) sw t1,0(s0)
a0=1, a1=1, a2=0 — ALLOWEDPermitted by the axiomatic models, FORBIDDEN by the operational model — the known discrepancy. The RSW same-store reasoning gets slippery when access sizes differ.

The candidate fix is a new PPO rule — in herd syntax, (po-loc & rsw);ppo;[W] — ordering a load before a later store whenever an intervening RSW-paired load is PPO-ordered before that store. It is not official, but the spec’s advice to implementers is unambiguous:

Many implementations will already enforce this ordering naturally. As such, even though this rule is not official, we recommend that implementers enforce it nevertheless in order to ensure forwards compatibility.

Hardware Designer Notes

The meta-lesson for a verification plan: run BOTH reference models (herd axiomatic and the operational simulator) against your RTL, and when they disagree on a mixed-size test, agree with the stricter one. That closes uA; Appendix B formalizes everything this appendix explained in prose.

Minimal Linux-boot hart MUST

  • Nothing today — both behaviors are currently conformant

MAY simplify / trap-and-emulate

  • Enforce the proposed (po-loc & rsw);ppo;[W] ordering now — in-order LSUs and most OoO designs already do — and be forward-compatible if it is ratified

Check yourself — known issues

1.The mixed-size RSW family exposes a discrepancy between RVWMO's two formalizations. Which way does it cut?

2.What should an implementer do about the proposed-but-unofficial mixed-size RSW rule?

2 questions