Reproducible Execution of POSIX Programs with DiOS View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2019-09-09

AUTHORS

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

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

PAGES

333-349

Book

TITLE

Software Engineering and Formal Methods

ISBN

978-3-030-30445-4
978-3-030-30446-1

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-30446-1_18

DOI

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

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1120927752


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Baranov\u00e1", 
        "givenName": "Zuzana", 
        "id": "sg:person.015764046444.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015764046444.46"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Mr\u00e1zek", 
        "givenName": "Jan", 
        "id": "sg:person.011477066543.53", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477066543.53"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kejstov\u00e1", 
        "givenName": "Katar\u00edna", 
        "id": "sg:person.07560316405.30", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barnat", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011367557177.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2019-09-09", 
    "datePublishedReg": "2019-09-09", 
    "description": "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.", 
    "editor": [
      {
        "familyName": "\u00d6lveczky", 
        "givenName": "Peter Csaba", 
        "type": "Person"
      }, 
      {
        "familyName": "Sala\u00fcn", 
        "givenName": "Gwen", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-30446-1_18", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-30445-4", 
        "978-3-030-30446-1"
      ], 
      "name": "Software Engineering and Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "virtual machines", 
      "operating system", 
      "machine code", 
      "system calls", 
      "symbolic executor", 
      "verification platform", 
      "such executions", 
      "symbolic executor Klee", 
      "reproducible execution", 
      "experimental evaluation", 
      "instruction traces", 
      "primary platform", 
      "APIs", 
      "same input", 
      "platform", 
      "execution", 
      "same program", 
      "DivM", 
      "particular program", 
      "new components", 
      "parallelism", 
      "portability", 
      "machine", 
      "modularity", 
      "Klee", 
      "executor", 
      "code", 
      "services", 
      "kernel", 
      "threads", 
      "capability", 
      "input", 
      "program", 
      "traces", 
      "system", 
      "second part", 
      "calls", 
      "components", 
      "part", 
      "evaluation", 
      "use", 
      "DIO", 
      "paper"
    ], 
    "name": "Reproducible Execution of POSIX Programs with DiOS", 
    "pagination": "333-349", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1120927752"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-30446-1_18"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-30446-1_18", 
      "https://app.dimensions.ai/details/publication/pub.1120927752"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:18", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_284.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-30446-1_18"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-30446-1_18'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-30446-1_18'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-30446-1_18'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-30446-1_18'


 

This table displays all metadata directly associated to this object as RDF triples.

