UBIFS Concepts

This page archives the formal model accompanying the publication:

1. Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif: Abstract Specification of the UBIFS File System for Flash Memory. In Proc. of FM 2009, Eindhoven, Netherlands.

Back to the main site.

The project developed (see here for a graphical overview) consists of the following important specifications:

• For the interface to the Linux VFS, file descriptors, directory entries ("dentries") and inodes are specified.
• The main data structure used in UBIFS is nodes. Nodes come in three variants:
  • They may store the information of an inode.
  • They may also specify a directory entry.
  • Finally they may contain a page of raw data of a file.
• Nodes are stored in the file store, which maps a finite number of addresses to nodes. This is the main data structure for storing data on flash memory.
• The file store itself is derived from a generic definition of stores imported from KIV's library of data types. A store is a partial function, that maps finitely many elements of the parameter type elem to values of parameter type data. Two instances are used: the file store, which maps addresses to nodes, and the index type which map keys to addresses.
• keys are used in two indexes, one stored in flash memory, and one only kept in RAM. Keys are references for nodes, therefore they also come in three variants:
  • An inodekey references an inode by its number
  • A dentrykey gives the inode number of the containing directory and the name of the file (our model uses the name; in reality a hash value is used).
  • A datakey references a page of data, by the inode number identifying the file and the part number, which says which part of the file the page contains.
• The full file system consists of the file store (variable fs), the RAM (variable ri) and the flash index (fi), and the journal (log), which in our abstract model is just a list of addresses. It is derived from a specification of lists (with several subspecifications) from the library.
• Specification filesystem-base contains basic operations and predicates for the file system: fs-cons and a number of auxiliary predicates (fs-dir-cons, fs-file-cons, valid-ino etc.) specify consistency of the file system. Predicate iso specifies, when two file systems are isomorphic, i.e. have the same relevant data (used to specify garbage collection). A large number of simplification rules is proved over this specification.
• Specification filesystem-asm defines all the operations for the file system. The top level operation FSOP#, that selects suitable input data (with choose) and calls one of the operations nondeterministically is just to conform to the convention of ASMs which requires one toplevel rule. Note, that although the syntax used is ASM-like, the operations are not executed atomically (as an ASM rule): the semantics of KIV's temporal logic only executes parallel assignments atomically.
• The theorem base of this specification contains the bulk of the proofs:
  • Theorems term-op prove termination of each operation op.
  • prepost-op prove total correctness assertions with suitable pre and postconditions.
  • fscons-op prove that fs-cons an invariant of the operations. store-cons-op and several more are similar for other predicates.
• Specification filesystem is the toplevel specification. It defines the log-cons predicate using the replay# operation. The theorem base has proof that log-cons is also an invariant of all operations.