krabka_verified/
local_recovery.rs

1//! Local-log segment-chain and torn-tail recovery decisions.
2
3#[cfg(creusot)]
4use creusot_std::prelude::{DeepModel, Int, invariant, logic};
5
6#[krabka_macros::model_type]
7pub struct LocalRecoveryStep {
8    pub valid_end: u64,
9    pub last_offset: i64,
10    pub next_offset: i64,
11}
12
13/// What `Log::open` observes at one base offset that carries a compaction
14/// `.swap` file, from a single directory listing.
15///
16/// Compaction writes its survivor segment under `.cleaned` names, fsyncs it,
17/// renames the sidecars and then the log from `.cleaned` to `.swap`, and only
18/// after that rename is durable deletes the segments it replaces. So a
19/// `.log.swap` with no `.log.cleaned` beside it is a complete, durable segment,
20/// and it may already be the only copy of the records it holds.
21#[krabka_macros::model_type]
22pub struct LocalRecoverySwapFacts {
23    /// `<base>.log.cleaned` exists: the rewrite, or its rename to `.swap`,
24    /// never finished.
25    pub log_cleaned_exists: bool,
26    /// `<base>.log.swap` exists.
27    pub log_swap_exists: bool,
28    /// `<base>.log` exists.
29    pub final_log_exists: bool,
30}
31
32/// Crash-recovery action for one base offset that carries `.swap` files.
33#[krabka_macros::model_type]
34pub enum LocalRecoverySwapAction {
35    /// The swap never committed: delete its `.swap` files. No segment it
36    /// would replace has been touched.
37    AbortSwap,
38    /// The swap committed: delete every segment it replaces, then rename the
39    /// swap into place. This is Kafka's `LogLoader.load` second and third
40    /// passes.
41    CompleteSwap,
42    /// The log rename already finished; promote the remaining sidecars.
43    PromoteSidecars,
44    /// Sidecar swaps with no log in any form.
45    Reject,
46}
47
48mod index_frontier;
49#[cfg(creusot)]
50pub use index_frontier::swap_committed;
51pub use index_frontier::{
52    local_recovery_batch_step, local_recovery_index_frontier, local_recovery_sealed_last,
53    local_recovery_segment_chain, local_recovery_swap_action, local_recovery_swap_replaces,
54};
55
56#[cfg(test)]
57mod tests;
krabka_verified/local_recovery.rs

krabka_verified/
local_recovery.rs
