检索结果-内蒙古大学图书馆

17th acm sigplan International conference on Software language Engineering (SLE)

作者： Lee, Yunjeong Gopinathan, Kiran Yang, Ziyi Flatt, Matthew Sergey, Ilya Natl Univ Singapore Singapore Singapore Univ Utah Salt Lake City UT USA

ISBN: (纸本)9798400711800

Domain-Specific languages (DSLs) are a popular way to simplify and streamline programmatic solutions of commonly occurring yet specialized tasks. While the design of frameworks for implementing DSLs has been a popular topic of study in the research community, significantly less attention has been given to studying how those frameworks end up being used by practitioners and assessing utility of their features for building DSLs "in the wild". In this paper, we conduct such a study focusing on a particular framework for DSL construction: the Racket programming language. We provide (a) a novel taxonomy of language design intents enabled by Racket-embedded DSLs, and (b) a classification of ways to utilize Racket's mechanisms that make the implementation of those intents possible. We substantiate our taxonomy with an analysis of 30 popular Racket-based DSLs, discussing how they make use of the available mechanisms and accordingly achieve their design intents. The taxonomy serves as a reusable measure that can help language designers to systematically develop, compare, and analyze DSLs in Racket as well as other frameworks.

关键词： domain-specific languages meta-programming

来源：评论

学校读者我要写书评

暂无评论

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification language

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1510-1534页

作者： Parthasarathy, Gaurav Dardinier, Thibault Bonneau, Benjamin Muller, Peter Summers, Alexander J. Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland Univ Grenoble Alpes CNRS Grenoble INP VERIMAG Grenoble France Univ British Columbia Vancouver BC Canada

Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation, not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.

关键词： Software Verification Intermediate Verification languages Formal Semantics Proof Certification

来源：评论

学校读者我要写书评

暂无评论

Modular Hardware design of Pipelined Circuits with Hazards

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 28-51页

作者： Jang, Minseong Rhee, Jungin Lee, Woojin Zhao, Shuangshuang Kang, Jeehoon Korea Adv Inst Sci & Technol Daejeon South Korea

Modular design is critical in reducing hardware designer's cognitive load and development cost. However, it is challenging to modularize high-performance pipelined circuits with structural, data, and control hazards because their resolution-stalling, and bypassing, and discard-and-restarting-introduce cross-stage dependencies. The dependencies could potentially mandate monolithic control logic and create combinational loops, hindering modular design. An effective method to modularize pipelined circuits is valid-ready interfaces, but they apply to a relatively simple form of pipelined circuits only with structural hazards. We propose hazard interfaces, a generalization of valid-ready interfaces that can modularize pipelined circuits not only with structural but also with data and control hazards. The key idea is enveloping the cross-stage dependencies within interfaces. We also design combinators for hazard interfaces in the style of map-reduce that facilitate decomposition of control logic. We implement a compiler (to synthesizable Verilog) for a prototype language supporting hazard interfaces and combinators, and design a sound and efficient type checker that proves the absence of combinational loops. With case studies on 5-stage RISC-V CPU core and 100 Gbps Ethernet NIC, we demonstrate that hazard interfaces indeed facilitate modular design while incurring no noticeable cost in performance, power, and area over reference designs in Chisel and Verilog.

关键词： hardware description language functional programming pipelining hazard combinator

来源：评论

学校读者我要写书评

暂无评论

Allo: A programming Model for Composable Accelerator design

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 593-620页

作者： Chen, Hongzheng Zhang, Niansong Xiang, Shaojie Zeng, Zhichen Dai, Mengjia Zhang, Zhiru Cornell Univ Ithaca NY 14853 USA Univ Sci & Technol China Hefei Peoples R China

