Ontology type: schema:ScholarlyArticle Open Access: True
2020-10-23
AUTHORSPetr Ročkai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiříí Barnat
ABSTRACTIn 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... »
PAGES363-382
http://scigraph.springernature.com/pub.10.1007/s10270-020-00837-y
DOIhttp://dx.doi.org/10.1007/s10270-020-00837-y
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1132019834
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
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