Turing Lecture: The Computer Science of Concurrency – The Early Years(cacm.acm.org)
cacm.acm.org
Turing Lecture: The Computer Science of Concurrency – The Early Years
http://cacm.acm.org/magazines/2015/6/187316-turing-lecture-the-computer-science-of-concurrency
4 comments
>The proof of correctness of the algorithm revealed that the read or write of an entire number need not be atomic. The bakery algorithm is correct as long as reading a number returns the correct value if the number is not concurrently being written. It doesn't matter what value is returned by a read that overlaps a write. The algorithm is correct even if reading a number while it is changing from 9 to 10 obtains the value 2496.
How?
How?
> It doesn't matter what value is returned by a read that overlaps a write. The algorithm is correct even if reading a number while it is changing from 9 to 10 obtains the value 2496.
There are two variables involved in the bakery algorithm[1] -- choosing[k] and number[k]:
- choosing[k] takes only the two values 0 & 1, hence reading/writing to it is atomic.
- number[k] is boundless, hence the question of inconsistency while reading it. Lamport shows (see Assertion 2's Proof in [1]) that given,
I think it is much easier to understand with the two-arrow formalism presented later in the article.
[1]: http://msr-waypoint.com/en-us/um/people/lamport/pubs/bakery....
There are two variables involved in the bakery algorithm[1] -- choosing[k] and number[k]:
- choosing[k] takes only the two values 0 & 1, hence reading/writing to it is atomic.
- number[k] is boundless, hence the question of inconsistency while reading it. Lamport shows (see Assertion 2's Proof in [1]) that given,
1. tL2 < tL3 (on process i), and
2. te < tw < tc (on process k),
I think it is much easier to understand with the two-arrow formalism presented later in the article.
[1]: http://msr-waypoint.com/en-us/um/people/lamport/pubs/bakery....
[deleted]
It comes down to how you define correctness. Weaker consistency requirements accept executions that do not serialize processor orderings allowing for algorithms like bakery to work without strong atomic operations.
[deleted]
One of the best things I read today :)
Thanks for posting.
[1] http://research.microsoft.com/en-us/um/people/lamport/pubs/l...