nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Reproducible Execution of POSIX Programs with DiOS

verfasst von : Petr Ročkai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiří Barnat

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Efficient Formal Verification for the Linux Kernel

Nächstes Kapitel Using Relational Verification for Program Slicing

https://divine.fi.muni.cz/2019/dios/.

If execution A creates a file and leaves it around, execution B might get derailed when it tries to create the same file, or might detect its presence and behave differently.

The main exception is KLEE, where the execution stack is completely inaccessible to the program under test and only the virtual machine can access the information stored in it. See also Sect. 3.2.

A version of KLEE with fixes for those problems is available online, along with other supplementary material, from https://divine.fi.muni.cz/2019/dios/.

The details of how this is done are discussed in the online supplementary material at https://divine.fi.muni.cz/2019/dios/.

In DIVINE [1], a model checker based on DiVM, interrupt points are dynamically enabled when the executing thread performs a visible action. Thread identification is supplied by the scheduler in DiOS using a platform-specific (hypercall) interface.

For instance, on contemporary x86-64 processors, this interface is available via the syscall and sysret instructions.

The list of system calls is only fixed relative to the host operating system. To allow the system call proxy component to function properly, the list needs to match what is available on the host. For instance, creat, uname or fdatasync are system calls on Linux but standard libc functions on OpenBSD.

This extraction is performed at DiOS build time, using hostabi.pl, which is part of the DiOS source distribution. The technical details are discussed in the online supplementary material.

All test programs are available online at http://divine.fi.muni.cz/2019/dios/, including scripts to reproduce the results reported in this and in the following sections.

Baranová, Z., et al.: Model checking of C and C++ with DIVINE 4. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201–207. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_14CrossRef

Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_55CrossRef

Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX Association (2008)

Chirigati, F., Shasha, D., Freire, J.: Reprozip: using provenance to support computational reproducibility. In: Proceedings of the 5th USENIX Workshop on the Theory and Practice of Provenance, TaPP 2013, Berkeley, CA, USA, pp. 1:1–1:4. USENIX Association (2013). http://dl.acm.org/citation.cfm?id=2482949.2482951

Frew, J., Metzger, D., Slaughter, P.: Automatic capture and reconstruction of computational provenance. Concurr. Comput. Pract. Exper. 20(5), 485–496 (2008). https://doi.org/10.1002/cpe.v20:5. ISSN 1532–0626CrossRef

Inverso, O., Nguyen, T.L., Fischer, B., Torre, S.L., Parlato, G.: Lazy-CSeq: a context-bounded model checking tool for multi-threaded C-programs. In: 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 807–812 (2015). https://doi.org/10.1109/ASE.2015.108

Joshi, S., Orso, A.: Scarpe: a technique and tool for selective capture and replay of program executions. In: 2007 IEEE International Conference on Software Maintenance, pp. 234–243 (2007). https://doi.org/10.1109/ICSM.2007.4362636. ISBN 978-1-4244-1256-3

Kejstová, K.: Model checking with system call traces. Master’s thesis, Masarykova univerzita, Fakulta informatiky, Brno (2019). http://is.muni.cz/th/tukvk/

Kejstová, K., Ročkai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 225–240. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_14CrossRef

10.

Kong, S., Tillmann, N., de Halleux, J.: Automated testing of environment-dependent programs-a case study of modeling the file system for Pex. In: 2009 Sixth International Conference on Information Technology: New Generations, pp. 758–762. IEEE (2009). https://doi.org/10.1109/ITNG.2009.80

11.

Krekel, H., Oliveira, B., Pfannschmidt, R., Bruynooghe, F., Laugher, B., Bruhin, F.:. Pytest 4.5 (2004). https://github.com/pytest-dev/pytest

12.

Lauko, H., Štill, V., Ročkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 204–208. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_14. ISBN 978-3-030-17502-3CrossRef

13.

Leungwattanakit, W., Artho, C., Hagiya, M., Tanabe, Y., Yamamoto, M., Takahashi, K.: Modular software model checking for distributed systems. IEEE Trans. Softw. Eng. 40(5), 483–501 (2014). https://doi.org/10.1109/TSE.2013.49CrossRef

14.

Mackinnon, T., Freeman, S., Craig, P.: Extreme Programming Examined. Chapter Endo-testing: Unit Testing with Mock Objects, pp. 287–301. Addison-Wesley Longman Publishing Co. Inc., Boston (2001). http://dl.acm.org/citation.cfm?id=377517.377534. ISBN 0-201-71040-4

15.

Mostafa, S., Wang, X.: An empirical study on the usage of mocking frameworks in software testing. In: 2014 14th International Conference on Quality Software, pp. 127–132 (2014). https://doi.org/10.1109/QSIC.2014.19

16.

Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Symposium on Operating Systems Design and Implementation, USENIX (2008)

17.

Ročkai, P., Štill, V., Černá, I., Barnat, J.: DiVM: model checking with LLVM and graph memory. J. Syst. Softw. 143, 1–13 (2018). https://doi.org/10.1016/j.jss.2018.04.026. ISSN 0164–1212CrossRef

18.

Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: Formal Methods in Computer-Aided Design, pp. 210–217. IEEE (2013). https://doi.org/10.1109/FMCAD.2013.6679412

19.

Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded c programs. Technical report (2008)

20.

Štill, V., Ročkai, P., Barnat, J.: Using off-the-shelf exception support components in C++ verification. In: Software Quality, Reliability and Security (QRS), pp. 54–64 (2017)

Titel: Reproducible Execution of POSIX Programs with DiOS
verfasst von: Petr Ročkai
Zuzana Baranová
Jan Mrázek
Katarína Kejstová
Jiří Barnat
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-30445-4

Electronic ISBN: 978-3-030-30446-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30446-1_18

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner