From 4a9cc3ce2e75f2564dfe7ac16052b7044a3322de Mon Sep 17 00:00:00 2001
From: Julien Cretin <cretin@google.com>
Date: Sun, 22 Mar 2020 17:17:21 +0100
Subject: [PATCH] Add more details to the store documentation
---
src/embedded_flash/store/format.rs | 7 +++++--
src/embedded_flash/store/mod.rs | 22 ++++++++++++++++++++++
2 files changed, 27 insertions(+), 2 deletions(-)
diff --git a/src/embedded_flash/store/format.rs b/src/embedded_flash/store/format.rs
index 8308c4a..447506c 100644
--- a/src/embedded_flash/store/format.rs
+++ b/src/embedded_flash/store/format.rs
@@ -61,10 +61,13 @@ pub struct Format {
/// Whether a user entry has sensitive data.
///
- /// When a user entry with sensitive data is deleted, the data is overwritten with zeroes.
- ///
/// - 0 for sensitive data.
/// - 1 for non-sensitive data.
+ ///
+ /// When a user entry with sensitive data is deleted, the data is overwritten with zeroes. This
+ /// feature is subject to the same guarantees as all other features of the store, in particular
+ /// deleting a sensitive entry is atomic. See the store module-level documentation for more
+ /// information.
sensitive_bit: usize,
/// The data length of a user entry.
diff --git a/src/embedded_flash/store/mod.rs b/src/embedded_flash/store/mod.rs
index e2ed2fa..9453372 100644
--- a/src/embedded_flash/store/mod.rs
+++ b/src/embedded_flash/store/mod.rs
@@ -43,6 +43,28 @@
//! The data-structure can be configured with the `StoreConfig` trait. By implementing this trait,
//! the number of possible tags and the association between keys and entries are defined.
//!
+//! # Properties
+//!
+//! The data-structure provides the following properties:
+//! - When an operation returns success, then the represented multi-set is updated accordingly. For
+//! example, an inserted entry can be find with alteration until replaced or deleted.
+//! - When an operation returns an error, the resulting multi-set state is described in the error
+//! documentation.
+//! - When power is lost before an operation returns, the operation will either succeed or be
+//! rolled-back on the next initialization. So the multi-set would be either left unchanged or
+//! updated accordingly.
+//!
+//! Those properties rely on the following assumptions:
+//! - Writing a word to flash is atomic. When power is lost, the word is either fully written or not
+//! written at all.
+//! - Reading a word from flash is deterministic. When power is lost while writing or erasing a word
+//! (erasing a page containing that word), reading that word repeatedly returns the same result
+//! (until it is written or its page is erased).
+//! - To decide whether a page has been erased, it is enough to test if all its bits are equal to 1.
+//!
+//! The properties still hold outside those assumptions but with weaker probabilities as the usage
+//! diverges from the assumptions.
+//!
//! # Implementation
//!
//! The store is a page-aligned sequence of bits. It matches the following grammar:
--
GitLab