Added mdb_init() to set mdb root node to arbitrary address.
authorSimon Gerber <simon.gerber@inf.ethz.ch>
Tue, 17 Dec 2013 14:03:57 +0000 (15:03 +0100)
committerGerd Zellweger <mail@gerdzellweger.com>
Tue, 14 Oct 2014 06:47:38 +0000 (08:47 +0200)
This function is supposed to be used in conjunction with the value of mdb_root
in the kcb.  The function ensures that the value that is set is the root of a
valid mdb tree by running the sanity checks and invariant checks on the
address.

errors/errno.fugu
include/mdb/mdb_tree.h
lib/mdb/mdb_tree.c

index db3dddf..4764ec1 100644 (file)
@@ -143,6 +143,11 @@ errors libcaps CAPS_ERR_ {
     // general errors
     failure INVALID_ARGS        "Invalid arguments",
 
+    // restore errors
+    failure MDB_ALREADY_INITIALIZED "MDB not emtpy during restore",
+    failure MDB_INVALID_STATE       "MDB not in valid state after restore",
+    failure MDB_INVARIANT_VIOLATION "MDB invariant violated",
+
     // mdb operation errors
     failure MDB_DUPLICATE_ENTRY "Inserted entry already present",
     failure MDB_ENTRY_NOTFOUND  "Removed entry not found",
index 3d79286..a06ee86 100644 (file)
@@ -21,25 +21,41 @@ __BEGIN_DECLS
 struct capability;
 struct cte;
 
-enum {
-    // All checked invariants hold
-    MDB_INVARIANT_OK = 0,
-    // A node with level > 0 must have both children
-    MDB_INVARIANT_BOTHCHILDREN,
-    // The level of a node's left child must be lt the node's level
-    MDB_INVARIANT_LEFT_LEVEL_LESS,
-    // The level of a node's right child must be leq the node's level
-    MDB_INVARIANT_RIGHT_LEVEL_LEQ,
-    // The level of a node's right grandchildren must bt lt the node's level
-    MDB_INVARIANT_RIGHTRIGHT_LEVEL_LESS,
-    MDB_INVARIANT_RIGHTLEFT_LEVEL_LESS,
-    // The node's "end" value must be the maximum of the subtree's ends
-    MDB_INVARIANT_END_IS_MAX,
-    // The left child of a node must be earlier in the ordering
-    MDB_INVARIANT_LEFT_SMALLER,
-    // The right child of a node must be later in the ordering
-    MDB_INVARIANT_RIGHT_GREATER,
+#define mdb_invariants(f) \
+    /* All checked invariants hold*/\
+    f(MDB_INVARIANT_OK) \
+    /* A node with level > 0 must have both children*/\
+    f(MDB_INVARIANT_BOTHCHILDREN) \
+    /* The level of a node's left child must be lt the node's level*/\
+    f(MDB_INVARIANT_LEFT_LEVEL_LESS) \
+    /* The level of a node's right child must be leq the node's level*/\
+    f(MDB_INVARIANT_RIGHT_LEVEL_LEQ) \
+    /* The level of a node's right grandchildren must bt lt the node's level*/\
+    f(MDB_INVARIANT_RIGHTRIGHT_LEVEL_LESS) \
+    f(MDB_INVARIANT_RIGHTLEFT_LEVEL_LESS) \
+    /* The node's "end" value must be the maximum of the subtree's ends*/\
+    f(MDB_INVARIANT_END_IS_MAX) \
+    /* The left child of a node must be earlier in the ordering*/\
+    f(MDB_INVARIANT_LEFT_SMALLER) \
+    /* The right child of a node must be later in the ordering*/\
+    f(MDB_INVARIANT_RIGHT_GREATER)
+
+#define f_enum(x) x,
+enum mdb_invariant {
+    mdb_invariants(f_enum)
 };
+#undef f_enum
+
+#define f_str(x) #x,
+static const char *mdb_invariant_str[] = { mdb_invariants(f_str) };
+#undef f_str
+
+#undef mdb_invariants
+
+static inline const char *mdb_invariant_to_str(enum mdb_invariant i)
+{
+    return mdb_invariant_str[i];
+}
 
 enum {
     // No cap was found covering the specified region
@@ -52,6 +68,11 @@ enum {
     MDB_RANGE_FOUND_PARTIAL = 3,
 };
 
+// Restore mdb state by passing in the address of the root node
+// requires: mdb not initialized
+// ensures: mdb_check_invariants() && mdb_is_sane()
+errval_t mdb_init(lvaddr_t root_node);
+
 // Print the specified subtree
 void mdb_dump(struct cte *cte, int indent);
 // Print the complete tree
index 4b8d645..e81e66c 100644 (file)
@@ -76,6 +76,34 @@ mdb_dump_and_fail(struct cte *cte, int failure)
 struct cte *mdb_root = NULL;
 
 /*
+ * (re)initialization
+ */
+errval_t
+mdb_init(lvaddr_t root_node)
+{
+    if (mdb_root) {
+        printf("mdb already has root node, aborting\n");
+        return CAPS_ERR_MDB_ALREADY_INITIALIZED;
+    }
+    // set root
+    mdb_root = (struct cte *)root_node;
+    // check tree
+    if (!mdb_is_sane()) {
+        printf("restored mdb not in valid state\n");
+        mdb_root = NULL;
+        return CAPS_ERR_MDB_INVALID_STATE;
+    }
+    // always check invariants here
+    int i = mdb_check_invariants();
+    if (i) {
+        printf("mdb invariant %s violated\n", mdb_invariant_to_str(i));
+        mdb_root = NULL;
+        return CAPS_ERR_MDB_INVARIANT_VIOLATION;
+    }
+    return SYS_ERR_OK;
+}
+
+/*
  * Debug printing.
  */