Three histories, one rule
Three histories, one rule
precedence must hold and every read must see the latest preceding write
t0
t1
t2
t3
t4
t5
h1
write(1), t0 to t2
read to 1
LINEARIZABLE
h2
write(1), t0 to t2
read to 0 STALE
NOT LINEARIZABLE
stale after complete
write done before read starts: precedence forces order
h3
write(1), t0 to t5
read to 0, overlapping: allowed
LINEARIZABLE
completed write then later stale read: reject that order, keep searching the rest
overlapping operations linearize either way: h3 may return 0 or 1
timed-out write is indeterminate: the checker tries took-effect and never-did branches
legend: violet = writes, blue = reads, green = accepted, rose = rejected
a passing sample never proves the next execution: pair with probes and monitors