Publikation: DimSum : A Decentralized Approach to Multi-language Semantics and Verification
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
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)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
SAMMLER, 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/3571220BibTex
@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>