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

33rd acm sigplan conference on programming language design and implementation

作者： Cartey, Luke Lyngsoe, Rune de Moor, Oege Univ Oxford Oxford OX1 2JD England

ISBN: (纸本)9781450312059

Over the last five years, graphics cards have become a tempting target for scientific computing, thanks to unrivaled peak performance, often producing a runtime speed-up of x10 to x25 over comparable CPU solutions. However, this increase can be difficult to achieve, and doing so often requires a fundamental rethink. This is especially problematic in scientific computing, where experts do not want to learn yet another architecture. In this paper we develop a method for automatically parallelising recursive functions of the sort found in scientific papers. Using a static analysis of the function dependencies we identify sets - partitions - of independent elements, which we use to synthesise an efficient GPU implementation using polyhedral code generation techniques. We then augment our language with DSL extensions to support a wider variety of applications, and demonstrate the effectiveness of this with three case studies, showing significant performance improvement over equivalent CPU methods, and similar efficiency to hand-tuned GPU implementations.

关键词： language Performance gpu scientific applications program synthesis dynamic programming

来源：评论

学校读者我要写书评

暂无评论

Type-preserving Compilation for End-to-end Verification of Security Enforcement

Type-preserving Compilation for End-to-end Verification of S...

引用

acm sigplan conference on programming language design and implementation

作者： Chen, Juan Chugh, Ravi Swamy, Nikhil Microsoft Research United States University of California San Diego United States

ISBN: (纸本)9781450300193

A number of programming languages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. Others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must be further compiled to an executable form. A language suitable for source programming backed by a compiler that enables end-to-end verification is missing. In this paper, we present a type-preserving compiler that translates programs written in FINE, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate language. FINE is type checked using an external SMT solver to reduce the proof burden on source programmers. We extract explicit LCF-style proof terms from the solver and carry these proof terms in the compilation to DCIL, thereby removing the solver from the trusted computing base. Explicit proofs enable DCIL to be used in a number of important scenarios, including the verification of mobile code, proof-carrying authorization, and evidence-based auditing. We report on our experience using FINE to build reference monitors for several applications, ranging from a plugin-based email client to a conference management server.

关键词： Security type systems dependent types bytecode languages functional programming authorization information flow mobile code security compilers

来源：评论

学校读者我要写书评

暂无评论

Dependent types in practical programming

Conference Record of the Annual ACM Symposium on Principles ...

引用

conference Record of the Annual acm Symposium on Principles of programming languages 1999年 214-227页

作者： Xi, Hongwei Pfenning, Frank Oregon Graduate Inst of Science and Technology Beaverton OR United States

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. A major complication resulting from introducing dependent types is that pure type inference for the enriched system is no longer possible, but we show that type-checking a sufficiently annotated program in DML(C) can be reduced to constraint satisfaction in the constraint domain C. We exhibit the unobtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. The main contribution of the paper lies in our language design, including the formulation of type-checking rules which makes the approach practical. To our knowledge, no previous type system for a general purpose programming language such as ML has combined dependent types with features including datatype declarations, higher-order functions, general recursions, let-polymorphism, mutable references, and exceptions. In addition, we have finished a prototype implementation of DML(C) for an integer constraint domain C, where constraints are linear inequalities (Xi and Pfenning 1998).

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

REGISTER ALLOCATION ACROSS PROCEDURE AND MODULE BOUNDARIES 90

引用

1990 CONF OF THE SPECIAL INTEREST GROUP ON programming languageS OF THE ASSOC FOR COMPUTING MACHINERY : programming language design AND implementation

作者： SANTHANAM, V ODNERT, D HEWLETT PACKARD CO CALIF LANGUAGE LABCUPERTINOCA 95014

ISBN: (纸本)9780897913645

This paper describes a method for compiling programs using interprocedural register allocation. A strategy for handling programs built from multiple modules is presented, as well as algorithms for global variable promotion and register spill code motion. These algorithms attempt to address some of the shortcomings of previous interprocedural register allocation strategies. Results are given for an implementation on a single register file RISC-based architecture.

关键词： Reduced instruction set computing

来源：评论

学校读者我要写书评

暂无评论

An automatically generated, realistic compiler for an imperative programming language

An automatically generated, realistic compiler for an impera...

引用

acm sigplan conference on programming language design and implementation, PLDI 1988

作者： Pleban, Uwe F. Lee, Peter Tektronix Laboratories P.O. Box 500 M/S 50-662 BeavertonOR9077 United States Department of Computer Science Carnegie Mellon University PittsburghPA15213 United States

ISBN: (纸本)0897912691

We describe the automatic generation of a complete, realistic compiler from formal specifications of the syntax and semantics of Sol/C, a nontrivial imperative language "sort of like C." The compiler exhibits a three pass structure, is efficient, and produces object programs whose performance characteristics compare favorably with those produced by commercially available compilers. To our knowledge, this is the first time that this has been accomplished. © 1988 acm.

