Reproducible execution of POSIX programs with DiOS View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2020-10-23

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

PAGES

363-382

References to SciGraph publications

  • 2019-04-04. Extending DIVINE with Symbolic Verification Using SMT in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2017-09-27. Model Checking of C and C++ with DIVINE 4 in AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS
  • 2010. From Operating-System Correctness to Pervasively Verified Applications in INTEGRATED FORMAL METHODS
  • 2017-09-06. From Model Checking to Runtime Verification and Back in RUNTIME VERIFICATION
  • 2016-04-09. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016) in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10270-020-00837-y

    DOI

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

    DIMENSIONS

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


    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\u00ed", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-030-17502-3_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1113233409", 
              "https://doi.org/10.1007/978-3-030-17502-3_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-67531-2_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1091543387", 
              "https://doi.org/10.1007/978-3-319-67531-2_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-16265-7_9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1023698443", 
              "https://doi.org/10.1007/978-3-642-16265-7_9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-662-49674-9_55", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1016503019", 
              "https://doi.org/10.1007/978-3-662-49674-9_55"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-68167-2_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1091962613", 
              "https://doi.org/10.1007/978-3-319-68167-2_14"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2020-10-23", 
        "datePublishedReg": "2020-10-23", 
        "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. 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.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10270-020-00837-y", 
        "isAccessibleForFree": true, 
        "isFundedItemOf": [
          {
            "id": "sg:grant.8861734", 
            "type": "MonetaryGrant"
          }
        ], 
        "isPartOf": [
          {
            "id": "sg:journal.1136228", 
            "issn": [
              "1619-1366", 
              "1619-1374"
            ], 
            "name": "Software and Systems Modeling", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "20"
          }
        ], 
        "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", 
          "execution", 
          "platform", 
          "same program", 
          "DivM", 
          "particular program", 
          "kernel", 
          "overhead", 
          "parallelism", 
          "portability", 
          "machine", 
          "modularity", 
          "Klee", 
          "executor", 
          "code", 
          "services", 
          "threads", 
          "capability", 
          "input", 
          "program", 
          "traces", 
          "system", 
          "second part", 
          "calls", 
          "components", 
          "use", 
          "part", 
          "evaluation", 
          "DIO", 
          "paper"
        ], 
        "name": "Reproducible execution of POSIX programs with DiOS", 
        "pagination": "363-382", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1132019834"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10270-020-00837-y"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10270-020-00837-y", 
          "https://app.dimensions.ai/details/publication/pub.1132019834"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-08-04T17:09", 
        "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/article/article_848.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10270-020-00837-y"
      }
    ]
     

    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/s10270-020-00837-y'

    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/s10270-020-00837-y'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10270-020-00837-y'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10270-020-00837-y'


     

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

    149 TRIPLES      21 PREDICATES      72 URIs      59 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10270-020-00837-y schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author Nd9983f8c7f904892a0255e83200ae7bd
    4 schema:citation sg:pub.10.1007/978-3-030-17502-3_14
    5 sg:pub.10.1007/978-3-319-67531-2_14
    6 sg:pub.10.1007/978-3-319-68167-2_14
    7 sg:pub.10.1007/978-3-642-16265-7_9
    8 sg:pub.10.1007/978-3-662-49674-9_55
    9 schema:datePublished 2020-10-23
    10 schema:datePublishedReg 2020-10-23
    11 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. 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.
    12 schema:genre article
    13 schema:isAccessibleForFree true
    14 schema:isPartOf N3149d467ee35460baccda78f1898cccd
    15 Ne7b56672b521417fb0869d7e19d89f4c
    16 sg:journal.1136228
    17 schema:keywords APIs
    18 DIO
    19 DivM
    20 Klee
    21 calls
    22 capability
    23 code
    24 components
    25 evaluation
    26 execution
    27 executor
    28 experimental evaluation
    29 input
    30 instruction traces
    31 kernel
    32 machine
    33 machine code
    34 modularity
    35 operating system
    36 overhead
    37 paper
    38 parallelism
    39 part
    40 particular program
    41 platform
    42 portability
    43 primary platform
    44 program
    45 reproducible execution
    46 same input
    47 same program
    48 second part
    49 services
    50 such executions
    51 symbolic executor
    52 symbolic executor Klee
    53 system
    54 system calls
    55 threads
    56 traces
    57 use
    58 verification platform
    59 virtual machines
    60 schema:name Reproducible execution of POSIX programs with DiOS
    61 schema:pagination 363-382
    62 schema:productId N47b813f2881142ecaa98e62641ac86dc
    63 Nba85d67ec4d84a33a05be4ba87a4083e
    64 schema:sameAs https://app.dimensions.ai/details/publication/pub.1132019834
    65 https://doi.org/10.1007/s10270-020-00837-y
    66 schema:sdDatePublished 2022-08-04T17:09
    67 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    68 schema:sdPublisher N4cfbe79b1f4849ac86180e9da010bb73
    69 schema:url https://doi.org/10.1007/s10270-020-00837-y
    70 sgo:license sg:explorer/license/
    71 sgo:sdDataset articles
    72 rdf:type schema:ScholarlyArticle
    73 N3149d467ee35460baccda78f1898cccd schema:issueNumber 2
    74 rdf:type schema:PublicationIssue
    75 N3bf5ad92133e4933a182d98c1a0e08b3 rdf:first sg:person.015764046444.46
    76 rdf:rest Ne44b82211eba43c6bfef7297b09343dd
    77 N47b813f2881142ecaa98e62641ac86dc schema:name dimensions_id
    78 schema:value pub.1132019834
    79 rdf:type schema:PropertyValue
    80 N4cfbe79b1f4849ac86180e9da010bb73 schema:name Springer Nature - SN SciGraph project
    81 rdf:type schema:Organization
    82 N67c2a1f5defc45509e0bfbd267e88a9d rdf:first Nda465d3b00164d8fa71698fc554c1689
    83 rdf:rest rdf:nil
    84 Nba85d67ec4d84a33a05be4ba87a4083e schema:name doi
    85 schema:value 10.1007/s10270-020-00837-y
    86 rdf:type schema:PropertyValue
    87 Nc155c9f66ade4ce0b7d1d7210360c680 rdf:first sg:person.07560316405.30
    88 rdf:rest N67c2a1f5defc45509e0bfbd267e88a9d
    89 Nd9983f8c7f904892a0255e83200ae7bd rdf:first sg:person.07377571657.86
    90 rdf:rest N3bf5ad92133e4933a182d98c1a0e08b3
    91 Nda465d3b00164d8fa71698fc554c1689 schema:affiliation grid-institutes:grid.10267.32
    92 schema:familyName Barnat
    93 schema:givenName Jiříí
    94 rdf:type schema:Person
    95 Ne44b82211eba43c6bfef7297b09343dd rdf:first sg:person.011477066543.53
    96 rdf:rest Nc155c9f66ade4ce0b7d1d7210360c680
    97 Ne7b56672b521417fb0869d7e19d89f4c schema:volumeNumber 20
    98 rdf:type schema:PublicationVolume
    99 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    100 schema:name Information and Computing Sciences
    101 rdf:type schema:DefinedTerm
    102 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    103 schema:name Computer Software
    104 rdf:type schema:DefinedTerm
    105 sg:grant.8861734 http://pending.schema.org/fundedItem sg:pub.10.1007/s10270-020-00837-y
    106 rdf:type schema:MonetaryGrant
    107 sg:journal.1136228 schema:issn 1619-1366
    108 1619-1374
    109 schema:name Software and Systems Modeling
    110 schema:publisher Springer Nature
    111 rdf:type schema:Periodical
    112 sg:person.011477066543.53 schema:affiliation grid-institutes:grid.10267.32
    113 schema:familyName Mrázek
    114 schema:givenName Jan
    115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477066543.53
    116 rdf:type schema:Person
    117 sg:person.015764046444.46 schema:affiliation grid-institutes:grid.10267.32
    118 schema:familyName Baranová
    119 schema:givenName Zuzana
    120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015764046444.46
    121 rdf:type schema:Person
    122 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
    123 schema:familyName Ročkai
    124 schema:givenName Petr
    125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
    126 rdf:type schema:Person
    127 sg:person.07560316405.30 schema:affiliation grid-institutes:grid.10267.32
    128 schema:familyName Kejstová
    129 schema:givenName Katarína
    130 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30
    131 rdf:type schema:Person
    132 sg:pub.10.1007/978-3-030-17502-3_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1113233409
    133 https://doi.org/10.1007/978-3-030-17502-3_14
    134 rdf:type schema:CreativeWork
    135 sg:pub.10.1007/978-3-319-67531-2_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1091543387
    136 https://doi.org/10.1007/978-3-319-67531-2_14
    137 rdf:type schema:CreativeWork
    138 sg:pub.10.1007/978-3-319-68167-2_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1091962613
    139 https://doi.org/10.1007/978-3-319-68167-2_14
    140 rdf:type schema:CreativeWork
    141 sg:pub.10.1007/978-3-642-16265-7_9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023698443
    142 https://doi.org/10.1007/978-3-642-16265-7_9
    143 rdf:type schema:CreativeWork
    144 sg:pub.10.1007/978-3-662-49674-9_55 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016503019
    145 https://doi.org/10.1007/978-3-662-49674-9_55
    146 rdf:type schema:CreativeWork
    147 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
    148 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
    149 rdf:type schema:Organization
     




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


    ...