wip

Author: pavel-kirienko

specification/Cyphal_Specification.tex

@@ -81,12 +81,14 @@ \section*{Limitation of liability}
 \end{titlepage}
 
 \tableofcontents
-\listoftables
-\listoffigures
+\clearpage\listoftables
+\BeginRightColumn\listoffigures
 
 \mainmatter
 
 \input{introduction/introduction.tex}
+\input{session/session.tex}
 \input{transport/transport.tex}
+\input{appendices/appendices.tex}
 
 \end{document}

specification/appendices/appendices.tex

@@ -0,0 +1,6 @@
+\appendix
+
+\input{appendices/eviction.tex}
+\input{appendices/core_tla.tex}
+\input{appendices/proof.tex}
+\input{appendices/rapidhash.tex}

specification/appendices/core_tla.tex

@@ -0,0 +1,256 @@
+\chapter{\texorpdfstring{TLA\textsuperscript{+}}{TLA+} model of the allocation CRDT}\label{sec:appendix_core_tla}
+
+This appendix reproduces the complete contents of
+\texttt{model/tlaplus/Core.tla} from the Cy reference implementation.
+Core.tla is the primary source of truth for the semantics of the topic
+allocation CRDT described in section~\ref{sec:session_crdt}; where this
+specification and Core.tla disagree, Core.tla is authoritative.
+The \verb|Check_| statements have been removed from this transcript.
+
+\begin{minted}[fontsize=\scriptsize]{text}
+------------------------------ MODULE Core ------------------------------
+\* Key operators defined on Cyphal named topics. This is the core part of the formal protocol specification.
+\* This is pure TLA+ without PlusCal.
+\*
+\* The decentralized topic subject-ID allocation protocol in Cyphal solves the problem of allocating unique subject-IDs
+\* per topic name. The objective is to find a bijective configuration that is conflict-free
+\* (one topic name per subject-ID) and non-divergent (one subject-ID per topic name).
+\*
+\* There is no central coordinator. Nodes eventually find the consensus by periodically broadcasting gossip messages.
+\* Each gossip message carries a single topic->subject allocation entry (nodes apply simple rules to choose which entry
+\* to gossip next). Every node only keeps the entries that it needs (publishers/subscribers that the application needs
+\* to use); no node is required to keep the full set of entries. Every node must be *eventually* able to receive and
+\* send gossip messages for the protocol to make progress; transient inability to do so will not break the protocol
+\* but may delay the consensus (resource-limited nodes may choose to drop some gossip messages to reduce processing
+\* burden; this does not violate the core assumptions of the protocol as long as such nodes are able to *eventually*
+\* receive each live allocation entry).
+\*
+\* The allocation protocol does not operate on topic names directly, substituting them with numerical hashes instead.
+\* The application layer is expected to attach names to hashes but this is of no relevance to the core protocol.
+\* From the standpoint of the core allocation protocol, "topic name" and "topic hash" can be used interchangeably.
+\*
+\* Each allocation entry contains three fields: the topic hash, the topic eviction count, and the topic age.
+\* A pair of entries can be compared to each other to determine if the pair constitutes a collision
+\* (different names, same subject) or a divergence (same name, different subjects);
+\* other comparison outcomes are of no interest.
+\*
+\* The eviction count is used as a Lamport clock and hence implementations ensure that it cannot overflow. Since
+\* evictions are static on a quiescent network, even relatively narrow representations (e.g., 32 bit) may suffice.
+\*
+\* The subject-ID assigned to a topic is defined as some function of its hash and eviction count. One possible way
+\* to define the function is, assuming 64-bit unsigned arithmetics:
+\*
+\*      subject_id = 8192 + ((hash + evictions**2) % 8380403)
+\*
+\* For the background on the subject of open addressing schemes and why the specific values were chosen this way, see:
+\* - https://en.wikipedia.org/wiki/Quadratic_probing
+\* - https://github.com/OpenCyphal-Garage/cy/issues/12
+\*
+\* The eviction count of a topic is incremented whenever the topic is involved in a collision and loses arbitration.
+\* Arbitration is defined as two functions, defined here as LeftWinsCollision and LeftWinsDivergence.
+\* The topic age is incremented monotonically as some kind of real or logical clock, such that each node that holds
+\* this topic is expected to increment its age at approximately the same rate (the protocol does not require the
+\* increment rate to match accurately, but better rate matching results in faster worst-case convergence).
+\* The age is used to determine which topic wins arbitration in the event of a collision or a divergence,
+\* with the core idea being that older topics win arbitration to avoid disturbances to established networks.
+\*
+\* The topic-subject allocation table described above is a kind of CRDT (conflict-free replicated data type).
+\* A CRDT only guarantees eventual convergence while the system is quiescent, which seemingly contradicts the
+\* use of the age counter that increments continuously. To work around this, the protocol uses the binary
+\* logarithm of topic ages for topic comparison instead of the actual age value, which naturally slows down
+\* the increment rate over time, approaching quiescence.
+\*
+\* When a node creates a new topic (i.e., when the local application creates a new subscription or publication),
+\* its age and eviction counter are set to zero; the initial subject-ID is obtained using the function above.
+\* The topic is commissioned to use immediately without the need to wait for the network to converge,
+\* despite the fact that it is known that the initial allocation may be conflicting or divergent.
+\* To avoid the risk of data misinterpretation should a collision occur, the transport layer carries the
+\* topic hash per transfer, and the transfer is rejected should the hash be incorrect.
+\* Each local topic is reconfigured as necessary should the allocation protocol require so, transparently for
+\* the application.
+\*
+\* Upon reception of a gossip, the age of the matching local topic, if there is one, is updated as:
+\* local_age = max(local_age, 2**remote_age_log2).
+\*
+\* Pavel Kirienko <pavel@opencyphal.org>, MIT license
+
+EXTENDS Utils
+LOCAL INSTANCE Integers
+LOCAL INSTANCE TLC
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE FiniteSets
+
+\* Computes floor(log2(x)), with the special case floor(log2(0)) == -1
+RECURSIVE Log2Floor(_)
+Log2Floor(x) == IF x > 1 THEN 1 + Log2Floor(x \div 2) ELSE x - 1
+
+\* Special case: Pow2(-1) = 0
+Pow2(x) == IF x > 1 THEN 2^x ELSE x + 1
+
+FloorToPow2(x) == Pow2(Log2Floor(x))
+
+\***********************************************************************************************************************
+\* Subject-ID mapping function. The ring size is the total number of distinct subject-IDs.
+\* TODO: Switch to quadratic probing: https://github.com/OpenCyphal-Garage/cy/issues/12
+SubjectIDRing == 10
+SubjectID(hash, evictions) == (hash + evictions) % SubjectIDRing
+
+\***********************************************************************************************************************
+\* COLLISION is when topics with different hashes land on the same subject-ID (see the subject_id mapping).
+LeftWinsCollision(a, b) == IF   Log2Floor(a.age) # Log2Floor(b.age)
+                           THEN Log2Floor(a.age) > Log2Floor(b.age)
+                           ELSE a.hash < b.hash
+
+\* DIVERGENCE is when topics with the same hash are found to have different eviction counters:
+\* the eviction counters have to match, so we need to decide which one is the correct one.
+LeftWinsDivergence(a, b) == \/  Log2Floor(a.age) > Log2Floor(b.age)
+                            \/ (Log2Floor(a.age) = Log2Floor(b.age) /\ a.evictions > b.evictions)
+
+\***********************************************************************************************************************
+\* The result is Nothing if no such topic exists.
+\* Topics are stored in sets because all operations on them are ordering-invariant,
+\* which is a basic prerequisite for CRDT operations.
+GetByHash(hash, topics)            == Get(topics, LAMBDA x: x.hash = hash)
+GetBySubjectID(subject_id, topics) == Get(topics, LAMBDA x: SubjectID(x.hash, x.evictions) = subject_id)
+
+\***********************************************************************************************************************
+\* A set of topics without the specified one. Same set if the specified topic is not a member.
+RemoveTopic(hash, topics) == { t \in topics : t.hash # hash }
+
+\* Add or replace a topic into a set of topics.
+\* Use this to mutate a topic state in a set.
+ReplaceTopic(new, topics) == {new} \cup RemoveTopic(new.hash, topics)
+
+\* A set of topics extended with the specified one, and the existing topics possibly altered.
+\* Uniqueness is guaranteed; if the topic is in the set already, it will be modified.
+\* This can also be used to model state update of the local topic table.
+RECURSIVE AllocateTopic(_, _)
+AllocateTopic(t, topics) ==
+    LET ts == RemoveTopic(t.hash, topics)
+        x == GetBySubjectID(SubjectID(t.hash, t.evictions), ts)
+        Evicted(z) == [hash |-> z.hash, evictions |-> 1 + z.evictions, age |-> z.age]
+    IN   IF x = Nothing             THEN {t} \cup ts
+    ELSE IF LeftWinsCollision(t, x) THEN AllocateTopic(Evicted(x), {t} \cup ts)
+    ELSE                                 AllocateTopic(Evicted(t), ts)          \* Retry with evictions+1
+
+\***********************************************************************************************************************
+\* Constructs a conflict-free topic set. This is meant for constructing the initial node state.
+\* Each hash can occur at most once.
+RECURSIVE AllocateTopics(_, _)
+AllocateTopics(new, topics) ==
+    IF Cardinality(new) = 0 THEN topics
+    ELSE LET t == CHOOSE x \in new : TRUE
+         IN AllocateTopics(new \ {t}, AllocateTopic(t, topics))
+
+\***********************************************************************************************************************
+\* Implementation of the divergence resolution rule with CRDT age merge.
+LOCAL AcceptGossip_Divergence(remote, topics) ==
+    LET hash == remote.hash
+        local == GetByHash(hash, topics)
+        \* The serialization protocol floors the remote age to pow2 before transmission.
+        new_age == Max({IF local # Nothing THEN local.age ELSE 0, FloorToPow2(remote.age)})
+    IN
+    IF local # Nothing THEN
+        IF local.evictions # remote.evictions /\ LeftWinsDivergence(remote, local)
+        THEN AllocateTopic([hash|->hash, evictions|->remote.evictions, age|->new_age], topics)
+        ELSE              {[hash|->hash, evictions|-> local.evictions, age|->new_age]} \cup RemoveTopic(hash, topics)
+    ELSE topics
+
+\* Implementation of the collision resolution rule.
+LOCAL AcceptGossip_Collision(remote, topics) ==
+    LET local == GetBySubjectID(SubjectID(remote.hash, remote.evictions), topics)
+    IN IF local # Nothing /\ LeftWinsCollision(remote, local)
+    THEN AllocateTopic([hash |-> local.hash, evictions |-> local.evictions + 1, age |-> local.age], topics)
+    ELSE topics
+
+\* An updated sequence of topics based on a received gossip message.
+\* The sequence may be modified if the gossiped entry is observed to diverge or collide with a local entry,
+\* and the affected local entry loses arbitration to the gossiped one.
+\* The naive implementation is as simple as:
+\*
+\*      AcceptGossip_Collision(remote, AcceptGossip_Divergence(remote, topics))
+\*
+\* which is correct and converges eventually; however, it is not optimal because it may cause a local entry
+\* to lose a collision arbitration to a divergent remote entry, which will cause unnecessary eviction counter
+\* increments and thus delay convergence. To avoid this, we ignore collisions if the remote entry is seen to be
+\* divergent from a local entry and the local entry wins the divergence arbitration.
+AcceptGossip(remote, topics) ==
+    IF GetByHash(remote.hash, topics) # Nothing     \* If the topic exists locally
+    THEN AcceptGossip_Divergence(remote, topics)    \* Divergence resolver will ensure collision-freedom as well
+    ELSE AcceptGossip_Collision(remote, topics)     \* We don't know this topic, just ensure collision-freedom
+
+\***********************************************************************************************************************
+\* Divergent allocation detector operating on a function node_id -> {topic_0, topic_1, ..., topic_n}
+\* A divergent allocation occurs when topic records with the same hash have distinct eviction counters.
+\* If no divergences are found, the result is an empty set.
+FindDivergent(node_topics) ==
+    LET hashes == { t.hash : t \in UNION Range(node_topics) }
+        flat == { [hash |-> t.hash, evictions |-> t.evictions] : t \in UNION Range(node_topics) }
+    IN { h \in hashes : Cardinality({ s \in flat : s.hash = h }) > 1 }
+
+\***********************************************************************************************************************
+\* Allocation collision detector operating on a function node_id -> {topic_0, topic_1, ..., topic_n}
+\* A collision occurs when topic records with distinct hashes have identical subject-ID.
+\* If no collisions are found, the result is an empty set.
+FindCollisions(node_topics) ==
+    LET flat == { [hash |-> t.hash, subject_id |-> SubjectID(t.hash, t.evictions)] : t \in UNION Range(node_topics) }
+        subject_ids == { t.subject_id : t \in flat }
+    IN { s \in subject_ids : Cardinality({ t \in flat : t.subject_id = s }) > 1 }
+
+\***********************************************************************************************************************
+\* Whether the network has converged to a stable state.
+\* Once a stable state is reached, the topics that are involved in it will no longer be altered as long as
+\* no older topics are introduced to the network (such as in the event of network departitioning).
+\* Appearance of young topics will not affect the existing entries by design.
+Converged(node_topics) ==
+    /\ FindDivergent(node_topics) = {}
+    /\ FindCollisions(node_topics) = {}
+
+========================================================================================================================
+\end{minted}
+
+\begin{minted}[fontsize=\scriptsize]{text}
+------------------------------ MODULE Utils ------------------------------
+\* General-purpose utilities not specific to this problem.
+\* There are a few utilities here copied over from https://github.com/tlaplus/CommunityModules (MIT license)
+
+LOCAL INSTANCE Integers
+LOCAL INSTANCE Naturals
+LOCAL INSTANCE TLC
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE FiniteSets
+
+CONSTANT Nothing
+
+\* From https://github.com/tlaplus/CommunityModules (MIT license)
+PrintVal(id, exp) == Print(<<id, exp>>, TRUE)
+IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
+SeqToSet(s) == {s[i] : i \in DOMAIN s}
+SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
+SetToSeqs(S) == LET D == 1..Cardinality(S) IN { f \in [D -> S] : \A i,j \in D : i # j => f[i] # f[j] }
+Range(f) == { f[x] : x \in DOMAIN f }
+
+Min(S) == CHOOSE s \in S : \A t \in S : s <= t
+Max(S) == CHOOSE s \in S : \A t \in S : s >= t
+
+\* The first element in a sequence where test(e) is TRUE; Nothing if the test is FALSE for all elements.
+FirstMatch(haystack, test(_)) ==
+    LET i == CHOOSE i \in 1..(Len(haystack)+1): (i > Len(haystack)) \/ test(haystack[i])
+    IN IF i > Len(haystack) THEN Nothing ELSE haystack[i]
+
+\* The set element where test(e) is TRUE; Nothing if the test is false for all elements.
+Get(haystack, test(_)) == LET matches == { x \in haystack : test(x) }
+                          IN IF matches = {} THEN Nothing ELSE CHOOSE x \in matches : TRUE
+
+\* A sequence that contains zero needles.
+SeqWithout(haystack, needle) == SelectSeq(haystack, LAMBDA x: x # needle)
+
+\* <<1, 2, 3>> ==> <<2, 3, 1>>
+SeqRotLeft(seq) == IF Len(seq) > 0 THEN Tail(seq) \o <<Head(seq)>> ELSE seq
+
+\* Converts {<<k1, v1>>, <<k2, v2>>, ...} into a function [k |-> v]. Keys must be unique.
+FunFromTupleSet(S) == [
+    k \in {p[1] : p \in S} |-> CHOOSE v \in {r[2] : r \in S} : <<k, v>> \in S
+]
+========================================================================================================================
+\end{minted}

specification/appendices/eviction.tex

@@ -0,0 +1,88 @@
+\chapter{Eviction counter recovery}\label{sec:appendix_eviction_solver}
+
+Given a topic hash, a subject-ID, and the subject-ID modulus, the eviction
+counter of a non-pinned topic can be reconstructed in constant time.
+This works because the subject-ID mapping
+(section~\ref{sec:session_subject_id_mapping})
+uses quadratic probing modulo a prime $M$ with $M \bmod 4 = 3$, which makes
+the probing sequence invertible via the closed-form square root
+$r = d^{(M+1)/4} \bmod M$ for quadratic residues $d$.
+
+The recovery is useful for diagnostic tools -- for example, to cross-check a
+running network against the mapping formula, or to display a topic's
+eviction history in a monitoring dashboard -- but it is not required for
+protocol participation. Any implementation that participates in the
+consensus protocol already has the eviction counter on hand.
+
+\begin{remark}
+    The solver below has been exhaustively brute-force verified for the
+    moduli $57203$, $131071$, and $8388607$.
+    Implementations that use it for diagnostics should treat a
+    \texttt{UINT32\_MAX} return value as \emph{the subject-ID was not
+    produced from the given hash by the mapping function}, which is a valid
+    outcome when the diagnostic tool is probing an unrelated subject.
+    The solver assumes that the eviction counter does not exceed
+    $\lfloor M / 2 \rfloor$; above that bound the probing sequence starts
+    to repeat and the recovery is no longer unique.
+\end{remark}
+
+\begin{minted}[fontsize=\scriptsize]{cpp}
+// Pavel Kirienko <pavel@opencyphal.org>, MIT license
+
+// a**e mod m
+static uint32_t pow_mod_u32(uint32_t a, uint32_t e, const uint32_t m)
+{
+    uint32_t r = 1 % m;
+    a %= m;
+    while (e) {
+        if (e & 1U) {
+            r = (uint32_t)(((uint64_t)r * (uint64_t)a) % m);
+        }
+        a = (uint32_t)(((uint64_t)a * (uint64_t)a) % m);
+        e >>= 1U;
+    }
+    return r;
+}
+
+// Legendre symbol: a^((p-1)/2) mod p is 1 for residues, p-1 for non-residues, 0 for a==0.
+static bool is_quadratic_residue_prime(const uint32_t a, const uint32_t p)
+{
+    return (a == 0) || (pow_mod_u32(a, (p - 1U) / 2U, p) == 1U);
+}
+
+// Derives evictions from a non-pinned subject-ID. For pinned subject-IDs returns 0.
+// Assumes subject_id_modulus is a prime with (subject_id_modulus % 4) == 3.
+// Returns UINT32_MAX if the subject-ID was obtained using distinct parameters.
+// If evictions > floor(modulus/2), the subject-ID sequence repeats, leading to non-unique solutions;
+// the solver assumes that evictions stay below that bound. Complexity is O(1).
+static uint32_t topic_evictions_from_subject_id(const uint64_t hash,
+                                                const uint32_t subject_id,
+                                                const uint32_t subject_id_modulus)
+{
+    const uint32_t p = subject_id_modulus;
+    assert((p > 3) && ((p & 3U) == 3U));
+    if (subject_id <= 8191U) {
+        return 0; // Pinned subject; eviction count is not meaningful here.
+    }
+    const uint32_t base = subject_id - 8192U;
+    if (base >= p) {
+        return UINT32_MAX;
+    }
+    const uint32_t delta = (uint32_t)(((uint64_t)base + (uint64_t)p - (hash % p)) % p);
+    if (!is_quadratic_residue_prime(delta, p)) {
+        return UINT32_MAX;
+    }
+    // sqrt(delta) mod p  (since p % 4 == 3):  r = delta^((p+1)/4) mod p
+    const uint32_t r1 = (delta == 0U) ? 0U : pow_mod_u32(delta, (p + 1U) / 4U, p);
+    const uint32_t r2 = (r1 == 0U) ? 0U : (p - r1);
+    uint32_t       best     = UINT32_MAX;
+    const uint32_t roots[2] = { r1, r2 };
+    for (unsigned i = 0; i < 2; i++) {
+        const uint64_t s = roots[i];
+        if ((s <= (p / 2U)) && (s < best)) {
+            best = (uint32_t)s;
+        }
+    }
+    return best;
+}
+\end{minted}