关键词： Sols

来源：评论

学校读者我要写书评

暂无评论

Compiling Stan to Generative Probabilistic languages and Extension to Deep Probabilistic programming 2021

Compiling Stan to Generative Probabilistic Languages and Ext...

引用

42nd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Baudart, Guillaume Burroni, Javier Hirzel, Martin Mandel, Louis Shinnar, Avraham PSL Univ Ecole Normale Super INRIA Paris Paris France UMass Amherst Amherst MA USA IBM Res MIT IBM Watson AI Lab Armonk NY USA

ISBN: (纸本)9781450383912

Stan is a probabilistic programming language that is popular in the statistics community, with a high-level syntax for expressing probabilistic models. Stan differs by nature from generative probabilistic programming languages like Church, Anglican, or Pyro. This paper presents a comprehensive compilation scheme to compile any Stan model to a generative language and proves its correctness. We use our compilation scheme to build two new backends for the Stanc3 compiler targeting Pyro and NumPyro. Experimental results show that the NumPyro backend yields a 2.3x speedup compared to Stan in geometric mean over 26 benchmarks. Building on Pyro we extend Stan with support for explicit variational inference guides and deep probabilistic models. That way, users familiar with Stan get access to new features without having to learn a fundamentally new language.

关键词： Probabilistic programming Semantics Stan Pyro

来源：评论

学校读者我要写书评

暂无评论

The Essence of Bluespec A Core language for Rule-Based Hardware design 2020

The Essence of Bluespec A Core Language for Rule-Based Hardw...

引用

41st acm sigplan conference on programming language design and implementation (PLDI)

作者： Bourgeat, Thomas Pit-Claudel, Clement Chlipala, Adam Arvind MIT CSAIL 77 Massachusetts Ave Cambridge MA 02139 USA

ISBN: (纸本)9781450376136

The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits. Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design. In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies. Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits. We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.

关键词： HDL Semantics Compiler Correctness

来源：评论

学校读者我要写书评

暂无评论

design, implementation and evaluation of the FNC-2 attribute grammar system 90

Design, implementation and evaluation of the FNC-2 attribute...

引用

proceedings of the acm sigplan '90 conference on programming language design and implementation

作者： Jourdan, Martin Parigot, Didier Julie, Catherine Durin, Olivier Le Bellec, Carole INRIA Le Chesnay France

ISBN: (纸本)0897913647

FNC-2 is a new attribute grammar processing system aiming at expressive power, efficiency, ease of use and versatility. Its development at INRIA started in 1986, and a first running prototype is available since early 1989. Its most important features are: efficient exhaustive and incremental visit-sequence-based evaluation of strongly (absolutely) non-circular AGs;extensive space optimizations;a specially-designed AG-description language, with provisions for true modularity;portability and versatility of the generated evaluators;complete environment for application development. This paper briefly describes the design and implementation of FNC-2 and its peripherals. Then preliminary experience with the system is reported.

关键词： Computer Operating Systems

来源：评论

学校读者我要写书评

暂无评论

A single intermediate language that supports multiple implementations of exceptions

A single intermediate language that supports multiple implem...

引用

acm sigplan' 00 conference on programming language design and implementation (PLDI)

作者： Ramsey, N Jones, SP Harvard Univ Cambridge MA 02138 USA

We present mechanisms that enable our compiler-target language, C--, to express four of the best known techniques for implementing exceptions, all within a single, uniform framework. We define the mechanisms precisely, using a formal operational semantics. We also show that exceptions need not require special treatment in the optimizer;by introducing extra dataflow edges, we make standard optimization techniques work even on programs that use exceptions. Our approach clarifies the design space of exception-handling techniques, and it allows a single optimizer to handle a variety of implementation techniques. Our ultimate goal is to allow a source-language compiler the freedom to choose its exception-handling policy, while encapsulating the architecture-dependent mechanisms and their optimization in an implementation of C-- that can be used by compilers for many source languages.

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

Study of dead data members in C++ applications

Study of dead data members in C++ applications

引用

proceedings of the 1998 Annual acm sigplan conference on programming language design and implementation, PLDI

作者： Sweeney, Peter P. Tip, Frank IBM Thomas J. Watson Research Cent Yorktown Heights United States

Object-oriented applications may contain data members that can be removed from the application without affecting program behavior. Such `dead' data members may occur due to unused functionality in class libraries, or due to the programmer losing track of member usage as the application changes over time. We present a simple and efficient algorithm for detecting dead data members in C++ applications. This algorithm has been implemented using a prototype version of the IBM VisualAge C++ compiler, and applied to a number of realistic benchmark programs ranging from 600 to 58,000 lines of code. For the non-trivial benchmarks, we found that up to 27.3% of the data members in the benchmarks are dead (average 12.5%), and that up to 11.6% of the object space of these applications may be occupied by dead data members at run-time (average 4.4%).

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：