Continue compacting until content fits window during compaction

Also increase the virtual window size.
This commit is contained in:
Julien Cretin
2021-09-25 16:29:19 +02:00
committed by Julien Cretin
parent a3965eac2d
commit 67fa8bee0b
3 changed files with 53 additions and 34 deletions

View File

@@ -266,24 +266,24 @@ impl Format {
/// The total virtual capacity in words, denoted by V.
///
/// We have V = (N - 1) × (Q - 1) - M.
/// We have V = (N - 1) × Q - M - 1.
///
/// 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 can show V ≥ (N - 2) × Q with the following steps:
/// - M + 1 ≤ Q from M < Q from [M](Format::max_prefix_len)'s definition
/// - -M - 1 ≥ -Q from above
/// - V ≥ (N - 1) × Q - Q from V's definition
pub fn virt_size(&self) -> Nat {
(self.num_pages() - 1) * (self.virt_page_size() - 1) - self.max_prefix_len()
(self.num_pages() - 1) * self.virt_page_size() - self.max_prefix_len() - 1
}
/// The total user capacity in words, denoted by C.
///
/// We have C = V - N = (N - 1) × (Q - 2) - M - 1.
/// We have C = V - N = (N - 1) × (Q - 1) - M - 2.
///
/// 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
/// We can show C ≥ (N - 2) × (Q - 1) - 2 with the following steps:
/// - V ≥ (N - 2) × Q from [V](Format::virt_size)'s definition
/// - C ≥ (N - 2) × Q - N from C's definition
/// - (N - 2) × Q - N = (N - 2) × (Q - 1) - 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.