KIV Proofs for the Correctness of Wandering Trees

This page documents the KIV formalization of

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif:
Refinement and Separation: Modular Verification of Wandering Trees.
Presented at iFM 2023.

Project Overview gives an overview of the entire specification hierarchy.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.

• The specification of the top-level component is map-asm.
  • It has a state consisting of two finite maps RS and FS. Both map finitely many keys (of type Key in the paper, here we use a totally ordered type Tord from the library) to values (type Elem). The interface contains the following operations:
    • init# initializes both maps to empty
    • contains# checks whether a key is in the map
    • lookup# returns the value stored under key, if it exsists (otherwise EXISTS = false is returned)
    • store# adds a key value pair
    • remove# removes a key
    • commit# copies RS to FS
    • recover# (called after a crash) restores RS from FS
    All operations specify that they may signal an error (by initially setting ERR to a random value) that may result from a problem with the hardware (flash memory may contain broken blocks that are no longer readable).
  • The effect of a crash:RS is initialized with the old value of FS before the crash (the old value is indicate by a backquote).
  • The component is based on an algebraic specification of maps. KIV's library also defines maplets and other separation logic operators (sep. conjunction, magic wand, sharing separation) over maps.
• The top-level component is implemented by the component tree-asm.
  • tree-asm has the same operations as map-asm, but it uses binary trees instead of maps.
  • The basic function implemented on this level is searching over an ordered tree (algorithm search#), which is called by the other operations.
  • The component has no state but calls atomic operations of a subcomponent treebasic-asm which encapsulates simple atomic operations on binary trees.
  • The state of treebasic-asm consists of two binary search trees 'Tree' and 'Backup' which correspond to 'RS' and 'FS'. Since there is no empty binary tree, two flags 'Empty' and 'BEmpty' are used (true when no tree is needed). The component also stores a 'Path' (a list of LEFT and RIGHT) as state with elementary operations to traverse down (by adding LEFT or RIGHT to the end) or up (by removing the last element).
  • Verification ensures that all operations of treebasic-asm are called only, when their precondition is true. Typically this includes a check "Path ∈ Tree" that asserts that Path points to a subtree of Tree. Setting the value of a leaf node (setValue#) or removing a lead (remove#) is possible only when Path points to a leaf, checked with "Tree[Path].leaf?".
  • The component is based on an algebraic specification binary trees. Additional functions and predicates are used to check whether a path is contained in a tree, to select the subtree at some path, and to update a tree at a path.
  • The specification of paths is as a list of LEFT/RIGHT markers.
• The refinement from map-asm to tree-asm is proven to be correct with respect to a forward simulation absS in the theorem base of specification map-refine, which contains proofs for the proof obligations of the contract approach to data refinement (refine-store is e.g. the one for the store# operation).
• The proof obligations all roughly have the form "abs(as,cs), apre(as) ⊦ ⟪cop(cs)⟫⟨aop(as)⟩ abs(as,cs)" which asserts that given a pair of states related by the abstraction relation, where the abstract state satisfies the precondition of aop, then all runs of cop terminate, and for each run of cop a suitable run of aop exists, that terminates in a state where abs holds again (if there are outputs, then both are equal).
• While tree-asm contains algorithms of the final implementation, the basic operations of treebasic-asm are again a specification, which is implemented by the component wandering-tree-asm.
  • This component implements the atomic operations of treebasic-asm.
  • The 'Tree' is now implemented as a tree with proxy-nodes (of the algebraic type Proxytree with again some additional functions and predicates).
  • A proxynode may now point to an address on flash memory. If the address is null, then the node is dirty, i.e. it currently has no backup on flash memory.
  • The 'Backup' tree as well as the trees that are pointed to by proxynodes are now represented as a forest, i.e. a map that stores trees under addresses.
  • Again, the state is not stored in wanderingtree-asm, but in two subcomponents, that offer simple operations on the state: ram-asm stores the part that is kept in RAM, which is the proxytree 'RTree' together with a path 'CurPath' that points to some node (note that its operations do not have an ERR return value as this component does not access the hardware), and forest-asm stores the part that is stored on flash memory, which consists of the forest 'Forest', and a pointer 'FRoot' which points to the address where (the representation of) 'Backup' is stored.
  • The important algorithms implemented in wandering-tree-asm are
    • load#: loads a node of the tree from 'Forest' to 'RTree' (called from e.g. getValue#)
    • setDirty#: traverses upwards from 'CurPath' to the root setting all nodes to dirty
    • save#: recursively traverses the tree downward saving all dirty nodes (called from commit#).
    • remove# deletes the leaf at CurPath (loading nodes as necessary).
  • The operations of wandering-tree-asm satisfy some important invariants, given at the start of the specification under 'invariants'. Their definitions are given here. Proofs that the invariants are preserved (and all algorithms terminate) can be found in its theorem base (named 'inv-'). The theorem base also contains proof obligations for crash-safety (named 'crash-neutral-').
• The proof obligations for a correct refinement from tree-asm to wandering-tree-asm are proven in the theorem base of tree-refine. The full abstraction relation used is given in its specification.
• While the algorithms of wandering-tree-asm are part of the final implementation, ram-asm and forest-asm are still specifications which represent data inefficiently. In particular, forest-asm contains some contracts which are not directly executable:
  • Finding the address of the left/right subtree of a tree (in operations getLeft#/getRight#) is 'implemented' using the 'choose' operator which just chooses its address.
  • That this always works is ensured by the invariant invForest (specified here) which asserts that the trees stores in Forest are always downwards closed.
• The final two refinements from ram-asm to heap-asm and from forest-asm to flash-asm are used to represent data efficiently.
• heap-asm represents the proxytree a pointer structure stored in the (RAM) heap.
  The heap is a map from references (type 'Ref(Hnode)') to nodes on the heap (type 'Hnode').
  • The 'CurPath' is now simply represented a reference 'CurRef'.
  • The heap nodes contain a parent pointer. Shortening the path (moving up in the tree) is simply implementing by setting 'CurRef' to the parent pointer.
• The proof obligations for a correct refinement from ram-asm to heap-asm are discharged over specification ram-refine. The main predicate 'abs' used in the abstraction is based on separation logic. It is defined here.
• The last refinement refines forest-asm with flash-asm. Again the inefficient representation of forest-asm which stores all subtrees separately is replaced with a shared representation, which is a map from addresses (type 'Address') to flash nodes (type 'Fnode') stored sequentially (by saveLeaf#/saveNode#) on flash memory.
• The proof obligations for a correct refinement from forest-asm to flash-asm are discharged over specification flash-refine. The main predicate 'absF' used in the abstraction is based on using sharing separation from separation logic. It is defined here.

Used basic libraries:

• The basic KIV library with basic data types.
• KIV separation library with a formalization of Separation Logic.

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

[Imprint] [Data Privacy Statement] [E-Mail]