Memory consistency models: Worked examples — Hinglish deep dive

5.4.16 · D3 · Hardware › Memory Hierarchy & Caches › Memory consistency models

Intuition Yeh page kya hai

Parent note ne tumhe rulebook diya. Yeh page us rulebook ke har cell ko exercise karta hai: har model (SC → TSO → Weak), har reordering pair (L→L, L→S, S→S, S→L), degenerate cases (ek core, koi sharing nahi), limiting case (sab kuch fenced), aur twists (transitivity, IRIW). Is page ke baad koi bhi litmus test tumhe surprise nahi kar sakta.

Shuru karne se pehle ek vocabulary reminder, taaki koi bhi symbol unexplained na rahe:

Ek load L = memory se ek read. Ek store S = memory mein ek write.
Program order = wo top-to-bottom order jisme instructions ek core ke liye likhe gaye hain.
Globally visible = wo moment jab har doosra core us effect ko observe kar sake.
Notation $a <_{m} b$ ko yun padho: " $a$ , $b$ se pehle hota hai us ek sach-wale global order mein jise memory system commit karta hai." Subscript $m$ = "memory order".

The scenario matrix

Har litmus test jo hum face kar sakte hain wo is table ki ek row hai. Neeche ke 8 examples ka goal hai har cell ko kam se kam ek baar fill karna.

#	Case class	Concrete question	Models that differ here
A	S→L reorder (store buffer)	Store-Buffering: kya dono loads stale 0 read kar sakte hain?	SC=No, TSO/x86=Yes
B	S→S reorder	Message-passing flag: kya consumer flag dekh sakta hai lekin stale data?	SC/TSO=No, Weak=Yes
C	L→L reorder	Load-buffering: kya do loads apne stores se pehle reorder ho sakte hain?	SC/TSO=No, Weak=Yes
D	Degenerate: single core	Kya ek core apne khud ke ops ko kabhi out of order dekhta hai?	All models: No
E	Degenerate: no sharing	Do cores, disjoint addresses — koi interaction?	All models: No
F	Cycle test (proof)	Prove karo ki SC, SB ke bad outcome ko forbid karta hai	SC only
G	Multi-copy atomicity (IRIW)	Kya do readers do writes ke order par agree karte hain?	SC/TSO=Yes agree, POWER/ARM=No
H	Limiting case: full fences	`MFENCE` insert karo — kya TSO, SC recover kar leta hai?	recovers SC
I	Real-world twist	Spin-lock acquire/release correctness	needs acquire/release
J	Exam twist: transitivity	WWC / cumulative barriers across 3 cores	Weak needs cumulative fence

Example A — Store→Load reorder (cell A)

Worked example Store-Buffering (Dekker core)

Init x = 0, y = 0.

Core 1	Core 2
`x = 1` (S1)	`y = 1` (S3)
`r1 = y` (L2)	`r2 = x` (L4)

x86 (TSO) par, kya hum r1 == 0 && r2 == 0 ke saath finish kar sakte hain?

Forecast: aage padhne se pehle Yes ya No guess karo.

Answer: Yes.

Kya: S1, x=1 write karta hai lekin value pehle Core 1 ke store buffer mein jaati hai, memory mein nahi. Yeh step kyun? TSO ki sirf ek relaxation hai ki ek store buffered baith sakta hai jab core aage race karta hai — yeh S→L cell hai.
Kya: L2, y padhta hai. Memory mein abhi bhi y=0 hai (S3 bhi Core 2 ke buffer mein atak gaya hai). To r1 = 0. Kyun: doosre core par buffered store abhi globally visible nahi hai.
Kya: Symmetrically, L4, x=0 padhta hai, to r2 = 0. Kyun: dono cores ne ek saath yahi trick ki — yeh store buffer ka poora point hai.

Verify: SC ke under yeh impossible hai (Example F prove karta hai). TSO ke under do buffered stores plus do early loads exactly (r1,r2) = (0,0) dete hain. Yeh parent ke canonical claim se match karta hai. ✅

Example B — Store→Store reorder (cell B)

Worked example Weak hardware par message passing

Init data = 0, flag = 0.

Core 1 (producer)	Core 2 (consumer)
`data = 42` (S1)	`while(flag==0){}` (L3)
`flag = 1` (S2)	`r = data` (L4)

ARM (weak) par, jab consumer flag==1 dekhe, kya r == 0 ho sakta hai?

Forecast: Yes ya No?

Answer: Yes — r stale 0 ho sakta hai.

Kya: Weak hardware par S1 aur S2 ka koi S→S ordering nahi — flag=1, Core 2 tak data=42 se pehle pahunch sakta hai. Yeh step kyun? Yeh S→S cell hai; TSO ise forbid karta hai, ARM nahi karta.
Kya: Consumer ka loop L3, flag==1 dekhta hai, exit karta hai, phir L4, data padhta hai — lekin data=42 abhi propagate nahi hua, to r=0. Kyun: dono writes independently travel kiye.
Fix: producer, S1 aur S2 ke beech ek release fence insert karta hai; consumer, L3 ke baad ek acquire fence insert karta hai. Dekho Memory Barriers and Fences aur C++ Memory Model (acquire-release). Kyun: ek release-acquire pair us S→S / L→L ordering ko recreate karta hai jo algorithm ko chahiye.

Verify: TSO/x86 par S→S preserved hai, to r guaranteed 42 hai — pattern wahan bina fence ke kaam karta hai. ARM par bina fences ke r ∈ {0, 42}. Weak par dono outcomes legal hain, TSO par sirf 42. ✅

Example C — Load→Load reorder (cell C)

Answer: Sirf Weak (ARM/POWER) par; SC aur TSO par No.

Kya: r1==1 matlab L1 ne wo value padhi jo S4 ne likhi. r2==1 matlab L3 ne wo value padhi jo S2 ne likhi. Yeh step kyun? Hum pooch rahe hain ki kya ek load effectively uske neeche wale store ke baad slide kar sakta hai — L→S / L→L relaxation.
Kya: Iske liye, S4 L1 se pehle visible honi chahiye, aur S2, L3 se pehle — lekin program order mein L1<S2 aur L3<S4 hai. Kyun: SC/TSO par loads kabhi same core ke baad wale stores ko bypass nahi karte, to koi bhi core apna store apne earlier load ke complete hone se pehle publish nahi kar sakta.
Kya: ARM par load ko store ke past delay/speculate kiya ja sakta hai, dono 1s ko allow karte hue. Kyun: weak models by default L→L aur L→S ordering drop kar dete hain.

Verify: SC/TSO table rows dono L→S = ✅ dikhate hain, to LB ka (1,1) wahan impossible hai; ARM ki row sab ❌ hai to wahan allowed hai. ✅

Example D — Single core khud ko order mein dekhta hai (cell D)

Worked example Ek core apni khud ki writes padh raha hai

x = 5     (S1)
r = x     (L2)

r kya hai?

Forecast: kya ek store buffer kabhi purani value wapas de sakta hai yahan?

Answer: r = 5, hamesha, har model par.

Kya: TSO mein bhi store x=5 buffer mein baith jaata hai, lekin same address ka baad wala load pehle buffer check karta hai — store forwarding. Yeh step kyun? Yeh degenerate single-core case hai; consistency models sirf yeh govern karte hain ki doosre cores kya dekhte hain, khud core ka apna view nahi.
Kya: To L2, drain timing se independent, fresh value 5 dekhta hai. Kyun: har model per-core, per-address program order preserve karta hai — yeh Cache Coherence guarantee plus store forwarding hai, dekho Store Buffers and Write Buffering.

Verify: r = 5. Koi model yahan r = 0 allow nahi karta. Yeh woh invariant hai jo single-threaded code ko correct rakhta hai. ✅

Worked example Disjoint addresses

Init a=0, b=0. Core 1 sirf a touch karta hai; Core 2 sirf b touch karta hai.

Core 1	Core 2
`a = 1` (S1)	`b = 1` (S3)
`r1 = a` (L2)	`r2 = b` (L4)

Final (r1, r2)?

Answer: (1, 1) har model par.

Kya: Har core sirf apna address padhta hai, jo usne abhi likha. Yeh step kyun? Koi shared address nahi hone se consistency model ke paas constraint karne ke liye kuch nahi — yeh do independent single-core programs mein degenerate ho jaata hai (cell D do baar).
Kya: Store forwarding har r ko uske apne core ki fresh write deta hai. Kyun: cross-core ordering rules tab fire nahi hote jab koi location shared nahi hoti.

Verify: (r1, r2) = (1, 1). Reordering sharing ke bina invisible hai. ✅

Example F — Cycle proof: SC, SB ke bad outcome ko forbid karta hai (cell F)

