[jira] [Created] (IGNITE-16893) Implement HLC and clock syncrhonization logic

["Alexander Lapin (Jira)" <ji...@apache.org>]

Alexander Lapin created IGNITE-16893:
----------------------------------------

             Summary: Implement HLC and clock syncrhonization logic
                 Key: IGNITE-16893
                 URL: https://issues.apache.org/jira/browse/IGNITE-16893
             Project: Ignite
          Issue Type: Improvement
            Reporter: Alexander Lapin
         Attachments: Screenshot from 2022-04-22 16-14-27.png, Screenshot from 2022-04-22 16-16-10.png

HLC is similar to LC, but has a physical meaning and accurately represents physical time within a bound error.

The rules for updating HLC:
{code:java}
Initially l.j = 0; c.j = 0 

Send or local event 
l’.j = l.j; 
l.j = max(l’.j, pt.j); 
If (l.j = l’.j) then c.j = c.j + 1
Else c.j = 0;
Timestamp with l.j, c.j 
{code}
Receive event of message m 
{code:java}
l’.j = l.j; 
l.j = max(l’.j, l.m, pt.j); 
If (l.j = l’.j =l.m) then c.j = max(c.j, c.m)+1 
Elseif (l.j =l’.j) then c.j = c.j + 1 
Elseif (l.j =l.m) then c.j = c.m + 1 
Else c.j = 0 
Timestamp with l.j, c.j{code}
!Screenshot from 2022-04-22 16-14-27.png!The following statements hold true for HLC, represented by (l,c):
 # For any two events e and f, e <- f => (l.e; c.e) < (l.f; c.f) // Lexicographic comparison
 # For any event f, l.f >= pt.f
 # l.f > pt.f => (∃g : g <- f && pt.g = l.f)
 # For any event f, |l.f - pt.f| < ϶,
where ϶ represents clock sync uncertainty. For NTP e ~= 2 * ntp_offset
 # For any event f, c.f = k && k > 0 => (
∃g1; g2; … ; gk : (∀j: 1 <= j < k : gj <- gj+1) && (∀j : 1 <= j < k : l.(gj) = l.f) && (gk hb f)
)
 # For any event f, c.f <= |\{g : g <- f && l.g = l.f}|
 # For any event f, c.f <=  N * (϶ + 1), if a physical clock of a node is incremented by at least one between any two events on that node

HLC *may overflow* if physical time is not catching up with logical time. In this case only a causal counter can be used to move the timestamp forward. The *bounded time staleness requirement* is aimed to fix this.

HLC is not limited by NTP and can be used with other time sync protocols, like PTP.
h4. Consistent Cut

HLC can also be used to take a consistent snapshot at a logical time {_}t{_}.

The consistent cut should capture all causal relationships. It can be written down as follows:

*(e ∈ C) && (e’ <- e) => e’ ∈ C*

[https://www.cs.cornell.edu/courses/cs5414/2010fa/publications/BM93.pdf]

!Screenshot from 2022-04-22 16-16-10.png!

In the picture are shown two cuts: C - is the consistent cut, C’ - is the inconsistent cut.

HLC allows taking a consistent cut at logical time l=t, c=K

A global time, corresponding to the cut, lies in [t-϶,t]

h4. HLC Update Rules

We assume two major event sources for updating HLC for enlisted nodes:
h5. RAFT events

RAFT events help to synchronize HLC between RAFT replicas. All RAFT communications are initiated by a leader, and only one leader can exist at a time. This enforces monotonic growth of HLC on raft group replicas. RequestVote and AppendEntries RPC calls are enriched with sender’s HLC. The HLC update rules are applied on receiving messages. RAFT lease intervals are bound to the HLC range.
h5. Transaction protocol events

Another source of HLC sync is a transaction protocol. Each message involved in the execution of the transaction carries the sender’s HLC and updates receiver HLC according to rules.

 



--
This message was sent by Atlassian Jira
(v8.20.7#820007)