krabka_verified/
uniform_assignor.rs

1//! Uniform group-assignor kernels (KIP-848 `UniformAssignor`).
2//!
3//! Kafka's server-side `UniformAssignor`
4//! (`org.apache.kafka.coordinator.group.assignor`) picks one of two builders.
5//! `UniformHomogeneousAssignmentBuilder` runs when every member subscribes to
6//! the same topics, and `UniformHeterogeneousAssignmentBuilder` runs
7//! otherwise. Both rank balance ahead of stickiness, and neither consults
8//! replica racks. This module holds the two decisions that the builders make
9//! about members: the quota each member gets in the homogeneous builder, and
10//! the least-loaded subscriber that receives an unassigned partition in the
11//! heterogeneous builder. The host in `krabka-broker` owns the partition
12//! bookkeeping around them.
13
14use creusot_std::prelude::*;
15
16/// Kafka's floor-and-remainder split of a partition total over the members.
17#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
18pub struct UniformQuotaSplit {
19    /// `minimumMemberQuota`: every member gets at least this many partitions.
20    pub minimum_quota: usize,
21    /// `remainingMembersToGetAnExtraPartition`: this many members get one
22    /// partition more than `minimum_quota`.
23    pub extra_quotas: usize,
24}
25
26/// One member's quota in the homogeneous builder.
27#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
28pub struct HomogeneousMemberQuota {
29    /// Whether the member's target is `minimum_quota + 1`, not
30    /// `minimum_quota`.
31    pub takes_extra: bool,
32    /// How many partitions the member keeps from its current assignment.
33    pub retain: usize,
34    /// How many unassigned partitions the member receives.
35    pub fill: usize,
36}
37
38/// A subscriber's load while the heterogeneous builder assigns one topic.
39#[krabka_macros::model_type(proof(std::clone::Clone, Copy))]
40pub struct SubscriberLoad {
41    /// Partitions the member holds now, across every topic.
42    pub assigned: usize,
43    /// Partitions the member held when the builder started on this topic.
44    pub assigned_at_topic_start: usize,
45}
46
47mod select_least_loaded;
48#[cfg(creusot)]
49pub use select_least_loaded::{
50    extras_left_before, keeps_extra_quota, load_precedes, member_target,
51};
52pub use select_least_loaded::{
53    homogeneous_member_quotas, select_least_loaded, uniform_quota_split,
54};
55
56#[cfg(test)]
57mod tests;
krabka_verified/uniform_assignor.rs

krabka_verified/
uniform_assignor.rs
