From f51264583747624d7e7c1fb6d2fe34492d44e745 Mon Sep 17 00:00:00 2001 From: Julien Cretin Date: Tue, 13 Oct 2020 12:46:25 +0200 Subject: [PATCH] Improve documentation --- libraries/persistent_store/src/format.rs | 12 ++++++++++-- libraries/persistent_store/src/lib.rs | 19 ++++++++++++++----- 2 files changed, 24 insertions(+), 7 deletions(-) diff --git a/libraries/persistent_store/src/format.rs b/libraries/persistent_store/src/format.rs index 147f318..4969e6d 100644 --- a/libraries/persistent_store/src/format.rs +++ b/libraries/persistent_store/src/format.rs @@ -456,8 +456,15 @@ bitfield! { LEN_COMPACT: Length, } -// Overview of the first word of the different kind of entries: +// Overview of the first word of the different kind of entries. // +// Each column represents a bit of the word. The first 2 lines give the position in hexadecimal of +// the bit in the word (the exponent of 2 when the word is written in binary). Each entry starts +// with the sequence of bits of its identifier. The dots following the identifier are the number of +// bits necessary to hold the information of the entry (including the checksum). The remaining free +// bits after the dots are not used by the entry. +// +// 0 1 // 0123456789abcdef0123456789abcdef // padding 0 // header 10.............................. @@ -466,7 +473,8 @@ bitfield! { // marker 11010.......... // remove 11011................. // -// NOTE: We could pad the internal entries to the right. +// NOTE: We could pad the internal entries to the right by extending their identifier. This permits +// to free some space for shorter identifier for future kind of entries. // The fields of a padding entry. bitfield! { diff --git a/libraries/persistent_store/src/lib.rs b/libraries/persistent_store/src/lib.rs index 20f5088..6e358a9 100644 --- a/libraries/persistent_store/src/lib.rs +++ b/libraries/persistent_store/src/lib.rs @@ -95,7 +95,7 @@ //! The _total lifetime_ of the store is below `L = ((E + 1) * N - 1) * (P - 2)` and //! above `L - M` words, where `E` is the maximum number of erase cycles. The //! lifetime is used when capacity is used, including transiently, as well as when -//! compaction occurs. Compaction frequency and litetime consumption are positively +//! compaction occurs. Compaction frequency and lifetime consumption are positively //! correlated to the store load factor (the ratio of used capacity to total capacity). //! //! It is possible to approximate the cost of transient words in terms of capacity: @@ -125,8 +125,8 @@ //! It is preferred to use `Clear` with a threshold of 0 to keep the lifetime //! tracking. //! -//! The store properties may still hold outside some of those assumptions but with -//! weaker probabilities as the usage diverges from them. +//! The store properties may still hold outside some of those assumptions, but with +//! an increasing chance of failure. //! //! # Implementation //! @@ -301,9 +301,18 @@ //! erased word. Marking an entry as padding or deleted is a single bit operation, //! so the property trivially holds. For those cases, the proof relies on the fact //! that there is exactly one bit equal to 0 in the 3 first bits. Either the 3 first -//! bits are still `111` in which case we expect the remaining bits to bit equal +//! bits are still `111` in which case we expect the remaining bits to be equal //! to 1. Otherwise we can use the checksum of the given type of entry because those -//! 2 types of entries are not reachable from each other. +//! 2 types of entries are not reachable from each other. Here is a visualization of +//! the partitioning based on the first 3 bits: +//! +//! | First 3 bits | Description | How to check | +//! | ------------:| ------------------ | ---------------------------- | +//! | `111` | Erased word | All bits set to `1` | +//! | `101` | User entry | Contains a checksum | +//! | `110` | Internal entry | Contains a checksum | +//! | `100` | Deleted user entry | No check, atomically written | +//! | `0??` | Padding entry | No check, atomically written | //! //! To show that valid entries of a given type are not reachable from each other, we //! show 3 lemmas: