Reproducible execution of POSIX programs with DiOS

J 2021

Reproducible execution of POSIX programs with DiOS

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

Základní údaje

Originální název

Reproducible execution of POSIX programs with DiOS

Autoři

ROČKAI, Petr (703 Slovensko, domácí), Zuzana BARANOVÁ (703 Slovensko, domácí), Jan MRÁZEK (203 Česká republika, domácí), Katarína KEJSTOVÁ (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Software & Systems Modeling, Springer, 2021, 1619-1366

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 2.211

Kód RIV

RIV/00216224:14330/21:00118773

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1007/s10270-020-00837-y

UT WoS

000582103200001

Klíčová slova anglicky

model checking; posix; operating system; llvm; verification; model

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2022 09:50, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Citovat

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. Software & Systems Modeling. Springer, 2021, roč. 20, č. 2, s. 363-382. ISSN 1619-1366. Dostupné z: https://dx.doi.org/10.1007/s10270-020-00837-y.

@article{1688018,
   author = {Ročkai, Petr and Baranová, Zuzana and Mrázek, Jan and Kejstová, Katarína and Barnat, Jiří},
   article_number = {2},
   doi = {http://dx.doi.org/10.1007/s10270-020-00837-y},
   keywords = {model checking; posix; operating system; llvm; verification; model},
   language = {eng},
   issn = {1619-1366},
   journal = {Software & Systems Modeling},
   title = {Reproducible execution of POSIX programs with DiOS},
   url = {https://divine.fi.muni.cz/2020/dios/},
   volume = {20},
   year = {2021}
}

TY  - JOUR
ID  - 1688018
AU  - Ročkai, Petr - Baranová, Zuzana - Mrázek, Jan - Kejstová, Katarína - Barnat, Jiří
PY  - 2021
TI  - Reproducible execution of POSIX programs with DiOS
JF  - Software & Systems Modeling
VL  - 20
IS  - 2
SP  - 363-382
EP  - 363-382
PB  - Springer
SN  - 16191366
KW  - model checking
KW  - posix
KW  - operating system
KW  - llvm
KW  - verification
KW  - model
UR  - https://divine.fi.muni.cz/2020/dios/
N2  - 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.
ER  -

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. \textit{Software \&{} Systems Modeling}. Springer, 2021, roč.~20, č.~2, s.~363-382. ISSN~1619-1366. Dostupné z: https://dx.doi.org/10.1007/s10270-020-00837-y.

Podrobný výpis o publikaci