Information Technology Reference
In-Depth Information
suitable was available. Since then, efforts have been made to address problems
like ours [16] using general frameworks.
8.1
Vocabulary
The simulation layer executes tasks in all possible inter-leavings. We will describe
tasks in more detail below, as they are used as a thread layer. A task step
defines an atomic action. Simulating DFS-R requires providing a handle into
the atomic actions that a machine may perform, but of equal importance also
provide environment actions, such as file system operations. The actions that
are presented to the simulator are summarized as
L
action
. Finally, we can define
a simulation trace
S
trace
as a sequence
d
of actions. In our experiments we set
d
= 16, with the assumption that most bugs could be exercised with a few
number of operations.
Σ
file
=
{
a, b, c, d
}
vocabulary of files
Σ
dir
=
{
p, q, r
}
directories
Σ
res
=
Σ
file
∪
Σ
dir
resources
L
fs
=
{
share/, noshare/
}
(
Σ
dir
/
)
∗
Σ
res
file paths
Σ
m
=
{
m
1
,m
2
,m
3
,m
4
}
machines
L
action
=
rename
(
Σ
m
,
L
fs
,
L
fs
)
actions
∪
create
(
Σ
m
,
L
fs
)
∪
update
(
Σ
m
,
L
fs
)
∪
delete
(
Σ
m
,
L
fs
)
∪
sync
(
Σ
m
,Σ
m
)
∪
read
−
journal
(
Σ
m
,N
∪{
ω
}
)
d
action
S
trace
=
L
simulation trace
The set of possible file system operations are generated using a finite alphabet
of file and directory names. They may take place on one of the machines listed
in
Σ
m
. The internal actions of DFS-R are split into two sets: (1) reading the
USNjournalfor1,2,3,etc.stepsoruntilreachingafix-point(
ω
steps); (2)
synchronizing symmetrically between two machines. Paths starting with
share
are replicated, paths starting with
noshare
are outside the replicated folder.
8.2
A Custom Memory Layer
Key to supporting ecient backtracking is to be able to save and restore state.
Our simulation does not backtrack over suspensions within stack frames. This
limitation allowed us to concentrate on tracking heap allocated memory only.
In summary, the simulation environment saves aside a copy of the heap when
entering a new backtracking point for the first time. When re-entering the back-
tracking point, it can dispense all memory allocated within the branch and re-
store the previous state. Unfortunately, not all heap-allocated memory can be
reclaimed at backtracking points. In particular, memory that is associated with
device state cannot just be overwritten on backtracking points. For instance,
Search WWH ::
Custom Search