Reproducible Execution of POSIX Programs with DiOS

D 2019

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, garant, domácí)

Vydání

17th ed. Cham, Software Engineering and Formal Methods, od s. 333-349, 17 s. 2019

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107772

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-30445-4

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-30446-1_18

UT WoS

000716915400016

Klíčová slova anglicky

DIVINE; DiOS; operating system; formal verification; model checking; POSIX; C; C++

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 25. 10. 2021 13:11, RNDr. Jan Mrázek

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. 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.

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ů

MUNI/A/1018/2018, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1108/2020, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Akronym: SV-FI MAV X.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.

Citovat

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible Execution of POSIX Programs with DiOS. In Peter Csaba Ölveczky and Gwen Salaün. Software Engineering and Formal Methods. 17th ed. Cham: Springer International Publishing, 2019, s. 333-349. ISBN 978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1_18.

@inproceedings{1577576,
   author = {Ročkai, Petr and Baranová, Zuzana and Mrázek, Jan and Kejstová, Katarína and Barnat, Jiří},
   address = {Cham},
   booktitle = {Software Engineering and Formal Methods},
   doi = {http://dx.doi.org/10.1007/978-3-030-30446-1_18},
   edition = {17th ed.},
   editor = {Peter Csaba Ölveczky and Gwen Salaün},
   keywords = {DIVINE; DiOS; operating system; formal verification; model checking; POSIX; C; C++},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-30445-4},
   pages = {333-349},
   publisher = {Springer International Publishing},
   title = {Reproducible Execution of POSIX Programs with DiOS},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18},
   year = {2019}
}

TY  - JOUR
ID  - 1577576
AU  - Ročkai, Petr - Baranová, Zuzana - Mrázek, Jan - Kejstová, Katarína - Barnat, Jiří
PY  - 2019
TI  - Reproducible Execution of POSIX Programs with DiOS
PB  - Springer International Publishing
CY  - Cham
SN  - 9783030304454
KW  - DIVINE
KW  - DiOS
KW  - operating system
KW  - formal verification
KW  - model checking
KW  - POSIX
KW  - C
KW  - C++
UR  - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18
L2  - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_18
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. 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.
ER  -

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible Execution of POSIX Programs with DiOS. In Peter Csaba Ölveczky and Gwen Salaün. \textit{Software Engineering and Formal Methods}. 17th ed. Cham: Springer International Publishing, 2019, s.~333-349. ISBN~978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1\_{}18.

Podrobný výpis o publikaci