nikita1212 / lamport-logical-clock-it-s-varification Goto Github PK

The Lamport Logical Clock problem Given a distributed system with N processes, each process goes through a finite number of events. The events could be internal or send or receive. We assume that broadcast is a send event with more than two receive events. In a correct execution of the (entire) distributed system: - each send event is followed by one or more receive events (no messages are lost) - a process has only one receive event associated with a send event executed at another process (there is no duplication of messages received) - there is no receive event without a send event that has happen at a different process earlier in the execution. We know that there is no global (shared) clock in a distributed system. Since a common physical clock is difficult to maintain and we are not interested in exact global real time but only in the ordering of these occurrences in time, we use the notion of logical clocks to have a partial order between events. As we learnt in the class, a logical clock C maps occurrences of events in a computation to partially ordered set such that 𝑎≺𝑏 ⇒ 𝐶(𝑎) < 𝐶(𝑏). Two examples of logical clocks are Lamport’s logical clock and the vector clock. In class we discussed and gave examples of how to calculate the Lamport logical clock values for events. Each process encounters a number of events and each event will have a Lamport Logical Clock value, simply LC-value, associated with it. In the next paragraph we will describe how to calculate these values. After that we will discuss if,, given values, how to detect whether a process has a correct or incorrect execution. Both aspects are important for the two algorithms that you have to design and implement. Let P be some process in the N-node distributed network. We need to calculate the LC-value for all the events that P encounters. We will reword the definition of the Lamport logical clock to make it more recursive. Let a be some event encountered by P. 1. If a is the first event and is an internal or send event, then LC(a) = 1. 2. If a is the first event and is a receive event, then LC(a) = k + 1 where k is the LC-value of the send event corresponding to a (that has occurred at a process other than P). 3. If a is not the first event and is an internal or send event, then LC(a) = k + 1 where k is the LC-value of the event just before a at process P. 4. If a is not the first event and is a receive event, let b be the send event corresponding to a (that has occurred at a process other than P) and k be the clock value of the event just before a at process P. Then LC(a) = max{ k, LC(b) } + 1

License: Eclipse Public License 1.0