kmwebnet/OpenSK
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Introduce window size to fix hidden entries

Browse Source
This commit is contained in:
Julien Cretin
2021-10-01 17:50:49 +02:00
committed by Julien Cretin
parent 9dc5286633
commit af3bee64a5
3 changed files with 96 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
libraries/persistent_store/src/format.rs
View File

@@ -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 })

130
libraries/persistent_store/src/lib.rs
View File

@@ -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
//!

4
libraries/persistent_store/src/store.rs
View File

@@ -532,7 +532,7 @@ impl<S: Storage> Store<S> {
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<S: Storage> Store<S> {
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;