|
41 | 41 | //! [1023](format::Format::max_value_len) bytes (for large enough pages).
|
42 | 42 | //!
|
43 | 43 | //! The store provides the following _updates_:
|
44 |
| -//! - Given a key and a value, [`StoreUpdate::Insert`] updates the store such that the value is |
45 |
| -//! associated with the key. The values for other keys are left unchanged. |
46 |
| -//! - Given a key, [`StoreUpdate::Remove`] updates the store such that no value is associated with |
47 |
| -//! the key. The values for other keys are left unchanged. Additionally, if there was a value |
48 |
| -//! associated with the key, the value is wiped from the storage (all its bits are set to 0). |
| 44 | +//! - Given a key and a value, [`StoreUpdate::Insert`] updates the store such that the value is |
| 45 | +//! associated with the key. The values for other keys are left unchanged. |
| 46 | +//! - Given a key, [`StoreUpdate::Remove`] updates the store such that no value is associated with |
| 47 | +//! the key. The values for other keys are left unchanged. Additionally, if there was a value |
| 48 | +//! associated with the key, the value is wiped from the storage (all its bits are set to 0). |
49 | 49 | //!
|
50 | 50 | //! The store provides the following _read-only operations_:
|
51 |
| -//! - [`Store::iter`] iterates through the store returning all entries exactly once. The iteration |
52 |
| -//! order is not specified but stable between mutable operations. |
53 |
| -//! - [`Store::capacity`] returns how many words can be stored before the store is full. |
54 |
| -//! - [`Store::lifetime`] returns how many words can be written before the storage lifetime is |
55 |
| -//! consumed. |
| 51 | +//! - [`Store::iter`] iterates through the store returning all entries exactly once. The iteration |
| 52 | +//! order is not specified but stable between mutable operations. |
| 53 | +//! - [`Store::capacity`] returns how many words can be stored before the store is full. |
| 54 | +//! - [`Store::lifetime`] returns how many words can be written before the storage lifetime is |
| 55 | +//! consumed. |
56 | 56 | //!
|
57 | 57 | //! The store provides the following _mutable operations_:
|
58 |
| -//! - Given a set of independent updates, [`Store::transaction`] applies the sequence of updates. |
59 |
| -//! - Given a threshold, [`Store::clear`] removes all entries with a key greater or equal to the |
60 |
| -//! threshold. |
61 |
| -//! - Given a length in words, [`Store::prepare`] makes one step of compaction unless that many |
62 |
| -//! words can be written without compaction. This operation has no effect on the store but may |
63 |
| -//! still mutate its storage. In particular, the store has the same capacity but a possibly |
64 |
| -//! reduced lifetime. |
| 58 | +//! - Given a set of independent updates, [`Store::transaction`] applies the sequence of updates. |
| 59 | +//! - Given a threshold, [`Store::clear`] removes all entries with a key greater or equal to the |
| 60 | +//! threshold. |
| 61 | +//! - Given a length in words, [`Store::prepare`] makes one step of compaction unless that many |
| 62 | +//! words can be written without compaction. This operation has no effect on the store but may |
| 63 | +//! still mutate its storage. In particular, the store has the same capacity but a possibly |
| 64 | +//! reduced lifetime. |
65 | 65 | //!
|
66 | 66 | //! A mutable operation is _atomic_ if, when power is lost during the operation, the store is either
|
67 | 67 | //! updated (as if the operation succeeded) or left unchanged (as if the operation did not occur).
|
68 | 68 | //! If the store is left unchanged, lifetime may still be consumed.
|
69 | 69 | //!
|
70 | 70 | //! The store relies on the following _storage interface_:
|
71 |
| -//! - It is possible to [read](Storage::read_slice) a byte slice. The slice won't span multiple |
72 |
| -//! pages. |
73 |
| -//! - It is possible to [write](Storage::write_slice) a word slice. The slice won't span multiple |
74 |
| -//! pages. |
75 |
| -//! - It is possible to [erase](Storage::erase_page) a page. |
76 |
| -//! - The pages are sequentially indexed from 0. If the actual underlying storage is segmented, |
77 |
| -//! then the storage layer should translate those indices to actual page addresses. |
| 71 | +//! - It is possible to [read](Storage::read_slice) a byte slice. The slice won't span multiple |
| 72 | +//! pages. |
| 73 | +//! - It is possible to [write](Storage::write_slice) a word slice. The slice won't span multiple |
| 74 | +//! pages. |
| 75 | +//! - It is possible to [erase](Storage::erase_page) a page. |
| 76 | +//! - The pages are sequentially indexed from 0. If the actual underlying storage is segmented, then |
| 77 | +//! the storage layer should translate those indices to actual page addresses. |
78 | 78 | //!
|
79 | 79 | //! The store has a _total capacity_ of C = (N - 1) * (P - 4) - M - 1 words, where:
|
80 |
| -//! - P is the number of words per page |
81 |
| -//! - [N](format::Format::num_pages) is the number of pages |
82 |
| -//! - [M](format::Format::max_prefix_len) is the maximum length in words of a value (256 for large |
83 |
| -//! enough pages) |
| 80 | +//! - P is the number of words per page |
| 81 | +//! - [N](format::Format::num_pages) is the number of pages |
| 82 | +//! - [M](format::Format::max_prefix_len) is the maximum length in words of a value (256 for large |
| 83 | +//! enough pages) |
84 | 84 | //!
|
85 | 85 | //! The capacity used by each mutable operation is given below (a transient word only uses capacity
|
86 | 86 | //! during the operation):
|
|
108 | 108 | //! ## Preconditions
|
109 | 109 | //!
|
110 | 110 | //! The following assumptions need to hold, or the store may behave in unexpected ways:
|
111 |
| -//! - A word can be written [twice](Storage::max_word_writes) between erase cycles. |
112 |
| -//! - A page can be erased [E](Storage::max_page_erases) times after the first boot of the store. |
113 |
| -//! - When power is lost while writing a slice or erasing a page, the next read returns a slice |
114 |
| -//! where a subset (possibly none or all) of the bits that should have been modified have been |
115 |
| -//! modified. |
116 |
| -//! - Reading a slice is deterministic. When power is lost while writing a slice or erasing a |
117 |
| -//! slice (erasing a page containing that slice), reading that slice repeatedly returns the same |
118 |
| -//! result (until it is overwritten or its page is erased). |
119 |
| -//! - To decide whether a page has been erased, it is enough to test if all its bits are equal |
120 |
| -//! to 1. |
121 |
| -//! - When power is lost while writing a slice or erasing a page, that operation does not count |
122 |
| -//! towards the limits. However, completing that write or erase operation would count towards |
123 |
| -//! the limits, as if the number of writes per word and number of erase cycles could be |
124 |
| -//! fractional. |
125 |
| -//! - The storage is only modified by the store. Note that completely erasing the storage is |
126 |
| -//! supported, essentially losing all content and lifetime tracking. It is preferred to use |
127 |
| -//! [`Store::clear`] with a threshold of 0 to keep the lifetime tracking. |
| 111 | +//! - A word can be written [twice](Storage::max_word_writes) between erase cycles. |
| 112 | +//! - A page can be erased [E](Storage::max_page_erases) times after the first boot of the store. |
| 113 | +//! - When power is lost while writing a slice or erasing a page, the next read returns a slice |
| 114 | +//! where a subset (possibly none or all) of the bits that should have been modified have been |
| 115 | +//! modified. |
| 116 | +//! - Reading a slice is deterministic. When power is lost while writing a slice or erasing a slice |
| 117 | +//! (erasing a page containing that slice), reading that slice repeatedly returns the same result |
| 118 | +//! (until it is overwritten or its page is erased). |
| 119 | +//! - To decide whether a page has been erased, it is enough to test if all its bits are equal to 1. |
| 120 | +//! - When power is lost while writing a slice or erasing a page, that operation does not count |
| 121 | +//! towards the limits. However, completing that write or erase operation would count towards the |
| 122 | +//! limits, as if the number of writes per word and number of erase cycles could be fractional. |
| 123 | +//! - The storage is only modified by the store. Note that completely erasing the storage is |
| 124 | +//! supported, essentially losing all content and lifetime tracking. It is preferred to use |
| 125 | +//! [`Store::clear`] with a threshold of 0 to keep the lifetime tracking. |
128 | 126 | //!
|
129 | 127 | //! The store properties may still hold outside some of those assumptions, but with an increasing
|
130 | 128 | //! chance of failure.
|
131 | 129 | //!
|
132 | 130 | //! # Implementation
|
133 | 131 | //!
|
134 | 132 | //! We define the following constants:
|
135 |
| -//! - [E](format::Format::max_page_erases) <= [65535](format::MAX_ERASE_CYCLE) the number of times |
136 |
| -//! a page can be erased. |
137 |
| -//! - 3 <= [N](format::Format::num_pages) < 64 the number of pages in the storage. |
138 |
| -//! - 8 <= P <= 1024 the number of words in a page. |
139 |
| -//! - [Q](format::Format::virt_page_size) = P - 2 the number of words in a virtual page. |
140 |
| -//! - [M](format::Format::max_prefix_len) = min(Q - 1, 256) the maximum length in words of a |
141 |
| -//! value. |
142 |
| -//! - [W](format::Format::window_size) = (N - 1) * Q - M the window size. |
143 |
| -//! - [V](format::Format::virt_size) = (N - 1) * (Q - 1) - M the virtual capacity. |
144 |
| -//! - [C](format::Format::total_capacity) = V - N the user capacity. |
| 133 | +//! - [E](format::Format::max_page_erases) <= [65535](format::MAX_ERASE_CYCLE) the number of times a |
| 134 | +//! page can be erased. |
| 135 | +//! - 3 <= [N](format::Format::num_pages) < 64 the number of pages in the storage. |
| 136 | +//! - 8 <= P <= 1024 the number of words in a page. |
| 137 | +//! - [Q](format::Format::virt_page_size) = P - 2 the number of words in a virtual page. |
| 138 | +//! - [M](format::Format::max_prefix_len) = min(Q - 1, 256) the maximum length in words of a value. |
| 139 | +//! - [W](format::Format::window_size) = (N - 1) * Q - M the window size. |
| 140 | +//! - [V](format::Format::virt_size) = (N - 1) * (Q - 1) - M the virtual capacity. |
| 141 | +//! - [C](format::Format::total_capacity) = V - N the user capacity. |
145 | 142 | //!
|
146 | 143 | //! We build a virtual storage from the physical storage using the first 2 words of each page:
|
147 |
| -//! - The first word contains the number of times the page has been erased. |
148 |
| -//! - The second word contains the starting word to which this page is being moved during |
149 |
| -//! compaction. |
| 144 | +//! - The first word contains the number of times the page has been erased. |
| 145 | +//! - The second word contains the starting word to which this page is being moved during |
| 146 | +//! compaction. |
150 | 147 | //!
|
151 | 148 | //! The virtual storage has a length of (E + 1) * N * Q words and represents the lifetime of the
|
152 | 149 | //! store. (We reserve the last Q + M words to support adding emergency lifetime.) This virtual
|
|
177 | 174 | //!
|
178 | 175 | //! Entries are identified by a prefix of bits. The prefix has to contain at least one bit set to
|
179 | 176 | //! zero to differentiate from the tail. Entries can be one of:
|
180 |
| -//! - [Padding](format::ID_PADDING): A word whose first bit is set to zero. The rest is arbitrary. |
181 |
| -//! This entry is used to mark words partially written after an interrupted operation as padding |
182 |
| -//! such that they are ignored by future operations. |
183 |
| -//! - [Header](format::ID_HEADER): A word whose second bit is set to zero. It contains the |
184 |
| -//! following fields: |
185 |
| -//! - A [bit](format::HEADER_DELETED) indicating whether the entry is deleted. |
186 |
| -//! - A [bit](format::HEADER_FLIPPED) indicating whether the value is word-aligned and has all |
187 |
| -//! bits set to 1 in its last word. The last word of an entry is used to detect that an |
188 |
| -//! entry has been fully written. As such it must contain at least one bit equal to zero. |
189 |
| -//! - The [key](format::HEADER_KEY) of the entry. |
190 |
| -//! - The [length](format::HEADER_LENGTH) in bytes of the value. The value follows the header. |
191 |
| -//! The entry is word-aligned if the value is not. |
192 |
| -//! - The [checksum](format::HEADER_CHECKSUM) of the first and last word of the entry. |
193 |
| -//! - [Erase](format::ID_ERASE): A word used during compaction. It contains the |
194 |
| -//! [page](format::ERASE_PAGE) to be erased and a [checksum](format::WORD_CHECKSUM). |
195 |
| -//! - [Clear](format::ID_CLEAR): A word used during the clear operation. It contains the |
196 |
| -//! [threshold](format::CLEAR_MIN_KEY) and a [checksum](format::WORD_CHECKSUM). |
197 |
| -//! - [Marker](format::ID_MARKER): A word used during a transaction. It contains the [number of |
198 |
| -//! updates](format::MARKER_COUNT) following the marker and a [checksum](format::WORD_CHECKSUM). |
199 |
| -//! - [Remove](format::ID_REMOVE): A word used inside a transaction. It contains the |
200 |
| -//! [key](format::REMOVE_KEY) of the entry to be removed and a |
201 |
| -//! [checksum](format::WORD_CHECKSUM). |
| 177 | +//! - [Padding](format::ID_PADDING): A word whose first bit is set to zero. The rest is arbitrary. |
| 178 | +//! This entry is used to mark words partially written after an interrupted operation as padding |
| 179 | +//! such that they are ignored by future operations. |
| 180 | +//! - [Header](format::ID_HEADER): A word whose second bit is set to zero. It contains the following |
| 181 | +//! fields: |
| 182 | +//! - A [bit](format::HEADER_DELETED) indicating whether the entry is deleted. |
| 183 | +//! - A [bit](format::HEADER_FLIPPED) indicating whether the value is word-aligned and has all |
| 184 | +//! bits set to 1 in its last word. The last word of an entry is used to detect that an entry |
| 185 | +//! has been fully written. As such it must contain at least one bit equal to zero. |
| 186 | +//! - The [key](format::HEADER_KEY) of the entry. |
| 187 | +//! - The [length](format::HEADER_LENGTH) in bytes of the value. The value follows the header. |
| 188 | +//! The entry is word-aligned if the value is not. |
| 189 | +//! - The [checksum](format::HEADER_CHECKSUM) of the first and last word of the entry. |
| 190 | +//! - [Erase](format::ID_ERASE): A word used during compaction. It contains the |
| 191 | +//! [page](format::ERASE_PAGE) to be erased and a [checksum](format::WORD_CHECKSUM). |
| 192 | +//! - [Clear](format::ID_CLEAR): A word used during the clear operation. It contains the |
| 193 | +//! [threshold](format::CLEAR_MIN_KEY) and a [checksum](format::WORD_CHECKSUM). |
| 194 | +//! - [Marker](format::ID_MARKER): A word used during a transaction. It contains the [number of |
| 195 | +//! updates](format::MARKER_COUNT) following the marker and a [checksum](format::WORD_CHECKSUM). |
| 196 | +//! - [Remove](format::ID_REMOVE): A word used inside a transaction. It contains the |
| 197 | +//! [key](format::REMOVE_KEY) of the entry to be removed and a [checksum](format::WORD_CHECKSUM). |
202 | 198 | //!
|
203 | 199 | //! Checksums are the number of bits equal to 0.
|
204 | 200 | //!
|
|
336 | 332 | //!
|
337 | 333 | //! To show that valid entries of a given type are not reachable from each other, we show 3 lemmas:
|
338 | 334 | //!
|
339 |
| -//! 1. A bit sequence is not reachable from another if its number of bits equal to 0 is smaller. |
340 |
| -//! 2. A bit sequence is not reachable from another if they have the same number of bits equals to |
341 |
| -//! 0 and are different. |
342 |
| -//! 3. A bit sequence is not reachable from another if it is bigger when they are interpreted as |
343 |
| -//! numbers in binary representation. |
| 335 | +//! 1. A bit sequence is not reachable from another if its number of bits equal to 0 is smaller. |
| 336 | +//! 2. A bit sequence is not reachable from another if they have the same number of bits equals to 0 |
| 337 | +//! and are different. |
| 338 | +//! 3. A bit sequence is not reachable from another if it is bigger when they are interpreted as |
| 339 | +//! numbers in binary representation. |
344 | 340 | //!
|
345 | 341 | //! From those lemmas we consider the 2 cases. If both entries have the same number of bits equal to
|
346 | 342 | //! 0, they are either equal or not reachable from each other because of the second lemma. If they
|
|
0 commit comments