Kya: r1==0 ⇒ single total order $<_{m}$ mein, load L2 (y padhna) store S3 (y likhna) se pehle aaya. To $L 2 <_{m} S 3$ . Yeh step kyun? SC ek ऐसा ek total order deta hai jo har program order se consistent ho; initial 0 return karne wala load us store se pehle hona chahiye jo use change karta.
Kya: r2==0 ⇒ isi tarah $L 4 <_{m} S 1$ .
Kya: Program order force karta hai $S 1 <_{m} L 2$ (Core 1) aur $S 3 <_{m} L 4$ (Core 2). Kyun: SC kisi core ke khud ke operations ko kabhi reorder nahi karta.
Kya: Unhe chain karo: $S 1 <_{m} L 2 <_{m} S 3 <_{m} L 4 <_{m} S 1$ . Kyun: charon facts ko head-to-tail substitute karo.
Kya: Yeh kehta hai $S 1 <_{m} S 1$ — ek cycle. Ek total order antisymmetric hota hai, to yeh contradiction hai. ∎

Verify: Dependency graph mein ek 4-node directed cycle hai, to koi total order exist nahi karta ⇒ SC, (0,0) ko forbid karta hai. Isliye store buffers (TSO) SC se strictly weaker hain. ✅

Example G — Kya do readers agree karte hain? IRIW (cell G)

Worked example Independent Reads of Independent Writes

Init x=0, y=0.

C1	C2	C3	C4
`x=1` (S1)	`y=1` (S2)	`r1=x` (L3)	`r3=y` (L5)
		`r2=y` (L4)	`r4=x` (L6)

Kya r1=1, r2=0, r3=1, r4=0 ho sakta hai (C3 pehle x dekhta hai, C4 pehle y dekhta hai)?

Forecast: Yes ya No?

Answer: SC aur TSO par No. POWER/ARM (non-multi-copy-atomic) par Yes.

Kya: Yeh outcome poochta hai ki kya do independent writes alag-alag readers dwara alag-alag orders mein observe ki jaati hain. Yeh step kyun? Yeh kisi bhi single-core reordering se zyada strong property hai — yeh is baare mein hai ki kya ek single global store order exist bhi karta hai.
Kya: SC/TSO dono stores ko ek total store order mein commit karte hain, to sab readers agree karte hain ⇒ yeh outcome impossible hai. Kyun: "single total order" exactly wahi hai jo SC/TSO stores ke baare mein promise karte hain.
Kya: POWER/ARM, x=1 ko C3 tak jaldi propagate kar sakta hai jabki y=1, C4 tak jaldi pahunchta hai — writes multi-copy-atomic nahi hain. Kyun: weak interconnects writes ko alag-alag cores tak alag-alag times par deliver karte hain.

Verify: SC/TSO, split-observation (1,0,1,0) ko forbid karte hain; POWER/ARM ise allow karte hain. Weak hardware par agreement recover karne ke liye ek cumulative barrier chahiye (cell J). ✅

Example H — Limiting case: fences SC recover kar lete hain (cell H)

Worked example SB with a fence on each core

SB (Example A) lo aur har store aur load ke beech ek MFENCE insert karo:

Core 1	Core 2
`x = 1` (S1)	`y = 1` (S3)
`MFENCE`	`MFENCE`
`r1 = y` (L2)	`r2 = x` (L4)

x86 par, kya ab r1==0 && r2==0 ho sakta hai?

Answer: Nahi — fences is test ke liye SC restore kar dete hain.

Kya: MFENCE store buffer drain karta hai, S1 ko L2 execute hone se pehle globally visible hone pe majboor karta hai. Yeh step kyun? Yeh limiting case hai: TSO ki ek relaxation (S→L) ko wapas on karne se locally full SC ordering milti hai. Dekho Memory Barriers and Fences aur Atomic Operations and Locks.
Kya: Ab global order mein kam se kam ek store truly pehle hai, to dono loads 0 nahi padh sakte — Example F ka cycle argument reuse karo. Kyun: S→L re-enforce hone ke baad, SB ordering graph (0,0) ke liye acyclically impossible hai.

Verify: Fences ke saath, TSO ka L→L, L→S, S→S, aur S→L sab enforce hain ⇒ table row SC ke barabar ⇒ (0,0) forbidden. Fence woh "dial" hai jo TSO se SC tak wapas jaata hai. ✅

Example I — Real-world twist: ek spin-lock (cell I)

Worked example Acquire/release lock

