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

41st acm sigplan conference on programming language design and implementation, pldi 2020

作者： Porter, Chris Mururu, Girish Barua, Prithayan Pande, Santosh Georgia Institute of Technology United States

ISBN: (纸本)9781450376136

Modern software systems make extensive use of libraries derived from C and C++. Because of the lack of memory safety in these languages, however, the libraries may suffer from vulnerabilities, which can expose the applications to potential attacks. For example, a very large number of return-oriented programming gadgets exist in glibc that allow stitching together semantically valid but malicious Turing-complete and -incomplete programs. While CVEs get discovered and often patched and remedied, such gadgets serve as building blocks of future undiscovered attacks, opening an ever-growing set of possibilities for generating malicious programs. Thus, significant reduction in the quantity and expressiveness (utility) of such gadgets for libraries is an important problem. In this work, we propose a new approach for handling an application's library functions that focuses on the principle of "getting only what you want." This is a significant departure from the current approaches that focus on "cutting what is unwanted." Our approach focuses on activating/deactivating library functions on demand in order to reduce the dynamically linked code surface, so that the possibilities of constructing malicious programs diminishes substantially. The key idea is to load only the set of library functions that will be used at each library call site within the application at runtime. This approach of demand-driven loading relies on an input-aware oracle that predicts a near-exact set of library functions needed at a given call site during the execution. The predicted functions are loaded just in time and unloaded on return. We present a decision-tree based predictor, which acts as an oracle, and an optimized runtime system, which works directly with library binaries like GNU libc and libstdc++. We show that on average, the proposed scheme cuts the exposed code surface of libraries by 97.2%, reduces ROP gadgets present in linked libraries by 97.9%, achieves a prediction accuracy in most

关键词： C++ (programming language)

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

NOVA: A functional language for data parallelism 1

NOVA: A functional language for data parallelism

引用

1st acm sigplan International Workshop on Libraries, languages and Compilers for Array programming, ARRAY 2014 - Part of pldi 2014

作者： Collins, Alexander Grewe, Dominik Grover, Vinod Lee, Sean Susnea, Adriana University of Edinburgh United Kingdom NVIDIA Corporation United Kingdom

ISBN: (纸本)9781450329378

Functional languages provide a solid foundation on which complex optimization passes can be designed to exploit parallelism available in the underlying system. Their mathematical foundations enable high-level optimizations that would be impossible in traditional imperative languages. This makes them uniquely suited for generation of efficient target code for parallel systems, such as multiple Central Processing Units (CPUs) or highly data-parallel Graphics Processing Units (GPUs). Such systems are becoming the mainstream for scientific and commodity desktop computing. Writing performance portable code for such systems using lowlevel languages requires significant effort from a human expert. This paper presents NOVA, a functional language and compiler for multi-core CPUs and GPUs. The NOVA language is a polymorphic, statically-typed functional language with a suite of higher-order functions which are used to express parallelism. These include map, reduce and scan. The NOVA compiler is a light-weight, yet powerful, optimizing compiler. It generates code for a variety of target platforms that achieve performance comparable to competing languages and tools, including hand-optimized code. The NOVA compiler is stand-Alone and can be easily used as a target for higher-level or domain specific languages or embedded in other applications. We evaluate NOVA against two competing approaches: the Thrust library and hand-written CUDA C. NOVA achieves comparable performance to these approaches across a range of benchmarks. NOVA-generated code also scales linearly with the number of processor cores across all compute-bound benchmarks.. Copyright © 2014 acm 978-1-4503-2937-8/14/06. 15.00.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

Efficient control flow quantification 06

Efficient control flow quantification

引用

21st Annual acm sigplan conference on Object-oriented programming Systems, languages, and Applications, OOPSLA 2006

作者： Bockisch, Christoph Kanthak, Sebastian Haupt, Michael Arnold, Matthew Mezini, Mira Software Technology Group Darmstadt University of Technology Germany Software Architecture Research Group Hasso Plattner Institute for Software Systems Engineering Potsdam Germany IBM T. J.Watson Research Center Yorktown Heights NY United States

ISBN: (纸本)1595933484

