Class RaftInvariantChecker

java.lang.Object
com.loomcache.server.consensus.RaftInvariantChecker
public class RaftInvariantChecker extends Object
Utility class for checking Raft safety invariants at runtime.

Provides static methods to validate Raft invariants: - Election Safety: at most one leader per term - Log Matching: if two logs have the same entry at an index, all preceding entries are identical - Leader Completeness: committed entries persist in leaders of higher-numbered terms - Commit Index Monotonicity: commitIndex never decreases - Term Monotonicity: currentTerm never decreases

All methods return an InvariantResult record with the validation status and violation message.

  • Method Details

    • checkElectionSafety

      public static RaftInvariantChecker.InvariantResult checkElectionSafety(List<RaftNode> nodes)
      Check Election Safety: at most one leader per term across a list of nodes.

      Verifies that for any given term, at most one node claims to be the leader.

      Parameters:
      nodes - non-null list of RaftNode instances
      Returns:
      InvariantResult with validation status
      Throws:
      NullPointerException - if nodes is null

    • checkLogMatching

      public static RaftInvariantChecker.InvariantResult checkLogMatching(RaftLog log1, RaftLog log2)
      Check Log Matching Property: if two logs contain an entry with the same index and term, all entries preceding that index are identical.

      Compares two logs entry-by-entry up to the minimum last index.

      Parameters:
      log1 - first RaftLog
      log2 - second RaftLog
      Returns:
      InvariantResult with validation status
      Throws:
      NullPointerException - if either log is null

    • checkCommitIndexMonotonicity

      public static RaftInvariantChecker.InvariantResult checkCommitIndexMonotonicity(long oldIndex, long newIndex)
      Check Commit Index Monotonicity: commitIndex never decreases.

      Verifies that oldIndex invalid input: '<'= newIndex.

      Parameters:
      oldIndex - previous commitIndex value
      newIndex - new commitIndex value
      Returns:
      InvariantResult with validation status

    • checkTermMonotonicity

      public static RaftInvariantChecker.InvariantResult checkTermMonotonicity(long oldTerm, long newTerm)
      Check Term Monotonicity: currentTerm never decreases.

      Verifies that oldTerm invalid input: '<'= newTerm.

      Parameters:
      oldTerm - previous currentTerm value
      newTerm - new currentTerm value
      Returns:
      InvariantResult with validation status

    • checkFencingTokenMonotonicity

      public static RaftInvariantChecker.InvariantResult checkFencingTokenMonotonicity(long oldToken, long newToken)
      Check Fencing Token Monotonicity: a fencing token never decreases.
      Parameters:
      oldToken - previous fencing token value
      newToken - new fencing token value
      Returns:
      InvariantResult with validation status

    • checkLeaderCompleteness

      public static RaftInvariantChecker.InvariantResult checkLeaderCompleteness(RaftNode leader, long commitIndex)
      Check Leader Completeness: if a log entry is committed, it is present in logs of all current and future leaders.

      For a leader, verifies that all entries up to commitIndex are present in its log.

      Note: This is a basic check. Full verification requires examining multiple leaders across term transitions, which is tested in integration scenarios.

      Parameters:
      leader - the RaftNode claiming leadership
      commitIndex - the leader's commitIndex
      Returns:
      InvariantResult with validation status
      Throws:
      NullPointerException - if leader is null

    • checkStateMachineSafety

      public static RaftInvariantChecker.InvariantResult checkStateMachineSafety(RaftLog log)
      Check State Machine Safety (basic): verify that the same state machine entry is not applied at the same index with different commands.

      This is a simplified version that checks entry consistency in the log. Full state machine safety requires external tracking of applied commands.

      Parameters:
      log - the RaftLog to check
      Returns:
      InvariantResult with validation status
      Throws:
      NullPointerException - if log is null