Abstract Specification of the UBIFS File System for Flash Memory
This page describes the KIV specifications and proofs done for the abstract specification
of the UBIFS flash file system in [FM 09] (see bibliography below). A preliminary version
of the paper is available from the authors). The project developed
(see
here for a graphical overwiew)
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 is 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.
Used basic libraries:
Here you can find all our publications.
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.