Aspect-oriented programming (AOP) is increasingly gaining in popularity. However, the focus of aspect-oriented language research has been mostly on language design issues;efficient implementation techniques have been less popular. As a result, the performance of certain AOP constructs is still poor. This is in particular true for constructs that rely on dynamic properties of the execution (e.g., the cflow construct).In this paper, we present efficient implementation techniques for cflow that exploit direct access to internal structures of the virtual machine running an application, such as the call stack, as well as the integration of these techniques into the just-in-time compiler code generation *** results show that AOP has the potential to make programs that need to define control flow-dependent behavior not only more modular but also more efficient. By making means for control flow-dependent behavior part of the language, AOP opens the possibility of applying sophisticated compiler optimizations that are out of reach for application programmers. Copyright © 2006 acm.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Probabilistic register allocation

Probabilistic register allocation

引用

acm sigplan '92 conference on programming language design and implementation, pldi 1992

作者： Proebsting, Todd A. Fischer, Charles N. Univ of Wisconsin-Madison WI United States

ISBN: (纸本)0897914759

A new global register allocation technique, probabilistic register allocation, is described. Probabilistic register allocation quantifies the costs and benefits of allocating variables to registers over live ranges so that excellent allocation choices can be made. Local allocation is done first, and then global allocation is done iteratively beginning in the the most deeply nested loops. Because local allocation precedes global allocation, probabilistic allocation does not interfere with the use of well-known, high-quality local register allocation and instruction scheduling techniques.

关键词： Computer systems programming

来源：评论

学校读者我要写书评

暂无评论

Compressing Java class files

Proceedings of the ACM SIGPLAN Conference on Programming Lan...

引用

Proceedings of the acm sigplan conference on programming language design and implementation (pldi) 1999年 247-258页

作者： Pugh, William Univ of Maryland College Park MD United States

Java class files are often distributed as jar files, which are collections of individually compressed class files (and possibility other files). Jar files are typically about 1/2 the size of the original class files due to compression. I have developed a wire-code format for collections of Java class files. This format is typically 1/2 to 1/5 of the size of the corresponding compressed jar file (1/4 to 1/10 the size of the original class files).

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

Lazy code motion

Lazy code motion

引用

acm sigplan '92 conference on programming language design and implementation, pldi 1992

作者： Knoop, Jens Ruething, Oliver Steffen, Bernhard Christian-Albrechts-Univ Kiel Germany

ISBN: (纸本)0897914759

We present a bit-vector algorithm for the optimal and economical placement of computations within flow graphs, which is as efficient as standard uni-directional analyses. The point of our algorithm is the decomposition of the bi-directional structure of the known placement algorithms into a sequence of a backward and a forward analysis, which directly implies the efficiency result. Moreover, the new compositional structure opens the algorithm for modification: two further uni-directional analysis components exclude any unnecessary code motion. This laziness of our algorithm minimizes the register pressure, which has drastic effects on the run-time behaviour of the optimized programs in practice, where an economical use of registers is essential.

关键词： Computer 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

来源：评论

学校读者我要写书评

暂无评论

GenSQL: A Probabilistic programming System for Querying Generative Models of Database Tables

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 790-815页

作者： Huot, Mathieu Ghavami, Matin Lew, Alexander K. Schaechtle, Ulrich Freer, Cameron E. Shelby, Zane Rinard, Martin C. Saad, Feras A. Mansinghka, Vikash K. MIT Cambridge MA 02139 USA Digital Garage Tokyo Japan Carnegie Mellon Univ Pittsburgh PA USA

This article presents GenSQL, a probabilistic programming system for querying probabilistic generative models of database tables. By augmenting SQL with only a few key primitives for querying probabilistic models, GenSQL enables complex Bayesian inference workflows to be concisely implemented. GenSQL's query planner rests on a unified programmatic interface for interacting with probabilistic models of tabular data, which makes it possible to use models written in a variety of probabilistic programming languages that are tailored to specific workflows. Probabilistic models may be automatically learned via probabilistic program synthesis, hand-designed, or a combination of both. GenSQL is formalized using a novel type system and denotational semantics, which together enable us to establish proofs that precisely characterize its soundness guarantees. We evaluate our system on two case real-world studies-an anomaly detection in clinical trials and conditional synthetic data generation for a virtual wet lab-and show that GenSQL more accurately captures the complexity of the data as compared to common baselines. We also show that the declarative syntax in GenSQL is more concise and less error-prone as compared to several alternatives. Finally, GenSQL delivers a 1.7-6.8x speedup compared to its closest competitor on a representative benchmark set and runs in comparable time to hand-written code, in part due to its reusable optimizations and code specialization.

关键词： generative modeling Bayesian data science probabilistic query language

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：