  In this paper, we describe DiOS, a lightweight model operating system which
can be used to execute programs that make use of POSIX APIs. Such executions
are fully reproducible: running the same program with the same inputs twice
will result in two exactly identical instruction traces, even if the program
uses threads for parallelism.
  DiOS is implemented almost entirely in portable C and C++: although its
primary platform is DiVM, a verification-oriented virtual machine, it can be
configured to also run in KLEE, a symbolic executor. Finally, it can be
compiled into machine code to serve as a user-mode kernel.
  Additionally, DiOS is modular and extensible. Its various components can be
combined to match both the capabilities of the underlying platform and to
provide services required by a particular program. New components can be added
to cover additional system calls or APIs.
  The experimental evaluation has two parts. DiOS is first evaluated as a
component of a program verification platform based on DiVM. In the second part,
we consider its portability and modularity by combining it with the symbolic
executor KLEE.