Special-purpose hardware accelerators are increasingly pivotal for sustaining performance improvements in emerging applications, especially as the benefits of technology scaling continue to diminish. However, designers currently lack effective tools and methodologies to construct complex, high-performance accelerator architectures in a productive manner. Existing high-level synthesis (HLS) tools often require intrusive source-level changes to attain satisfactory quality of results. Despite the introduction of several new accelerator design languages (ADLs) aiming to enhance or replace HLS, their advantages are more evident in relatively simple applications with a single kernel. Existing ADLs prove less effective for realistic hierarchical designs with multiple kernels, even if the design hierarchy is flattened. In this paper, we introduce Allo, a composable programming model for efficient spatial accelerator design. Allo decouples hardware customizations, including compute, memory, communication, and data type from algorithm specification, and encapsulates them as a set of customization primitives. Allo preserves the hierarchical structure of an input program by combining customizations from different functions in a bottom-up, type-safe manner. This approach facilitates holistic optimizations that span across function boundaries. We conduct comprehensive experiments on commonly-used HLS benchmarks and several realistic deep learning models. Our evaluation shows that Allo can outperform state-of-the-art HLS tools and ADLs on all test cases in the PolyBench. For the GPT2 model, the inference latency of the Allo generated accelerator is 1.7x faster than the NVIDIA A100 GPU with 5.4x higher energy efficiency, demonstrating the capability of Allo to handle large-scale designs.

关键词： Hardware accelerators schedule language accelerator design language compiler optimization

来源：评论

学校读者我要写书评

暂无评论

An Algebraic language for Specifying Quantum Networks

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1313-1335页

作者： Buckley, Anita Chuprikov, Pavel Otoni, Rodrigo Soule, Robert Rand, Robert Eugster, Patrick USI Lugano Lugano Switzerland Yale Univ New Haven CT USA Univ Chicago Chicago IL 60637 USA

Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational semantics. BellKAT's constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.

关键词： Kleene algebra quantum networks entanglement

来源：评论

学校读者我要写书评

暂无评论

PL4XGL: A programming language Approach to Explainable Graph Learning

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 2148-2173页

作者： Jeon, Minseok Park, Jihyeok Oh, Hakjoo Korea Univ Dept Comp Sci & Engn Seoul South Korea

In this article, we present a new, language-based approach to explainable graph learning. Though graph neural networks (GNNs) have shown impressive performance in various graph learning tasks, they have severe limitations in explainability, hindering their use in decision-critical applications. To address these limitations, several GNN explanation techniques have been proposed using a post-hoc explanation approach providing subgraphs as explanations for classification results. Unfortunately, however, they have two fundamental drawbacks in terms of 1) additional explanation costs and 2) the correctness of the explanations. This paper aims to address these problems by developing a new graph-learning method based on programming language techniques. Our key idea is two-fold: 1) designing a graph description language (GDL) to explain the classification results and 2) developing a new GDL-based interpretable classification model instead of GNN-based models. Our graph-learning model, called PL4XGL, consists of a set of candidate GDL programs with labels and quality scores. For a given graph component, it searches the best GDL program describing the component and provides the corresponding label as the classification result and the program as the explanation. In our approach, learning from data is formulated as a program-synthesis problem, and we present top-down and bottom-up algorithms for synthesizing GDL programs from training data. Evaluation using widely-used datasets demonstrates that PL4XGL produces high-quality explanations that outperform those produced by the state-of-the-art GNN explanation technique, SUBGRAPHX. We also show that PL4XGL achieves competitive classification accuracy comparable to popular GNN models.

关键词： Graph Learning Domain-Specific language Program Synthesis

来源：评论

学校读者我要写书评

暂无评论

A pred-LL(*) Parsable Typed Higher-Order Macro System for Architecture Description languages 2023

A pred-LL(*) Parsable Typed Higher-Order Macro System for Ar...

引用

22nd acm sigplan International conference on Generative programming - Concepts and Experiences (GPCE)

作者： Hochrainer, Christoph Krall, Andreas TU Wien Vienna Austria

ISBN: (纸本)9798400704062

Macro systems are powerful language extension tools for Architecture Description languages (ADLs). Their generative power in combination with the simplicity of specification languages allows for a substantial reduction of repetitive specification sections. This paper explores how the introduction of function- and record types in a template-based macro system impacts the specification of ADLs. We present design and implementation of a pattern-based syntax macro system for the Vienna Architecture Description language (VADL). The macro system is directly integrated into the language and is analyzed at parse time using a context-sensitive predLL(*) parser. The usefulness of the macro system is illustrated by some typical macro application design patterns. The effectiveness is shown by a detailed evaluation of the Instruction Set Architecture (ISA) specification of five different processor architectures. The observed specification reduction can be up to 90 times, leading to improved maintainability, readability and runtime performance of the specifications.

关键词： macro system higher-order macros pattern-based generative programming architecture description language

来源：评论

学校读者我要写书评

暂无评论

A Lightweight Polyglot Code Transformation language

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1288-1312页

