Publikation:

DimSum : A Decentralized Approach to Multi-language Semantics and Verification

Lade...
Vorschaubild

Dateien

Sammler_2-d0xjn46upae76.pdf
Sammler_2-d0xjn46upae76.pdfGröße: 525.45 KBDownloads: 22

Datum

2023

Autor:innen

Sammler, Michael
Spies, Simon
Song, Youngju
Krebbers, Robbert
Garg, Deepak
Dreyer, Derek

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

DOI (zitierfähiger Link)
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

European Union (EU): 101003349

Projekt

Open Access-Veröffentlichung
Open Access Gold
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published

Erschienen in

Proceedings of the ACM on Programming Languages. Association for Computing Machinery (ACM). 2023, 7(POPL), 27. eISSN 2475-1421. Verfügbar unter: doi: 10.1145/3571220

Zusammenfassung

Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions. Concretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators). We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

multi-language semantics, verification, compilers, non-determinism, separation logic, Iris, Coq

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690SAMMLER, Michael, Simon SPIES, Youngju SONG, Emanuele D'OSUALDO, Robbert KREBBERS, Deepak GARG, Derek DREYER, 2023. DimSum : A Decentralized Approach to Multi-language Semantics and Verification. In: Proceedings of the ACM on Programming Languages. Association for Computing Machinery (ACM). 2023, 7(POPL), 27. eISSN 2475-1421. Verfügbar unter: doi: 10.1145/3571220
BibTex
@article{Sammler2023-01-09DimSu-70278,
  year={2023},
  doi={10.1145/3571220},
  title={DimSum : A Decentralized Approach to Multi-language Semantics and Verification},
  number={POPL},
  volume={7},
  journal={Proceedings of the ACM on Programming Languages},
  author={Sammler, Michael and Spies, Simon and Song, Youngju and D'Osualdo, Emanuele and Krebbers, Robbert and Garg, Deepak and Dreyer, Derek},
  note={Article Number: 27}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/70278">
    <dc:contributor>D'Osualdo, Emanuele</dc:contributor>
    <dc:contributor>Garg, Deepak</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-06-28T10:22:03Z</dc:date>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>D'Osualdo, Emanuele</dc:creator>
    <dc:creator>Dreyer, Derek</dc:creator>
    <dc:contributor>Dreyer, Derek</dc:contributor>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/70278/1/Sammler_2-d0xjn46upae76.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2023-01-09</dcterms:issued>
    <dc:creator>Spies, Simon</dc:creator>
    <dcterms:title>DimSum : A Decentralized Approach to Multi-language Semantics and Verification</dcterms:title>
    <dc:contributor>Spies, Simon</dc:contributor>
    <dc:language>eng</dc:language>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-06-28T10:22:03Z</dcterms:available>
    <dc:contributor>Sammler, Michael</dc:contributor>
    <dc:creator>Sammler, Michael</dc:creator>
    <dcterms:abstract>Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions.
Concretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators).
We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.</dcterms:abstract>
    <dc:creator>Garg, Deepak</dc:creator>
    <dc:contributor>Song, Youngju</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/70278/1/Sammler_2-d0xjn46upae76.pdf"/>
    <dc:contributor>Krebbers, Robbert</dc:contributor>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/70278"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Song, Youngju</dc:creator>
    <dc:creator>Krebbers, Robbert</dc:creator>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Unbekannt
Diese Publikation teilen