From af3bee64a57da3493ddc2d06c7de7efd553fce4e Mon Sep 17 00:00:00 2001 From: Julien Cretin Date: Fri, 1 Oct 2021 17:50:49 +0200 Subject: [PATCH] Introduce window size to fix hidden entries --- libraries/persistent_store/src/format.rs | 27 +++-- libraries/persistent_store/src/lib.rs | 130 +++++++++++++---------- libraries/persistent_store/src/store.rs | 4 +- 3 files changed, 96 insertions(+), 65 deletions(-) diff --git a/libraries/persistent_store/src/format.rs b/libraries/persistent_store/src/format.rs index a7dd4f5..5690b93 100644 --- a/libraries/persistent_store/src/format.rs +++ b/libraries/persistent_store/src/format.rs @@ -264,14 +264,23 @@ impl Format { self.bytes_to_words(self.max_value_len()) } + /// The virtual window size in words, denoted by W. + /// + /// This is the span of virtual storage that is accessible. In particular, all store content + /// fits within this window. + /// + /// We have W = (N - 1) × Q - M. + pub fn window_size(&self) -> Nat { + (self.num_pages() - 1) * self.virt_page_size() - self.max_prefix_len() + } + /// The total virtual capacity in words, denoted by V. /// - /// We have V = (N - 1) × (Q - 1) - M. + /// This is the span of virtual storage after which we trigger a compaction. This is smaller + /// than the virtual window because compaction may transiently overflow out of this virtual + /// capacity. /// - /// We can show V ≥ (N - 2) × (Q - 1) with the following steps: - /// - M ≤ Q - 1 from M < Q from [M](Format::max_prefix_len)'s definition - /// - -M ≥ -(Q - 1) from above - /// - V ≥ (N - 1) × (Q - 1) - (Q - 1) from V's definition + /// We have V = W - (N - 1) = (N - 1) × (Q - 1) - M. pub fn virt_size(&self) -> Nat { (self.num_pages() - 1) * (self.virt_page_size() - 1) - self.max_prefix_len() } @@ -281,9 +290,9 @@ impl Format { /// We have C = V - N = (N - 1) × (Q - 2) - M - 1. /// /// We can show C ≥ (N - 2) × (Q - 2) - 2 with the following steps: - /// - V ≥ (N - 2) × (Q - 1) from [V](Format::virt_size)'s definition - /// - C ≥ (N - 2) × (Q - 1) - N from C's definition - /// - (N - 2) × (Q - 1) - N = (N - 2) × (Q - 2) - 2 by calculus + /// - M ≤ Q - 1 from M < Q from [M](Format::max_prefix_len)'s definition + /// - C ≥ (N - 1) × (Q - 2) - (Q - 1) - 1 from C's definition + /// - C ≥ (N - 2) × (Q - 2) - 2 by calculus pub fn total_capacity(&self) -> Nat { // From the virtual capacity, we reserve N - 1 words for `Erase` entries and 1 word for a // `Clear` entry. @@ -353,7 +362,7 @@ impl Format { WordState::Partial } else { let tail = COMPACT_TAIL.get(word); - if tail > self.virt_size() + self.max_prefix_len() { + if tail > self.window_size() { return Err(StoreError::InvalidStorage); } WordState::Valid(CompactInfo { tail }) diff --git a/libraries/persistent_store/src/lib.rs b/libraries/persistent_store/src/lib.rs index 5ef8670..ca82a47 100644 --- a/libraries/persistent_store/src/lib.rs +++ b/libraries/persistent_store/src/lib.rs @@ -139,6 +139,7 @@ //! - [Q](format::Format::virt_page_size) = P - 2 the number of words in a virtual page. //! - [M](format::Format::max_prefix_len) = min(Q - 1, 256) the maximum length in words of a //! value. +//! - [W](format::Format::window_size) = (N - 1) × Q - M the window size. //! - [V](format::Format::virt_size) = (N - 1) × (Q - 1) - M the virtual capacity. //! - [C](format::Format::total_capacity) = V - N the user capacity. //! @@ -163,7 +164,8 @@ //! //! We define t\_i as one past the last entry of the window i. If there are no entries in that //! window, we have t\_i = h\_i. We call t\_i the tail of the window i. We define the compaction -//! invariant as t\_i - h\_i ≤ V. +//! invariant as t\_i - h\_i ≤ V and the window invariant as t\_i - h\_i ≤ W. The compaction +//! invariant may temporarily be broken during a sequence of (at most N - 1) compactions. //! //! We define |x| as the capacity used before position x. We have |x| ≤ x. We define the capacity //! invariant as |t\_i| - |h\_i| ≤ C. @@ -204,87 +206,107 @@ //! //! ## Compaction //! -//! It should always be possible to fully compact the store, after what the remaining capacity -//! should be available in the current window (restoring the compaction invariant). We consider all -//! notations on the virtual storage after the full compaction. We will use the |x| notation -//! although we update the state of the virtual storage. This is fine because compaction doesn't -//! change the status of an existing word. +//! Let I be a window at which all invariants hold. We will show that the next N - 1 compactions +//! will preserve the window invariant (the capacity invariant is trivially preserved) after each +//! compaction. We will also show that after N - 1 compactions, the compaction invariant is +//! restored. //! -//! We want to show that the next N - 1 compactions won't move the tail past the last page of their -//! window, with I the initial window: +//! We consider all notations on the virtual storage after the full compaction. We will use the |x| +//! notation although we update the state of the virtual storage. This is fine because compaction +//! doesn't change the status of an existing word. //! -//! | | | | | -//! | ----------------:| ----------:|:-:|:------------------- | -//! | ∀(1 ≤ i ≤ N - 1) | t\_{I + i} | ≤ | (I + i + N - 1) × Q | +//! We first show that after each compaction, the window invariant is preserved. +//! +//! ```text +//! ∀(1 ≤ i ≤ N - 1) t_{I + i} - h_{I + i} ≤ W +//! ``` //! //! We assume i between 1 and N - 1. //! //! One step of compaction advances the tail by how many words were used in the first page of the //! window with the last entry possibly overlapping on the next page. //! -//! | | | | | -//! | --:| ----------:|:-:|:------------------------------------ | -//! | ∀j | t\_{j + 1} | = | t\_j + \|h\_{j + 1}\| - \|h\_j\| + 1 | +//! ```text +//! ∀j t_{j + 1} = t_j + |h_{j + 1}| - |h_j| + 1 +//! ``` //! //! By induction, we have: //! -//! | | | | -//! | ----------:|:-:|:------------------------------------ | -//! | t\_{I + i} | ≤ | t\_I + \|h\_{I + i}\| - \|h\_I\| + i | +//! ```text +//! t_{I + i} = t_I + |h_{I + i}| - |h_I| + i +//! ``` //! //! We have the following properties: //! -//! | | | | -//! | -------------------------:|:-:|:----------------- | -//! | t\_I | ≤ | h\_I + V | -//! | \|h\_{I + i}\| - \|h\_I\| | ≤ | h\_{I + i} - h\_I | -//! | h\_{I + i} | ≤ | (I + i) × Q + M | +//! ```text +//! t_I ≤ h_I + V +//! |h_{I + i}| - |h_I| ≤ h_{I + i} - h_I +//! ``` //! //! Replacing into our previous equality, we can conclude: //! -//! | | | | -//! | ----------:|:-:| ------------------------------------------- | -//! | t\_{I + i} | = | t_I + \|h_{I + i}\| - \|h_I\| + i | -//! | | ≤ | h\_I + V + (I + i) * Q + M - h\_I + i | -//! | | = | (N - 1) × (Q - 1) - M + (I + i) × Q + M + i | -//! | | = | (N - 1) × (Q - 1) + (I + i) × Q + i | -//! | | = | (I + i + N - 1) × Q + i - (N - 1) | -//! | | ≤ | (I + i + N - 1) × Q | +//! ```text +//! t_{I + i} = t_I + |h_{I + i}| - |h_I| + i +//! ≤ h_I + V + h_{I + 1} - h_I + i +//! iff +//! t_{I + i} - h_{I + 1} ≤ V + i +//! ≤ V + N - 1 +//! = W +//! ``` //! -//! We also want to show that after N - 1 compactions, the remaining capacity is available without -//! compaction. +//! An important corollary is that the tail stays within the window: //! -//! | | | | -//! | -:| --------------------------------------------- | --------------------------------- | -//! | | V - (t\_{I + N - 1} - h\_{I + N - 1}) | The available words in the window | -//! | ≥ | C - (\|t\_{I + N - 1}\| - \|h\_{I + N - 1}\|) | The remaining capacity | -//! | + | 1 | Reserved for clear | +//! ```text +//! t_{I + i} ≤ (I + i + N - 1) × Q +//! ``` +//! +//! We have the following property: +//! +//! ```text +//! h_{I + i} ≤ (I + i) × Q + M +//! ``` +//! +//! From which we conclude with the definition of W: +//! +//! ```text +//! t_{I + i} ≤ h_{I + i} + W +//! ≤ (I + i) × Q + M + (N - 1) × Q - M +//! = (I + i + N - 1) × Q +//! ``` +//! +//! We finally show that after N - 1 compactions, the compaction invariant is restored. In +//! particular, the remaining capacity is available without compaction. +//! +//! ```text +//! V - (t_{I + N - 1} - h_{I + N - 1}) ≥ C - (|t_{I + N - 1}| - |h_{I + N - 1}|) + 1 +//! ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~ +//! immediate capacity remaining capacity | +//! reserved for clear +//! ``` //! //! We can replace the definition of C and simplify: //! -//! | | | | | -//! | ---:| -------------------------------------:|:-:|:----------------------------------------------------- | -//! | | V - (t\_{I + N - 1} - h\_{I + N - 1}) | ≥ | V - N - (\|t\_{I + N - 1}\| - \|h\_{I + N - 1}\|) + 1 | -//! | iff | t\_{I + N - 1} - h\_{I + N - 1} | ≤ | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| + N - 1 | +//! ```text +//! V - (t_{I + N - 1} - h_{I + N - 1}) ≥ V - N - (|t_{I + N - 1}| - |h_{I + N - 1}|) + 1 +//! iff t_{I + N - 1} - h_{I + N - 1} ≤ |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1 +//! ``` //! //! We have the following properties: //! -//! -//! | | | | | -//! | ---------------------------------------:|:-:|:-------------------------------------------- |:------ | -//! | t\_{I + N - 1} | = | t\_I + \|h\_{I + N - 1}\| - \|h\_I\| + N - 1 | | -//! | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| | = | \|t\_I\| - \|h\_I\| | Compaction preserves capacity | -//! | \|h\_{I + N - 1}\| - \|t\_I\| | ≤ | h\_{I + N - 1} - t\_I | | +//! ```text +//! t_{I + N - 1} = t_I + |h_{I + N - 1}| - |h_I| + N - 1 +//! |t_{I + N - 1}| - |h_{I + N - 1}| = |t_I| - |h_I| +//! |h_{I + N - 1}| - |t_I| ≤ h_{I + N - 1} - t_I +//! ``` //! //! From which we conclude: //! -//! | | | | | -//! | ---:| -------------------------------:|:-:|:----------------------------------------------- | -//! | | t\_{I + N - 1} - h\_{I + N - 1} | ≤ | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| + N - 1 | -//! | iff | t\_I + \|h\_{I + N - 1}\| - \|h\_I\| + N - 1 - h\_{I + N - 1} | ≤ | \|t\_I\| - \|h\_I\| + N - 1 | -//! | iff | t\_I + \|h\_{I + N - 1}\| - h\_{I + N - 1} | ≤ | \|t\_I\| | -//! | iff | \|h\_{I + N - 1}\| - \|t\_I\| | ≤ | h\_{I + N - 1} - t\_I | -//! +//! ```text +//! t_{I + N - 1} - h_{I + N - 1} ≤ |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1 +//! iff t_I + |h_{I + N - 1}| - |h_I| + N - 1 - h_{I + N - 1} ≤ |t_I| - |h_I| + N - 1 +//! iff t_I + |h_{I + N - 1}| - h_{I + N - 1} ≤ |t_I| +//! iff |h_{I + N - 1}| - |t_I| ≤ h_{I + N - 1} - t_I +//! ``` //! //! ## Checksum //! diff --git a/libraries/persistent_store/src/store.rs b/libraries/persistent_store/src/store.rs index 0d617dd..d1e50bd 100644 --- a/libraries/persistent_store/src/store.rs +++ b/libraries/persistent_store/src/store.rs @@ -532,7 +532,7 @@ impl Store { self.entries = Some(Vec::new()); let mut pos = or_invalid(self.head)?; let mut prev_pos = pos; - let end = pos + self.format.virt_size(); + let end = pos + self.format.window_size(); while pos < end { let entry_pos = pos; match self.parse_entry(&mut pos)? { @@ -789,7 +789,7 @@ impl Store { fn transaction_apply(&mut self, sorted_keys: &[Nat], marker: Position) -> StoreResult<()> { self.delete_keys(&sorted_keys, marker)?; self.set_padding(marker)?; - let end = or_invalid(self.head)? + self.format.virt_size(); + let end = or_invalid(self.head)? + self.format.window_size(); let mut pos = marker + 1; while pos < end { let entry_pos = pos;