Thread Synchronization:Too Much Milk1Implementing Critical Sections in Software HardThe following example will demonstrate the difficulty of providing mutual exclusion with memory reads and writeswrites¾ Hardware support is neededThe code must work all of the time¾ Most concurrency bugs generate correct results for someinterleavingsDesigning mutual exclusion in software shows you how to think about concurrent updates2how to think about concurrent updates¾ Always look for what you are checking and what you are updating¾ A meddlesome thread can execute between the check and the update, the dreaded race conditionThread CoordinationJackJillToo much milk!JackLook in the fridge; out of milkGo to storeBuy milkArrive home; put milk awayJillLook in fridge; out of milkGo to storeBuy milkArrive home; put milk away3Arrive home; put milk awayOh, no!Fridge and milk are shared data structuresFridge and milk are shared data structuresFormalizing “Too Much Milk”Shared variables¾ “Look in the fridge for milk” – check a variable¾ “Put milk away” – update a variableSafety property¾ At most one person buys milkLiveness¾ Someone buys milk when neededHow can we solve this problem?4How to think about synchronization codeEvery thread has the same pattern¾ Entry section: code to attempt entry to critical section¾ Critical section: code that requires isolation (e.g., with mutual exclusion)exclusion)¾ Exit section: cleanup code after execution of critical region¾ Non-critical section: everything elseThere can be multiple critical regions in a program¾ Only critical regions that access the same resource (e.g., data structure) need to synchronize with each otherwhile(1) {5Entry sectionCritical sectionExit sectionNon-critical section}The correctness conditionsSafety¾ Only one thread in the critical regionLiveness¾ Some thread that enters the entry section eventually enters the critical region ¾ Even if some thread takes forever in non-critical regionBounded waiting¾ A thread that enters the entry section enters the critical section within some bounded number of operations.Failure atomicity¾It is OK for a thread to die in the critical region6¾It is OK for a thread to die in the critical region¾ Many techniques do not provide failure atomicitywhile(1) {Entry sectionCritical sectionExit sectionNon-critical section}Too Much Milk: Solution #0while(1) {if (noMilk) { // check milk (Entry section)if (noNote) { // check if roommate is getting milkleave Note; //Critical sectionbuy milk;while(1) {if (noMilk) { // check milk (Entry section)if (noNote) { // check if roommate is getting milkleave Note; //Critical sectionbuy milk;Is this solution¾ 1. Correct¾ 2. Not safebuy milk;remove Note; // Exit section}// Non-critical region}buy milk;remove Note; // Exit section}// Non-critical region}7¾ 3. Not live¾ 4. No bounded wait¾ 5. Not safe and not liveIt works sometime and doesn’t some other timesWhat if we switch the order of checks?Too Much Milk: Solution #1while(1) {while(turn ≠ Jack) ; //spinwhile (Milk) ; //spinb milk; // C iti l s ti nwhile(1) {while(turn ≠ Jack) ; //spinwhile (Milk) ; //spinb milk; // C iti l s ti nwhile(1) {while(turn ≠ Jill) ; //spinwhile (Milk) ; //spinb milk;while(1) {while(turn ≠ Jill) ; //spinwhile (Milk) ; //spinb milk;turn := Jill // Initializationturn := Jill // Initializationbuy milk; // Critical sectionturn := Jill // Exit section// Non-critical section}buy milk; // Critical sectionturn := Jill // Exit section// Non-critical section}buy milk;turn := Jack// Non-critical section}buy milk;turn := Jack// Non-critical section}Is this solution¾ 1. Correct¾ 2. Not safe8¾ 3. Not live¾ 4. No bounded wait¾ 5. Not safe and not liveAt least it is safeSolution #2 (a.k.a. Peterson’s algorithm): combine ideas of 0 and 1Variables:¾ ini: thread Tiis executing , or attempting to execute, in CS¾ turn: id of thread allowed to enter CS if multiple want toClaim: We can achieve mutual exclusion if the following invariant holds before entering the critical section:9{(¬inj ∨ (inj ∧turn= i)) ∧ini}CS………ini= false((¬in0 ∨ (in0∧turn= 1)) ∧in1) ∧((¬in1 ∨ (in1∧turn= 0)) ∧in0) ⇒((turn= 0) ∧ (turn= 1)) = falsePeterson’s AlgorithmJackwhile (1) {in0:= true; turn := Jack;Jackwhile (1) {in0:= true; turn := Jack;Jillwhile (1) {in1:= true; t JillJillwhile (1) {in1:= true; t Jillin0= in1= false;in0= in1= false;turn := Jack;while (turn == Jack&& in1) ;//waitCritical sectionin0:= false;Non-critical section}turn := Jack;while (turn == Jack&& in1) ;//waitCritical sectionin0:= false;Non-critical section}turn := Jill;while (turn == Jill&& in0);//waitCritical sectionin1:= false;Non-critical section}turn := Jill;while (turn == Jill&& in0);//waitCritical sectionin1:= false;Non-critical section}10Safe, live, and bounded waitingBut, only 2 participantsToo Much Milk: LessonsPeterson’s works, but it is really unsatisfactory¾ Limited to two threads¾Solution is complicated; proving correctness is tricky even¾Solution is complicated; proving correctness is tricky even for the simple example¾ While thread is waiting, it is consuming CPU timeHow can we do better?¾ Use hardware to make synchronization faster¾ Define higher-level programming abstractions to simplify concurrent programming11concurrent programming Towards a solutionThe problem boils down to establishing the following right after entryi(¬inj ∨ (inj ∧ turn = i)) ∧ ini= (¬inj ∨ turn = i) ∧ iniHow can we do that?12entryi = ini := true;while (inj ∧turn≠ i);We hit a snagThread T0while (!terminate) {in0:= trueThread T1hil (!t i t ) {{in0}while (in1 ∧turn≠ 0);{in0 ∧ (¬ in1 ∨turn= 0)}CS0………}while (!terminate) {in1:= true{in1}while (in0 ∧turn≠ 1);{in1 ∧ (¬ in0 ∨turn= 1)}CS1………13}The assignment to in0invalidates the invariant!What can we do?Add assignment to turn to establish the second disjunctThread T0while (!terminate) {in0:= true; turn := 1;{in0}while (in1 ∧turn≠ 0);{in0 ∧ (¬ in1 ∨turn= 0 ∨ at(α1))}CS0in: fls;Thread T0while (!terminate) {in0:= true; turn := 1;{in0}while (in1 ∧turn≠ 0);{in0 ∧ (¬ in1 ∨turn= 0 ∨ at(α1))}CS0in: fls;Thread T1while (!terminate) {in1:= true;turn := 0;{in1}while (in0 ∧turn≠ 1);{in1 ∧ (¬ in0 ∨turn= 1 ∨ at(α0))}CS1in: fls;Thread T1while (!terminate) {in1:= true;turn := 0;{in1}while (in0 ∧turn≠ 1);{in1 ∧ (¬ in0 ∨turn= 1 ∨ at(α0))}CS1in: