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

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

     [ https://issues.apache.org/jira/browse/IGNITE-16893?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]

Alexander Lapin updated IGNITE-16893:
-------------------------------------
    Labels: ignite-3  (was: )

> 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
>            Priority: Major
>              Labels: ignite-3
>         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)