Notes from reading the paper

[lemmy]

S1

• “In distributed systems...”: Consider mentioning 2f+1?
• “...supports switching between witness and non-witness servers.”: Not sure what this means

S2

• “regular servers”: Perhaps ordinary raft servers?
• All properties are absent in the TLA+ spec
• “minimal set of metadata”: Why “set of” metadata? And what is the metadata (indices, ...)?
• “frequency of witness visits”: Perhaps witness communication? More concrete: RPCs?
• “In the rest of this document...”: Consider using consistent and unambiguous terminology. Why not just speak of servers and witness?

S2.1

• Def 1, { s \in SUBSET (S \cup {witness}) : Cardinality(s) = Cardinality(Server) }
• Def 2, “..., each begins with a replication set.”: What does it mean for subterms to begin with a repl set?
• Prop == [][term # term' => subterm' = 0]_vars * I won't bother with term and subterm being functions here.
• “...consecutive integers”: consecutive natural numbers
• Prop == [][UNCHANGED subterm => UNCHANGED replSet]_vars

S2.2

• “...additional state...”: additional variables
• “...volatile variables”: Perhaps non-durable?
• “...that the leader sent to the witness.”: There can be more than one leader in Raft, which is also what the previous paragraph says. At this point I presume that the leader includes its term/subterm and the witness keeps the values from the leader with the highest term?
• <<index, term, subterm>>: Why not derive the index from the position of the tuple <<term, subterm>> in the log? Perhaps type, because figure 2.2 has <<term, subterm, value>>.
• “..., which is uniquely identified by index and term, and associated with subterm.”: Unclear why that is important at this stage

S2.3

• Broken Figure ??
• “...includes the current replication and ”: +set
• “...and metadata”: Define metadata: term, lastLogTerm, lastLogSubterm, lastIndex,
• Does it only ever send one entry at the time?
• “solely used for proof”: In TLA jargon that's called an auxiliary or history variable
• Broken ref: condition ??
• “...it also updates its witnessSubterm...”: This doesn't seem to exist in extendedraft.tla where witnessSubterm remains forever unchanged. Has Shortcut Replication not been modeled?
• “This is to ensure the leader... condition 1”
• extendedraft!AdjustReplicationSet: CHOOSE eliminates non-determinism here that should not be eliminated.
• extendedraft!AdjustReplicationSet: This does not create a new empty log entry (“...a new empty log entry must be appended...”)
  ∗ Figure 2.5 also doesn't create a new entry
• “The acknowledgement either comes from a regular server or the witness”: This sounds specific to a three node (2 servers+witness) cluster