[
https://issues.apache.org/jira/browse/IGNITE-16893?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Alexander Lapin updated IGNITE-16893:
-------------------------------------
Description:
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.
Tx.Phase1
was:
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.
> 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.
>
> Tx.Phase1
--
This message was sent by Atlassian Jira
(v8.20.7#820007)