135 TRIPLES      22 PREDICATES      67 URIs      60 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-30446-1_18 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N48a505ffa5994fcb88986201eecb3977
4 schema:datePublished 2019-09-09
5 schema:datePublishedReg 2019-09-09
6 schema:description 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.
7 schema:editor N8078d5377cee48499ad41887203ae2fa
8 schema:genre chapter
9 schema:isAccessibleForFree true
10 schema:isPartOf Nc6fab836ac1a437ea73358a5be9fc069
11 schema:keywords APIs
12 DIO
13 DivM
14 Klee
15 calls
16 capability
17 code
18 components
19 evaluation
20 execution
21 executor
22 experimental evaluation
23 input
24 instruction traces
25 kernel
26 machine
27 machine code
28 modularity
29 new components
30 operating system
31 paper
32 parallelism
33 part
34 particular program
35 platform
36 portability
37 primary platform
38 program
39 reproducible execution
40 same input
41 same program
42 second part
43 services
44 such executions
45 symbolic executor
46 symbolic executor Klee
47 system
48 system calls
49 threads
50 traces
51 use
52 verification platform
53 virtual machines
54 schema:name Reproducible Execution of POSIX Programs with DiOS
55 schema:pagination 333-349
56 schema:productId Ncdd5cb2ae0d64e55bc37f35cdbe00555
57 Nebf3d36b31d141efb7a5cbbab5ee6b43
58 schema:publisher Nc64510d22bdb4849af9478d2fe7c4ced
59 schema:sameAs https://app.dimensions.ai/details/publication/pub.1120927752
60 https://doi.org/10.1007/978-3-030-30446-1_18
61 schema:sdDatePublished 2022-08-04T17:18
62 schema:sdLicense https://scigraph.springernature.com/explorer/license/
63 schema:sdPublisher Nc672061e244a4086a757e0fe0d94365a
64 schema:url https://doi.org/10.1007/978-3-030-30446-1_18
65 sgo:license sg:explorer/license/
66 sgo:sdDataset chapters
67 rdf:type schema:Chapter
68 N0b32d63ac4e24bb680f4519dc14b353a schema:familyName Salaün
69 schema:givenName Gwen
70 rdf:type schema:Person
71 N13b8b42bf5bd4beb81a313fa0c605cdf rdf:first sg:person.011367557177.46
72 rdf:rest rdf:nil
73 N2db774bbf9894456a4b6b7e37721cc7c rdf:first sg:person.011477066543.53
74 rdf:rest Neff4d37ebcd143519ed63652bc82bf1b
75 N48a505ffa5994fcb88986201eecb3977 rdf:first sg:person.07377571657.86
76 rdf:rest Ne7f28a5ad36e46d19126ebbae486a10a
77 N8078d5377cee48499ad41887203ae2fa rdf:first N966c121f63824714b41e98206136afd1
78 rdf:rest Ncf6b4fe13cd04cd2b680f9418c862ab7
79 N966c121f63824714b41e98206136afd1 schema:familyName Ölveczky
80 schema:givenName Peter Csaba
81 rdf:type schema:Person
82 Nc64510d22bdb4849af9478d2fe7c4ced schema:name Springer Nature
83 rdf:type schema:Organisation
84 Nc672061e244a4086a757e0fe0d94365a schema:name Springer Nature - SN SciGraph project
85 rdf:type schema:Organization
86 Nc6fab836ac1a437ea73358a5be9fc069 schema:isbn 978-3-030-30445-4
87 978-3-030-30446-1
88 schema:name Software Engineering and Formal Methods
89 rdf:type schema:Book
90 Ncdd5cb2ae0d64e55bc37f35cdbe00555 schema:name doi
91 schema:value 10.1007/978-3-030-30446-1_18
92 rdf:type schema:PropertyValue
93 Ncf6b4fe13cd04cd2b680f9418c862ab7 rdf:first N0b32d63ac4e24bb680f4519dc14b353a
94 rdf:rest rdf:nil
95 Ne7f28a5ad36e46d19126ebbae486a10a rdf:first sg:person.015764046444.46
96 rdf:rest N2db774bbf9894456a4b6b7e37721cc7c
97 Nebf3d36b31d141efb7a5cbbab5ee6b43 schema:name dimensions_id
98 schema:value pub.1120927752
99 rdf:type schema:PropertyValue
100 Neff4d37ebcd143519ed63652bc82bf1b rdf:first sg:person.07560316405.30
101 rdf:rest N13b8b42bf5bd4beb81a313fa0c605cdf
102 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
103 schema:name Information and Computing Sciences
104 rdf:type schema:DefinedTerm
105 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
106 schema:name Computer Software
107 rdf:type schema:DefinedTerm
108 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
109 schema:familyName Barnat
110 schema:givenName Jiří
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
112 rdf:type schema:Person
113 sg:person.011477066543.53 schema:affiliation grid-institutes:grid.10267.32
114 schema:familyName Mrázek
115 schema:givenName Jan
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477066543.53
117 rdf:type schema:Person
118 sg:person.015764046444.46 schema:affiliation grid-institutes:grid.10267.32
119 schema:familyName Baranová
120 schema:givenName Zuzana
121 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015764046444.46
122 rdf:type schema:Person
123 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
124 schema:familyName Ročkai
125 schema:givenName Petr
126 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
127 rdf:type schema:Person
128 sg:person.07560316405.30 schema:affiliation grid-institutes:grid.10267.32
129 schema:familyName Kejstová
130 schema:givenName Katarína
131 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30
132 rdf:type schema:Person
133 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
134 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
135 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...