Reproducible execution of POSIX programs with DiOS

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ and Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. Software & Systems Modeling. Springer, 2021, vol. 20, No 2, p. 363-382. ISSN 1619-1366. Available from: https://dx.doi.org/10.1007/s10270-020-00837-y.

Basic information

• Original name: Reproducible execution of POSIX programs with DiOS
• Authors: ROČKAI, Petr (703 Slovakia, belonging to the institution), Zuzana BARANOVÁ (703 Slovakia, belonging to the institution), Jan MRÁZEK (203 Czech Republic, belonging to the institution), Katarína KEJSTOVÁ (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution).
• Edition: Software & Systems Modeling, Springer, 2021, 1619-1366.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• Impact factor: Impact factor: 2.211
• RIV identification code: RIV/00216224:14330/21:00118773
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.1007/s10270-020-00837-y
• UT WoS: 000582103200001
• Keywords in English: model checking; posix; operating system; llvm; verification; model
• Tags: International impact, Reviewed

Abstract

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.

Links

• GA18-02177S, research and development project: Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation