Thread Synchronization: Too Much MilkImplementing Critical Sections in Software HardThread CoordinationFormalizing “Too Much Milk”How to think about synchronization codeThe correctness conditionsToo Much Milk: Solution #0Too Much Milk: Solution #1Solution #2 (a.k.a. Peterson’s algorithm): combine ideas of 0 and 1Peterson’s AlgorithmToo Much Milk: LessonsTowards a solutionWe hit a snagWhat can we do?Safe?Live?Bounded waiting?1Thread Synchronization:Too Much Milk2Implementing Critical Sections in Software HardThe following example will demonstrate the difficulty of providing mutual exclusion with memory reads and writesHardware support is neededThe code must work all of the timeMost concurrency bugs generate correct results for some interleavingsDesigning mutual exclusion in software shows you how 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 condition3Thread CoordinationJackLook in the fridge; out of milkGo to storeBuy milkArrive home; put milk awayJillLook in fridge; out of milkGo to storeBuy milkArrive home; put milk awayOh, no!Too much milk!Fridge and milk are shared data structuresFridge and milk are shared data structures4Formalizing “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?5How 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)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) { Entry section Critical section Exit section Non-critical section}6The 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 regionMany techniques do not provide failure atomicitywhile(1) { Entry section Critical section Exit section Non-critical section}7Too Much Milk: Solution #0Is this solution1. Correct2. Not safe3. Not live4. No bounded wait5. Not safe and not liveIt works sometime and doesn’t some other timeswhile(1) { if (noMilk) { // check milk (Entry section) if (noNote) { // check if roommate is getting milk leave Note; //Critical section buy milk; remove Note; // Exit section } // Non-critical region}while(1) { if (noMilk) { // check milk (Entry section) if (noNote) { // check if roommate is getting milk leave Note; //Critical section buy milk; remove Note; // Exit section } // Non-critical region}What if we switch the order of checks?8Too Much Milk: Solution #1while(1) { while(turn ≠ Jack) ; //spin while (Milk) ; //spin buy milk; // Critical section turn := Jill // Exit section // Non-critical section}while(1) { while(turn ≠ Jack) ; //spin while (Milk) ; //spin buy milk; // Critical section turn := Jill // Exit section // Non-critical section}while(1) { while(turn ≠ Jill) ; //spin while (Milk) ; //spin buy milk; turn := Jack // Non-critical section}while(1) { while(turn ≠ Jill) ; //spin while (Milk) ; //spin buy milk; turn := Jack // Non-critical section}Is this solution1. Correct2. Not safe3. Not live4. No bounded wait5. Not safe and not liveAt least it is safeturn := Jill // Initializationturn := Jill // Initialization9Solution #2 (a.k.a. Peterson’s algorithm): combine ideas of 0 and 1Variables:ini: thread Ti is 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:{(¬inj  (inj  turn = i))  ini}CS……… ini = false((¬in0  (in0  turn = 1))  in1) ((¬in1  (in1  turn = 0))  in0) ((turn = 0)  (turn = 1)) false10Peterson’s AlgorithmSafe, live, and bounded waitingBut, only 2 participantsJackwhile (1) {in0:= true; turn := Jack;while (turn == Jack && in1) ;//waitCritical sectionin0 := false;Non-critical section}Jackwhile (1) {in0:= true; turn := Jack;while (turn == Jack && in1) ;//waitCritical sectionin0 := false;Non-critical section}Jillwhile (1) {in1:= true; turn := Jill;while (turn == Jill && in0);//waitCritical sectionin1 := false;Non-critical section}Jillwhile (1) {in1:= true; turn := Jill;while (turn == Jill && in0);//waitCritical sectionin1 := false;Non-critical section}in0 = in1 = false;in0 = in1 = false;11Too Much Milk: LessonsPeterson’s works, but it is really unsatisfactoryLimited to two threads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 programming12Towards 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?entryi = ini := true;while (inj turn ≠ i);13We hit a snagThread T0while (!terminate) {in0:= true{in0}while (in1 turn ≠ 0);{in0  (¬ in1  turn = 0)}CS0………}Thread T1while (!terminate) {in1:= true{in1}while (in0 turn ≠ 1); {in1  (¬ in0  turn = 1)} CS1………}The assignment to in0invalidates the invariant!14What can we do?Thread T0while (!terminate) {in0:= true; turn := 1;{in0}while (in1 turn ≠ 0);{in0  (¬ in1  turn = 0  at(1) )}CS0in0 := false;NCS0}Thread T0while (!terminate) {in0:= true; turn := 1;{in0}while (in1 turn ≠ 0);{in0  (¬ in1  turn = 0  at(1) )}CS0in0 := false;NCS0}Thread