Transcript PowerPoint

Using Alcoa to Specify a UNIX
File System
Specification of some structures and
operations in a File System
Alcoa
• Predicate logic to specify a system of
objects. (quantifiers, subsets, relations)
• Can only describe a two state relationship.
Missing a sequential composition operator.
OK
NO
current
time0
next
time1
time2
Alcoa
domain
{I
partition
entries:
pointsToI
//
no
Root
h
Root.p
//
Only
f
all
o:
Di
//
no
No
dir
o
:
Di
Alcoa Tool
• Finds an instance which satisfies the
specification.
– Finds contradictions.
– See an example of the specification.
• Preservation of some logical statement
through an operation.
current
operation
next
Invariant holds
here.
Does invariant
hold here?
a & b | c is true
Is a’ & b’ | c’ true?
Alcoa will check this and give counterexamples
if not true.
File System Basics
Directory Entry
Inode
Directory Entry
Inode
Directory Entry
File System Basics
Directory Entry
2
Inode
Directory Entry
1
Inode
Directory Entry
Datablocks
File System Basics
Directory Entry
2
Inode
Directory Entry
1
Inode
Directory Entry
Atomic Actions Ordering
• Imagine the system crashing while making
changes to the file system.
• How should the atomic actions be ordered
such that the file system can be recovered?
Atomic Actions Ordering
Directory Entry
a
Inode
rename a b
Atomic Actions Ordering
Directory Entry
a
Inode
rename a b
Lost inode if system crashes here.
Atomic Actions Ordering
Directory Entry
a
Inode
rename a b
Atomic Actions Ordering
Directory Entry
Inode
a
b
rename a b
Atomic Actions Ordering
Directory Entry
Inode
a
b
rename a b
Atomic Actions Ordering
• From “Metadata Update Performance in
File Systems” by G. Ganger, Y. Patt
• Operations
–
–
–
–
Link removal
Link addition
Block allocation
Block de-allocation
Link Addition
• 1. Link count in inode incremented.
• 2. Pointer to inode added to the list of
directory entries.
Link Count
DirEntry
1
Inode
Link Addition
• 1. Link count in inode incremented.
• 2. Pointer to inode added to the list of
directory entries.
Link Count
DirEntry
2
Inode
Link Addition
• 1. Link count in inode incremented.
• 2. Pointer to inode added to the list of
directory entries.
Link Count
DirEntry
2
Inode
DirEntry
Link Deletion
• 1. Directory Entry is removed first.
• 2. Link Count is decremented.
Link Count
DirEntry
2
Inode
DirEntry
Link Deletion
• 1. Directory Entry is removed first.
• 2. Link Count is decremented.
Link Count
DirEntry
2
Inode
Link Deletion
• 1. Directory Entry is removed first.
• 2. Link Count is decremented.
Link Count
DirEntry
1
Inode
The Problem
– Finding preserved invariant was not easy.
• “No lost inodes. All allocated inodes are pointed to
by a directory entry.” is not an invariant.
– Reverse engineering the invariant.
– Tool helped determine which invariants are
wrong.
Discovered Invariants
• “If an inode’s link count is zero, there are
no directory entries pointing to the inode.”
• “At all times, an inode’s link count is higher
than the number of directory entries
pointing to an inode.”
Discovered Invariants
• “If an inode’s link count is zero, there are
no directory entries pointing to the inode.”
– Important when recovering after a crash so that
an inode is not accidently deallocated.
Using the Invariants
• Weakened the precondition of the
operations to see if the invariants are
preserved.
• Some interesting configurations
– Link count much higher than the actual number
of directory entries.
Other Issues
• Relations in Alcoa can be
– A function, surjective, partial/total, injective
• Abstraction design decision
– Choosing relation type forces specification
writer to be careful and specific.
Other Issues
• Alcoa does not have numbers.
– Link Count was tricky to model.
• Inverse relations.
– Alcoa allows this and inadvertently used.
• Many invariants do not hold because of the
intermediate stages.
– Tricky specifying an invariant.
Other Issues
• Must clearly specify the precondition and
postcondition of an operation.
– Hoare Triple
• Instance finding useful for careless errors
such as typos.
– b in UsedB
– b not in UsedB’