Scope: RISC-V LR/SC (the Zalrsc part of the A extension) on the course model with MSI.

If the bits match, must a conditional store succeed?

No. LR (load-reserved) reads X and records a reservation. SC (store-conditional) writes only if the reservation is still valid. A write by another core clears it even if the value returns to its old bits, the ABA case (the value changes from A to B and back to A, so equal bits hide an intervening write). The reservation tracks interference, not values.

The RISC-V contract

From the RISC-V unprivileged ISA, A extension chapter, which splits A into Zalrsc (LR/SC) and Zaamo (AMOs):

• SC writes nothing on failure. It writes 0 to rd on success and a nonzero value on failure.

• Every SC, successful or not, invalidates any reservation held by the hart.

• An SC must fail if its address is not in the reservation set of the most recent LR, or if another SC (to any address) lies between the LR and the SC in program order.

• An SC may succeed only if no store from another hart to the reservation set can be observed between the LR and the SC.

• The reservation set may be arbitrarily large, provided it includes all bytes of the addressed word or doubleword. An SC may also fail for implementation reasons, provided the progress guarantee below still holds.

A constrained LR/SC loop meets all of these conditions:

1. The loop contains only an LR/SC sequence and the code to retry it, at most 16 instructions placed sequentially in memory.

2. The dynamic code between the LR and the SC contains only base I instructions, excluding loads, stores, backward jumps, taken backward branches, JALR, FENCE and SYSTEM instructions. Compressed forms of those I instructions are also allowed.

3. The retry code may branch back to repeat the sequence but otherwise has the same restrictions.

4. The LR and SC addresses lie in a memory region with the LR/SC eventuality property.

5. The SC is to the same effective address and data size as the latest LR on that hart.

For such a loop, the execution environment must guarantee that eventually this hart or another hart executes a successful SC to the reservation set, or another hart or device writes to it, or this hart exits the loop or traps. That is system-wide progress, not freedom from starvation for each hart. If other harts keep writing the reservation set, no hart is guaranteed to leave its loop.

Reservations on the course model

Warm-up: C0's LR missed, sent GetS(X) and installed S / 0, so H has S{C0}. The LR returned 0 and recorded the reservation on X's line. (An LR may also fetch the line with GetM, to save the later upgrade.) C1 then stores to X.

C1's store is the write miss from S{C0} in Write Miss and Ownership, same roles. It is not redrawn. What is new happens at C0: the Inv that takes its S copy at step 2 also clears the reservation, so the later SC fails locally and sends no message.

The last row is after the write miss has completed and C1 has stored 1.

Had no Inv arrived, C0's SC would have needed M first: an upgrade GetM, then the write. The reservation does not give write permission, and holding M does not make a reservation valid.

Granularity: designs commonly reserve the whole line, because Inv and Fwd-GetM arrive per line. The architecture only requires the reservation set to cover the addressed bytes, so a store by C1 to another word of the same line may fail C0's SC. That is a false failure, which the specification allows.

Livelock and the usual remedy

If C0 and C1 alternate, each LR takes the line, and each SC's GetM steals it from the other before the other's SC: both reservations keep being cleared and both SCs keep failing. A common remedy (a general design guideline, not an ISA rule) is to hold the line for a bounded window after LR: incoming Inv or Fwd-GetM for it is deferred until the SC executes or a timeout expires. The bound keeps the deferred requester from waiting forever, and the constrained-loop rules are what make the window short enough to be useful.

The atomics lesson traces an AMO at the cache holding M and describes far atomics at the home in one paragraph; neither is redrawn here.

Check it: a line-granularity reservation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

LINE = 64                                # reservation granularity: one 64-byte line
mem = {}
res = {"line": None}                     # C0's reservation, or None

def lr(addr):
    res["line"] = addr // LINE
    return mem.get(addr, 0)

def snoop(addr):                         # Inv or Fwd-GetM for the line, or C0's own eviction
    if res["line"] == addr // LINE:
        res["line"] = None

def remote_write(addr, value):           # C1's GetM reaches H, H revokes C0's copy first
    snoop(addr)
    mem[addr] = value

def sc(addr, value):                     # returns rd: 0 on success, nonzero on failure
    ok = res["line"] is not None and res["line"] == addr // LINE
    res["line"] = None                   # every SC clears the reservation
    if ok:
        mem[addr] = value
    return 0 if ok else 1

X = 0x1000
assert lr(X) == 0
remote_write(X + 8, 5)                   # another word in the same line
assert sc(X, 1) != 0 and mem.get(X, 0) == 0          # false failure, nothing written
assert lr(X) == 0
remote_write(X + LINE, 5)                # a different line
assert sc(X, 1) == 0 and mem[X] == 1
assert lr(X) == 1
assert sc(X + 2 * LINE, 7) != 0 and (X + 2 * LINE) not in mem   # SC outside the reservation
assert sc(X, 2) != 0 and mem[X] == 1     # the earlier SC cleared the reservation
assert lr(X) == 1
snoop(X)                                 # Inv delivered for the line
assert sc(X, 2) != 0 and mem[X] == 1
assert lr(X) == 1
remote_write(X, 2)                       # ABA: C1 writes 2, then restores 1
remote_write(X, 1)
assert mem[X] == 1 and sc(X, 3) != 0 and mem[X] == 1
assert lr(X) == 1 and sc(X, 3) == 0 and mem[X] == 3
print("PASS: line reservations fail on same-line writes, Inv, intervening SC and ABA, and survive other lines")

The model returns rd as RISC-V does: 0 for success, nonzero for failure. It checks a false failure from a same-line write, success across a write to another line, an intervening SC, an Inv, and the ABA case.

Related topics

• Shared course model

• Prerequisite: atomics and RMW at the cache