Information Technology Reference
In-Depth Information
buffers that are allocated by procedures that print to files cannot be reclaimed
using a stack discipline. This led to a dual mode custom memory layer, one for
backtracking mode and one for non-backtracking mode.
8.3
Thread Layering
It is challenging in itself to model check multi-threaded programs faithfully. A
real software model checker would have to allow context switches at arbitrary
control locations. The first problem requires infrastructure; the model checker
will have to save and restore the stack. This amounts to mirroring thread context
switches. A more fundamental problem is the significant increase in the state
space as every program counter is potentially a backtracking point.
We bypassed these issues by implementing a thread abstraction that wrapped
around thread pools and timer queues. Both facilities are supported by operating
system APIs, but require the caller to maintain different context depending on
whether a job is spawned directly in a thread pool or delayed in a timer queue.
Our thread layer combines these two concepts into a single task entity, which
can be set to run immediately, or with a non-zero delay. To support simulation,
tasks support dual modes: one for running in a multi-threaded environment, and
another for running in a single-threaded simulation environment.
8.4
Virtualization
The interfaces to the on-disk database, the file system, and the network layer
had to be abstracted and re-coded for speed and control. The abstractions were
indispensable in making simulation practical. Creation time of a fresh on-disk
JET-blue database takes for instance 2 seconds (it creates several larger files,
including logs). Backtracking over such disk operations would slow down simu-
lation to a crawl.
Using abstractions also came with several limitations. Foremost, bugs inside
the physical modules were not exposed by simulation, as they were simply not
exercised. It was also limited what we found worth to reflect in an abstraction.
The database abstraction did thus not implement the ACID properties. This was
reasonable as all transactions in DFS-R are short lived, but this prevented us
identifying code paths that would lead to conflicting updates. Such errors were
only later exposed during stress runs.
8.5
Partial Order Reduction
The set of simulation traces introduced in Section 8.1 contain a large number of
essentially symmetric traces. For example, the order of creating files share/p/a
and share/p/b on the same machine is insignificant.
More precisely, let π, π ∈L fs be file paths, then we define π
π (read as π is
orthogonal to π ) as a binary relation on paths if neither path is a prefix of the
 
Search WWH ::




Custom Search