For these tiny tests, yes. X and Y are distinct locations in different 64-byte lines, initially 0, with no cached copies. C0 and C1 execute the operations below. Registers r1 and r2 record the two load results. A third test, SB with fences, puts a fence F between each core's store and load.
Test | C0 program order | C1 program order |
|---|---|---|
SB | W(X)=1, r1=R(Y) | W(Y)=1, r2=R(X) |
MP | W(X)=1, W(Y)=1 | r1=R(Y), r2=R(X) |
SB with fences | W(X)=1, F, r1=R(Y) | W(Y)=1, F, r2=R(X) |
SC explores every instruction interleaving while preserving each core's program order. TSO additionally explores one FIFO store buffer per core: stores append, drains update shared memory, and loads forward from the newest own matching buffered store. A fence F may execute only when its own core's buffer is empty, so it stalls younger operations until older stores have drained. Under SC there is no buffer and F does nothing. Buffers start empty. Terminal executions have finished both programs and drained both buffers. Draining after the loads does not change recorded register results. With fifo=False the model lets any buffered entry drain first: a deliberately broken TSO, used to show which rule forbids MP's (1,0).
def outcomes(programs, tso, fifo=True):
start = ((0, 0), (0, 0), ((), ()), (-1, -1))
todo, seen, found = [start], set(), set()
while todo:
state = todo.pop()
if state in seen:
continue
seen.add(state)
pcs, memory, buffers, registers = state
if all(pcs[c] == len(programs[c]) for c in range(2)) and not any(buffers):
found.add(registers)
continue
for c in range(2):
if pcs[c] < len(programs[c]):
op, address, argument = programs[c][pcs[c]]
p, m, b, r = list(pcs), list(memory), list(buffers), list(registers)
p[c] += 1
if op == "W":
if tso:
b[c] = b[c] + ((address, argument),)
else:
m[address] = argument
elif op == "R":
value = memory[address]
for a, v in reversed(buffers[c]):
if a == address:
value = v
break
r[argument] = value
if op != "F" or not buffers[c]:
todo.append((tuple(p), tuple(m), tuple(b), tuple(r)))
if tso:
for i in range(min(1, len(buffers[c])) if fifo else len(buffers[c])):
address, value = buffers[c][i]
m, b = list(memory), list(buffers)
m[address], b[c] = value, b[c][:i] + b[c][i + 1:]
todo.append((pcs, tuple(m), tuple(b), registers))
return found
F = ("F", 0, 0)
SB = ((("W", 0, 1), ("R", 1, 0)), (("W", 1, 1), ("R", 0, 1)))
SB_F = ((("W", 0, 1), F, ("R", 1, 0)), (("W", 1, 1), F, ("R", 0, 1)))
MP = ((("W", 0, 1), ("W", 1, 1)), (("R", 1, 0), ("R", 0, 1)))
sb_sc, sb_tso, sb_f_tso = outcomes(SB, False), outcomes(SB, True), outcomes(SB_F, True)
assert sb_sc == {(0, 1), (1, 0), (1, 1)}
assert sb_tso == sb_sc | {(0, 0)}
assert (0, 0) in sb_tso and (0, 0) not in sb_f_tso and sb_f_tso == sb_sc
assert outcomes(MP, False) == outcomes(MP, True) == {(0, 0), (0, 1), (1, 1)}
assert (1, 0) in outcomes(MP, True, fifo=False)
forward = ((("W", 0, 1), ("R", 0, 0)), (("W", 1, 1), ("R", 1, 1)))
assert outcomes(forward, False) == outcomes(forward, True) == {(1, 1)}
print("PASS: SC and TSO outcome sets, fences, FIFO draining and forwarding")Model and initial X = Y = 0 | SB (r1, r2) | SB with fences (r1, r2) | MP (r1, r2) |
|---|---|---|---|
SC | (0,1), (1,0), (1,1) | (0,1), (1,0), (1,1) | (0,0), (0,1), (1,1) |
TSO, FIFO buffers | SC's set plus (0,0) | SC's set: (0,0) forbidden again | Same as SC: (1,0) forbidden |
Broken TSO, any entry may drain | Not asserted | Not asserted | (1,0) becomes reachable |
The block runs in the course checks and prints PASS. It asserts the exact sets above. The separate forwarding test stops a model that ignores its own pending stores from passing. The broken-TSO row shows why MP is forbidden under TSO: FIFO draining plus ordered loads. If W(Y)=1 could drain before the older W(X)=1, C1 could read the new flag and the old payload.
It ensures each recorded execution can finish all its issued stores. The later drains preserve the observed registers, including SB's TSO 0,0 result; they do not retroactively change earlier loads.