Informace o publikaci

Reproducible execution of POSIX programs with DiOS

Autoři

ROČKAI Petr BARANOVÁ Zuzana MRÁZEK Jan KEJSTOVÁ Katarína BARNAT Jiří

Rok publikování 2021
Druh Článek v odborném periodiku
Časopis / Zdroj Software & Systems Modeling
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://divine.fi.muni.cz/2020/dios/
Doi http://dx.doi.org/10.1007/s10270-020-00837-y
Klíčová slova model checking; posix; operating system; llvm; verification; model
Popis 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. Components can be added to cover additional system calls or APIs or removed to reduce overhead. The experimental evaluation has three 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. Finally, we consider its use as a standalone user-mode kernel.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info