作者： Ketkar, Ameya Ramos, Daniel Clapp, Lazaro Barik, Raj Ramanathan, Murali Krishna Gitar Inc San Mateo CA 94403 USA Carnegie Mellon Univ Pittsburgh PA 15213 USA Univ Lisbon INESC ID IST Lisbon Portugal Amazon Web Serv Santa Clara CA USA Uber Technol Inc San Francisco CA USA

In today's software industry, large-scale, multi-language codebases are the norm. This brings substantial challenges in developing automated tools for code maintenance tasks such as API migration or dead code cleanup. Tool builders often find themselves caught between two less-than-ideal tooling options: (1) language-specific code rewriting tools or (2) generic, lightweight match-replace transformation tools with limited expressiveness. The former leads to tool fragmentation and a steep learning curve for each language, while the latter forces developers to create ad-hoc, throwaway scripts to handle realistic tasks. To fill this gap, we introduce a new declarative domain-specific language (DSL) for expressing interdependent multi-language code transformations. Our key insight is that we can increase the expressiveness and applicability of lightweight match-replace tools by extending them to support for composition, ordering, and flow. We implemented an open-source tool for our language, called PolyglotPiranha, and deployed it in an industrial setting. We demonstrate its effectiveness through three case studies, where it deleted 210K lines of dead code and migrated 20K lines, across 1611 pull requests. We compare our DSL against state-of-the-art alternatives, and show that the tools we developed are faster, more concise, and easier to maintain.

关键词： Source-code rewriting Automated refactoring Code cleanup

来源：评论

学校读者我要写书评

暂无评论

Verified Extraction from Coq to OCaml

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 52-75页

作者： Forster, Yannick Sozeau, Matthieu Tabareau, Nicolas INRIA Gallinette Project Team Nantes France

One of the central claims of fame of the COQ proof assistant is extraction, i.e., the ability to obtain efficient programs in industrial programming languages such as OCAML, Haskell, or Scheme from programs written in COQ's expressive dependent type theory. Extraction is of great practical usefulness, used crucially e.g., in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are COQ's kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from COQ to OCAML, implemented and verified in COQ itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the METACOQ project, which aims at decreasing the TCB of COQ's kernel by re-implementing it in COQ itself and proving it correct w.r.t. a formal specification of COQ's type theory in COQ. Since OCAML does not have a formal specification, we make use of the MALFUNCTION project specifying the semantics of the intermediate language of the OCAML compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of COQ programs and their extraction. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, and prove that extracted programs of first-order data type are correct

关键词： Coq verified compilation extraction functional programming

来源：评论

学校读者我要写书评

暂无评论

Bringing the WebAssembly Standard up to Speed with SpecTec

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1559-1584页

作者： Youn, Dongjun Shin, Wonho Lee, Jaehyun Ryu, Sukyoung Breitner, Joachim Gardner, Philippa Lindley, Sam Pretnar, Matija Rao, Xiaojia Watt, Conrad Rossberg, Andreas Korea Adv Inst Sci & Technol Daejeon South Korea Imperial Coll London London England Univ Edinburgh Edinburgh Midlothian Scotland Univ Ljubljana Ljubljana Slovenia Univ Cambridge Cambridge England

WebAssembly (Wasm) is a portable low-level bytecode language and virtual machine that has seen increasing use in a variety of ecosystems. Its specification is unusually rigorous - including a full formal semantics for the language - and every new feature must be specified in this formal semantics, in prose, and in the official reference interpreter before it can be standardized. With the growing size of the language, this manual process with its redundancies has become laborious and error-prone, and in this work, we offer a solution. We present SpecTec, a domain-specific language (DSL) and toolchain that facilitates both the Wasm specification and the generation of artifacts necessary to standardize new features. SpecTec serves as a single source of truth - from a SpecTec definition of the Wasm semantics, we can generate a typeset specification, including formal definitions and prose pseudocode descriptions, and a meta-level interpreter. Further backends for test generation and interactive theorem proving are planned. We evaluate SpecTecs ability to represent the latest Wasm 2.0 and show that the generated meta-level interpreter passes 100% of the applicable official test suite. We show that SpecTec is highly effective at discovering and preventing errors by detecting historical errors in the specification that have been corrected and ten errors in five proposals ready for inclusion in the next version of Wasm. Our ultimate aim is that SpecTec should be adopted by the Wasm standards community and used to specify future versions of the standard.

关键词： WebAssembly language specification executable prose DSL

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：