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

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Rompf, Tiark Sujeeth, Arvind K. Brown, Kevin J. Lee, HyoukJoong Chafi, Hassan Olukotun, Kunle EPFL Zurich Switzerland Stanford Univ Stanford CA 94305 USA

ISBN: (纸本)9781450327848

Just-in-time (JIT) compilation of running programs provides more optimization opportunities than offline compilation. Modern JIT compilers, such as those in virtual machines like Oracle's HotSpot for Java or Google's V8 for JavaScript, rely on dynamic profiling as their key mechanism to guide optimizations. While these JIT compilers offer good average performance, their behavior is a black box and the achieved performance is highly unpredictable. In this paper, we propose to turn JIT compilation into a precision tool by adding two essential and generic metaprogramming facilities: First, allow programs to invoke JIT compilation explicitly. This enables controlled specialization of arbitrary code at run-time, in the style of partial evaluation. It also enables the JIT compiler to report warnings and errors to the program when it is unable to compile a code path in the demanded way. Second, allow the JIT compiler to call back into the program to perform compile-time computation. This lets the program itself define the translation strategy for certain constructs on the fly and gives rise to a powerful JIT macro facility that enables "smart" libraries to supply domain-specific compiler optimizations or safety checks. We present Lancet, a JIT compiler framework for Java bytecode that enables such a tight, two-way integration with the running program. Lancet itself was derived from a high-level Java bytecode interpreter: staging the interpreter using LMS (Lightweight Modular Staging) produced a simple bytecode compiler. Adding abstract interpretation turned the simple compiler into an optimizing compiler. This fact provides compelling evidence for the scalability of the staged-interpreter approach to compiler construction. In the case of Lancet, JIT macros also provide a natural interface to existing LMS-based toolchains such as the Delite parallelism and DSL framework, which can now serve as accelerator macros for arbitrary JVM bytecode.

关键词： design languages Performance JIT Compilation Staging Program Generation

来源：评论

学校读者我要写书评

暂无评论

A design and Verification Methodology for Secure Isolated Regions 16

A Design and Verification Methodology for Secure Isolated Re...

引用

37th acm sigplan conference on programming language design and implementation

作者： Sinha, Rohit Costa, Manuel Lal, Akash Lopes, Nuno P. Rajamani, Sriram Seshia, Sanjit A. Vaswani, Kapil Univ Calif Berkeley Berkeley CA 94720 USA Microsoft Res London England Microsoft Res Bengaluru Karnataka India

ISBN: (纸本)9781450342612

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running on a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime library that implements the interface. The runtime library includes core services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present/CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

关键词： Enclave Programs Secure Computation Confidentiality Formal Verification

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Scalable lock-free dynamic memory allocation

Scalable lock-free dynamic memory allocation

引用

