Implementing counting semaphores using binary semaphoresA. Udaya Shankarhttp://www.cs.umd.edu/users/shankar/412-Notes/10x-CountingFromBinarySemaphores.htmlAugust 11, 20111 IntroductionTwo implementations of counting semaphores using binary semaphores are given below. Implementation 1 isincorrect. Thanks to Timothy Alicie for pointing this out. Implementation 2 (by Barz) is proved to be correct.Assignment is←. Equality is "=". CSem stands for counting semaphores. BSem stands for binary semaphores.References• Hans W. Barz. 1983. Implementing semaphores by binary semaphores. SIGPLAN Not. 18, 2 (February1983), 39-45.DOI=10.1145/948101.948103 http://doi.acm.org/10.1145/948101.948103).• David Hemmendinger. 1989. Comments on “A correct and unrestrictive implementation of generalsemaphores”. SIGOPS Oper. Syst. Rev. 23, 1 (January 1989), 7-8.DOI=10.1145/65762.65763 http://doi.acm.org/10.1145/65762.65763.2 Implementation 1 (incorrect)CSem(K) cs { // counting sem, init Kint val ← K; // value of csemBSem wait(0); // to block on csemBSem mutex(1); // protects valPc(cs) {P(mutex);val ← val−1;if val < 0 {V(mutex);1: P(wait);} elseV(mutex);}Vc(cs) {P(mutex);val ← val + 1;if val ≤ 0V(wait);V(mutex);}}Evolution showing errorInitial:cs = 0; val = 0; wait = 0; mutex = 1.Thread t1 attempts Pc(cs):t1 at 1; val =−1; wait = 0; mutex = 1.Thread t2 attempts Pc(cs):t1, t2 at 1; val =−2; wait = 0; mutex = 1.Thread t3 executes Vc(cs) twice:t1, t2 at 1; val = 0; wait = 1; mutex = 1.Thread t2 gets past 1:t1 at 1; val = 0; wait = 0; mutex = 1.Thread t1 is blocked, but it should not be.13 Implementation 2 (correct)CSem(K) cs { // counting semaphore initialized to Kint val ← K; // the value of csemBSem gate(min(1,val)); // 1 if val > 0; 0 if val = 0BSem mutex(1); // protects valPc(cs) {P(gate)a1: P(mutex);val ← val−1;if val > 0V(gate);V(mutex);}Vc(cs) {P(mutex);val ← val + 1;if val = 1V(gate);V(mutex);}}3.1 Criteria for correct implementationNote that val is decremented at the end of Pc(cs) and incremented at the end of Vc(cs). Thus val alwaysequals the correct value of counting semaphore cs. Thus the program implements the counting semaphore if(and only if) the following hold:A1: val ≥ 0 always holds.A2: If a thread t is at Pc(cs) and val > 0 holds,then eventually either thread t gets past Pc(cs) or val = 0 holds.A1ensures that a thread gets past Pc(cs) only if val is higher than zero just before getting past (otherwise, A1would not hold just after the thread got past).A2ensures that if threads are waiting on Pc(cs) and val is positive, one thread will get past. (This is so-called"weak fairness". One can also prove "strong fairness" assuming the same of the binary semaphores.)3.2 Effective atomicityWhen analyzing the above program each of functions Pc(cs) and Vc(cs) can be treated as atomically executed.Proof: While a thread is inside Vc(cs), it is not affected by its environment nor does it affect the environment.The former is obvious. The latter is almost obvious.While a thread t is executing a code chunk, the environment learns nothing about the state of its execution.Another thread blocked on gate may get past P(gate) before thread t exits the code chunk (i.e., before itexecutes V(mutex)). But the environment cannot distinguish this from the situation where thread t executesV(mutex) first (but the news was slow to get to the environment).The argument for Pc(cs) is the same. (Blocking occurs only at the start, before thread t gets inside Pc(cs).)End of proof23.3 Proof of A1and A2Exactly one of the following always holds:B1: (no thread at a1) and (val ≥ 0) and (gate = 1 iff val > 0)B2: (exactly one thread at a1) and (val > 0) and (gate = 0)Proof: It is easy to check that each of functions Pc(cs) and Vc(cs) preserves (B1or B2): i.e., establishes(B1or B2) if (B1or B2) held before the step.(B1or B2) implies A1. (B1implies val ≥ 0, and B1implies val > 0.)B1implies A2. (If val is non-zero then gate equals 1, and so any thread at Pc(cs) is not blocked.End of
View Full Document
Unlocking...