Reproducible execution of POSIX programs with DiOS
- PDF / 847,818 Bytes
- 20 Pages / 595.276 x 790.866 pts Page_size
- 92 Downloads / 187 Views
SPECIAL SECTION PAPER
Reproducible execution of POSIX programs with DiOS Petr Roˇckai1
· Zuzana Baranová1 · Jan Mrázek1 · Katarína Kejstová1 · Jiˇríí Barnat1
Received: 1 March 2020 / Revised: 17 July 2020 / Accepted: 5 October 2020 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
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. Keywords Software verification · Operating systems · POSIX · Reproducibility · C/C++
1 Introduction Software verification and validation is a field with a long and varied tradition and includes many methods, processes and techniques. While a certain amount of human involvement in the effort is quite unavoidable, the trend is clearly towards maximal automation. For automation, consistency and reproducibility are clearly essential, but those properties are also of high value in manual efforts. In this paper, we focus on the lower-level aspects of software quality assurance, with emphasis on: – implementation-level pre- and post-conditions, invariants, and assertions, – correctness of memory management (memory safety), – low-level functional requirements (expressed as e.g. unit tests), Communicated by Gwen Salaün and Peter Csaba Ölveczky. This work has been partially supported by the Czech Science Foundation grant No. 18-02177S and by Red Hat, Inc.
B 1
Petr Roˇckai [email protected] Faculty of Informatics, Masaryk University, Brno, Czech Republic
– programming errors in the interaction of programs with the operating system, – medium-level functional requirements: the input–output behaviour of complete programs of moderate complexity. In particular, validation and high-level verification (system testing, integration testing and non-testing-based approaches at a similar level of abstraction) are out of scope. We have designed and implemented a compact model operating system, DiOS, with the aim to improve execution r
Data Loading...
