Wednesday, October 16, 2013

In addition to the previous post, we can consider some optimizations as well. When a request enters the queue, it was acknowledged immediately. However, one optimization is that not all acknowledgements are needed. For example, if a request has already been sent with a later timestamp, then that request acts as an acknowledgement. The timestamp in the packet is used to guarantee a known time for this process that is greater than the request time.
Another optimization from Ricart-Agrawala involves eliminating acknowledgements for even more requests. If a request has already been sent with a time stamp with an earlier timestamp than a received request and that request is still pending, there is no need to send an acknowledgement. When that request is granted, we will send a release message and that will serve as an acknowledgement. When the process Pt receives a request,timestamp from a process Pj, it defers an acknowledgement if Pt is in critical section or if the request from Pj with a later timestamp than the one we sent, is still pending. When the process Pt leaves the critical section, it will send out an acknowledgement.
This completes the non-token based approach for mutual exclusion that we wanted to discuss.
Reverting to the program proof of correctness topic, here is one more:
Take the program to find the greatest common divisor of two given integers. The program is described with the following:
Let X and Y be two integers that are given, we select two numbers x and y such that x = y = gcd(X,Y)
Initially the program sets x to be greater than zero and equal to X, y to be greater than zero and equal to Y.
at each step the program assigns x to x-y if x > y or y to y - x if y > x. By doing this repeatedly, the program converges to the gcd.
The fixed point of the program can be interepreted to be y = 0 when x > y and x = 0 when y > x from the above.
The invariant adds the condition the gcd of (x,y) should be the same as the gcd for (X,Y) in addition to requiring that both x and y are positive integers.
We could use the metric as x+y since this value continually decreases and remains bounded below because on each step a positive number is subtracted from either x or y. We know the program can guarantee the metric will change because if x and y are different, at the next computation, their sum will be decreased. Thus the program terminates.


No comments:

Post a Comment