Proceedings of the 2004 acm sigplan conference on programming language design and implementation (pldi'04)

作者： Michael, Maged M. IBM Thomas J. Watson Research Center P.O. Box 218 Yorktown Heights NY 10598 United States

Dynamic memory allocators (malloc/free) rely on mutual exclusion locks for protecting the consistency of their shared data structures under multithreading. The use of locking has many disadvantages with respect to performance, availability, robustness, and programming flexibility. A lock-free memory allocator guarantees progress regardless of whether some threads are delayed or even killed and regardless of scheduling policies. This paper presents a completely lock-free memory allocator. It uses only widely-available operating system support and hardware atomic instructions. It offers guaranteed availability even under arbitrary thread termination and crash-failure, and it is immune to dead-lock regardless of scheduling policies, and hence it can be used even in interrupt handlers and real-time applications without requiring special scheduler support. Also, by leveraging some high-level structures from Hoard, our allocator is highly scalable, limits space blowup to a constant factor, and is capable of avoiding false sharing. In addition, our allocator allows finer concurrency and much lower latency than Hoard. We use PowerPC shared memory multiprocessor systems to compare the performance of our allocator with the default AIX 5.1 libc malloc, and two widely-used multithread allocators, Hoard and Ptmalloc. Our allocator outperforms the other allocators in virtually all cases and often by substantial margins, under various levels of parallelism and allocation patterns. Furthermore, our allocator also offers the lowest contention-free latency among the allocators by significant margins.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Array operators using multiple dispatch a design methodology for array implementations in dynamic languages 1

Array operators using multiple dispatch a design methodology...

引用

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

作者： Bezanson, Jeff Chen, Jiahao Karpinski, Stefan Shah, Viral Edelman, Alan MIT Computer Science and Artificial Intelligence Laboratory United States

ISBN: (纸本)9781450329378

Arrays are such a rich and fundamental data type that they tend to be built into a language, either in the compiler or in a large lowlevel library. Defining this functionality at the user level instead provides greater flexibility for application domains not envisioned by the language designer. Only a few languages, such as C++ and Haskell, provide the necessary power to define n-dimensional arrays, but these systems rely on compile-time abstraction, sacrificing some flexibility. In contrast, dynamic languages make it straightforward for the user to define any behavior they might want, but at the possible expense of performance. As part of the Julia language project, we have developed an approach that yields a novel trade-off between flexibility and compiletime analysis. The core abstraction we use is multiple dispatch. We have come to believe that while multiple dispatch has not been especially popular in most kinds of programming, technical computing is its killer application. By expressing key functions such as array indexing using multi-method signatures, a surprising range of behaviors can be obtained, in a way that is both relatively easy to write and amenable to compiler analysis. The compact factoring of concerns provided by these methods makes it easier for userdefined types to behave consistently with types in the standard library.. Copyright © 2014 acm 978-1-4503-2937-8/14/06. 15.00.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Chimera: Hybrid Program Analysis for Determinism 12

Chimera: Hybrid Program Analysis for Determinism

引用

33rd acm sigplan conference on programming language design and implementation

作者： Lee, Dongyoon Chen, Peter M. Flinn, Jason Narayanasamy, Satish Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9781450312059

Chimera(1) uses a new hybrid program analysis to provide deterministic replay for commodity multiprocessor systems. Chimera leverages the insight that it is easy to provide deterministic multiprocessor replay for data-race-free programs (one can just record non-deterministic inputs and the order of synchronization operations), so if we can somehow transform an arbitrary program to be data-race-free, then we can provide deterministic replay cheaply for that program. To perform this transformation, Chimera uses a sound static data-race detector to find all potential data-races. It then instruments pairs of potentially racing instructions with a weak-lock, which provides sufficient guarantees to allow deterministic replay but does not guarantee mutual exclusion. Unsurprisingly, a large fraction of data-races found by the static tool are false data-races, and instrumenting them each of them with a weak-lock results in prohibitively high overhead. Chimera drastically reduces this cost from 53x to 1.39x by increasing the granularity of weak-locks without significantly compromising on parallelism. This is achieved by employing a combination of profiling and symbolic analysis techniques that target the sources of imprecision in the static data-race detector. We find that performance overhead for deterministic recording is 2.4% on average for Apache and desktop applications and about 86% for scientific applications.

关键词： design Performance Reliability Determinism Replay Data-race detection Static analysis Profiling Symbolic range analysis

来源：评论

学校读者我要写书评

暂无评论

A Compiler Framework for Extracting Superword Level Parallelism 12

A Compiler Framework for Extracting Superword Level Parallel...

引用

33rd acm sigplan conference on programming language design and implementation

作者： Liu, Jun Zhang, Yuanrui Jang, Ohyoung Ding, Wei Kandemir, Mahmut Penn State Univ University Pk PA 16802 USA

ISBN: (纸本)9781450312059

SIMD (single-instruction multiple-data) instruction set extensions are quite common today in both high performance and embedded microprocessors, and enable the exploitation of a specific type of data parallelism called SLP (Superword Level Parallelism). While prior research shows that significant performance savings are possible when SLP is exploited, placing SIMD instructions in an application code manually can be very difficult and error prone. In this paper, we propose a novel automated compiler framework for improving superword level parallelism exploitation. The key part of our framework consists of two stages: superword statement generation and data layout optimization. The first stage is our main contribution and has two phases, statement grouping and statement scheduling, of which the primary goals are to increase SIMD parallelism and, more importantly, capture more superword reuses among the superword statements through global data access and reuse pattern analysis. Further, as a complementary optimization, our data layout optimization organizes data in memory space such that the price of memory operations for SLP is minimized. The results from our compiler implementation and tests on two systems indicate performance improvements as high as 15.2% over a state-of-the-art SLP optimization algorithm.

关键词： design Algorithms languages Experimentation Performance SLP SIMD Scheduling Data Layout Compiler

来源：评论

学校读者我要写书评

暂无评论

Simple and efficient BURS table generation

Simple and efficient BURS table generation

引用

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

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

ISBN: (纸本)0897914759

A simple and efficient algorithm for generating bottom-up rewrite system (BURS) tables is described. A small prototype implementation produces tables 10 to 30 times more quickly than the best current techniques. The algorithm does not require novel data structures or complicated algorithmic techniques. Previously published methods for on-the-fly elimination of states are generalized and simplified to create a new method, triangle trimming, that is employed in the algorithm.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Sound and Precise Analysis of Parallel Programs through Schedule Specialization 12

Sound and Precise Analysis of Parallel Programs through Sche...

引用

33rd acm sigplan conference on programming language design and implementation

作者： Wu, Jingyue Tang, Yang Hu, Gang Cui, Heming Yang, Junfeng Columbia Univ New York NY 10027 USA

ISBN: (纸本)9781450312059

Parallel programs are known to be difficult to analyze. A key reason is that they typically have an enormous number of execution inter-leavings, or schedules. Static analysis over all schedules requires over-approximations, resulting in poor precision;dynamic analysis rarely covers more than a tiny fraction of all schedules. We propose an approach called schedule specialization to analyze a parallel program over only a small set of schedules for precision, and then enforce these schedules at runtime for soundness of the static analysis results. We build a schedule specialization framework for C/C++ multithreaded programs that use Pthreads. Our framework avoids the need to modify every analysis to be schedule-aware by specializing a program into a simpler program based on a schedule, so that the resultant program can be analyzed with stock analyses for improved precision. Moreover, our framework provides a precise schedule-aware def-use analysis on memory locations, enabling us to build three highly precise analyses: an alias analyzer, a data-race detector, and a path slicer. Evaluation on 17 programs, including 2 real-world programs and 15 popular benchmarks, shows that analyses using our framework reduced may-aliases by 61.9%, false race reports by 69%, and path slices by 48.7%;and detected 7 unknown bugs in well-checked programs.

关键词： Algorithms design Reliability Verification Specialization parallel programs multithreading control-flow analysis data-flow analysis constraint solving

来源：评论

学校读者我要写书评

暂无评论

An Integrated Proof language for Imperative Programs 09

An Integrated Proof Language for Imperative Programs

引用

acm sigplan conference on programming language design and implementation

作者： Zee, Karen Kuncak, Viktor Rinard, Martin C. CSAIL MIT Cambridge MA USA Ecole Polytech Fed Lausanne IC Lausanne VD Switzerland

ISBN: (纸本)9781605583921

We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties;2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition;3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system;and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time. The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems. We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of autom

关键词： Algorithms languages Reliability Verification verification theorem prover proof system

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：