// acquire:  while ( test_and_set(lock) ) {}      // ACQUIRE
//   ... critical section reads/writes shared data ...
// release:  store(lock, 0)                        // RELEASE

ARM par, kya critical section ke memory ops lock ke andar rahenge?

Forecast: kya lock akele yeh guarantee karta hai?

Answer: Sirf tab jab test_and_set ke paas acquire semantics hon aur release store ke paas release semantics hon.

Kya: ARM par ek plain load/store lock, critical-section reads ko acquire ke upar hoist hone deta hai (L→L relaxed) ya writes ko release ke neeche sink hone deta hai (S→S relaxed). Yeh step kyun? Ordering ke bina, doosra thread "unlocked" state observe kar sakta hai jabki hamare writes abhi in-flight hain — shared data corrupt ho sakta hai.
Kya: Acquire = koi baad wala op uske pehle reorder nahi ho sakta. Release = koi pehle wala op uske baad reorder nahi ho sakta. Kyun: saath milke yeh ek one-way fence pair banate hain jo critical section ko box karta hai — exactly C++ Memory Model (acquire-release) ki guarantee.
Kya: x86/TSO par ek LOCK-prefixed test-and-set already buffer drain karta hai, to lock wahan weaker source annotations ke saath kaam karta hai. Kyun: TSO mein sirf S→L ki kami thi, jo locked atomic fix kar deta hai.

Verify: lock-in par acquire + lock-out par release ⇒ har critical-section op unke beech ordered hai ⇒ koi leak nahi. Yeh weak models ke under mutual exclusion ka standard correctness proof hai. ✅

Example J — Exam twist: transitivity / cumulativity (cell J)

Worked example 3 cores ke across Write-to-Read Causality (WRC)

Init x=0, y=0.

C1	C2	C3
`x = 1` (S1)	`r1 = x` (L2)	`r2 = y` (L4)
	`y = 1` (S3)	`r3 = x` (L5)

Agar r1==1 aur r2==1 hai, to kya r3==1 zaroor hoga?

Forecast: kya causality middle core ke through chain hoti hai?

Answer: SC/TSO par haan. Plain ARM/POWER par nahi jab tak C2 ki fence cumulative na ho.

Kya: r1==1 matlab C2 ne C1 ka x=1 dekha; phir C2 ne y=1 publish kiya; r2==1 matlab C3 ne woh y dekha. Yeh step kyun? Intuitively causality ko C1→C2→C3 chain ke through x=1 carry karni chahiye.
Kya: Non-multi-copy-atomic hardware par, x=1 abhi bhi C3 tak nahi pahuncha hoga chahe y=1 pahunch gaya ho, to r3 0 ho sakta hai. Kyun: ordinary barriers sirf fencing core ke khud ke ops order karte hain; yeh force nahi karte ki pehle observed writes bhi propagate hon — woh zyada strong property cumulativity hai.
Kya: Ek cumulative release fence (e.g. ARM dmb ish / release store) force karta hai ki C1 ka x=1, C2 ke y=1 se pehle propagate ho, to r3 1 hona chahiye. Kyun: cumulativity fence ki reach un writes tak extend karti hai jo core ne padhi hain, na sirf likhi hain.

Verify: SC/TSO: single store order ⇒ r3 1 forced hai. Plain weak: r3 ∈ {0,1}. C2 par cumulative fence ⇒ r3 = 1. Yeh classic "barriers automatically transitive nahi hote" exam trap hai. ✅

Recall Har example kaun sa cell hit karta hai?

Example A kaun sa reordering pair hit karta hai? ::: S→L (store buffer) Example B kaun sa pair relax karta hai, aur sirf kaun se model par? ::: S→S, sirf Weak/ARM par Example C (Load-Buffering) kaun se models par impossible hai? ::: SC aur TSO Example F impossibility prove karne ke liye kaun si graph property use karta hai? ::: memory order mein ek directed cycle IRIW (G) kaun si hardware property distinguish karta hai? ::: multi-copy atomicity (single vs. per-core store propagation) Example H dikhata hai ki ek fence TSO ko kaun se model tak dial karta hai? ::: Sequential Consistency (SC) Example J ka trap yeh hai ki ordinary barriers mein kaun si property nahi hoti? ::: cumulativity (cores ke across transitivity)

Back to Memory consistency models · prerequisite recap: Out-of-Order Execution, Store Buffers and Write Buffering.

Core 1	Core 2
`r1 = x` (L1)	`r2 = y` (L3)
`y = 1` (S2)	`x = 1` (S4)