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

Latte: A language, Compiler, and Runtime for Elegant and Efficient Deep Neural Networks

acm sigplan NOTICES 2016年第6期51卷 209-223页

作者： Truong, Leonard Barik, Rajkishore Totoni, Ehsan Liu, Hai Markley, Chick Fox, Armando Shpeisman, Tatiana Univ Calif Berkeley Intel Labs Berkeley CA USA Intel Labs Berkeley CA USA Univ Calif Berkeley Berkeley CA USA

Deep neural networks (DNNs) have undergone a surge in popularity with consistent advances in the state of the art for tasks including image recognition, natural language processing, and speech recognition. The computationally expensive nature of these networks has led to the proliferation of implementations that sacrifice abstraction for high performance. In this paper, we present Latte, a domain-specific language for DNNs that provides a natural abstraction for specifying new layers without sacrificing performance. Users of Latte express DNNs as ensembles of neurons with connections between them. The Latte compiler synthesizes a program based on the user specification, applies a suite of domain-specific and general optimizations, and emits efficient machine code for heterogeneous architectures. Latte also includes a communication runtime for distributed memory data-parallelism. Using networks described using Latte, we demonstrate 3-6x speedup over Caffe (C++/MKL) on the three state-of-the-art ImageNet models executing on an Intel Xeon E5-2699 v3 x86 CPU.

关键词： Deep Learning Neural Networks Domain Specific language Compiler Optimization

来源：评论

学校读者我要写书评

暂无评论

Kindergarten Cop: Dynamic Nursery Resizing for GHC 2016

Kindergarten Cop: Dynamic Nursery Resizing for GHC

引用

25th International conference on Compiler Construction (CC)

作者： Ferreiro, Henrique Castro, Laura Janjic, Vladimir Hammond, Kevin Univ A Coruna Dept Comp Sci La Coruna Spain Univ St Andrews Sch Comp Sci St Andrews KY16 9AJ Fife Scotland

ISBN: (纸本)9781450342414

Generational garbage collectors are among the most popular garbage collectors used in programming language runtime systems. Their performance depends heavily on choosing the appropriate size of the area where new objects are allocated (the nursery). In imperative languages, it is usual to make the nursery as large as possible, within the limits imposed by the heap size. Functional languages, however, have quite different memory behaviour. In this paper, we study the effect that the nursery size has on the performance of lazy functional programs, through the interplay between cache locality and the frequency of collections. We demonstrate that, in contrast with imperative programs, having large nurseries is not always the best solution. Based on these results, we propose two novel algorithms for dynamic nursery resizing that aim to achieve a compromise between good cache locality and the frequency of garbage collections. We present an implementation of these algorithms in the state-of-the-art GHC compiler for the functional language Haskell, and evaluate them using an extensive benchmark suite. In the best case, we demonstrate a reduction in total execution times of up to 88.5%, or an 8.7 overall speedup, compared to using the production GHC garbage collector. On average, our technique gives an improvement of 9.3% in overall performance across a standard suite of 63 benchmarks for the production GHC compiler.

关键词： Generational garbage collection Cache locality Allocation area Functional programming

来源：评论

学校读者我要写书评

暂无评论

language-independent Storage Strategies for Tracing-JIT-based Virtual Machines

引用

acm sigplan NOTICES 2016年第2期51卷 104-113页

作者： Pape, Tobias Felgentreff, Tim Hirschfeld, Robert Gulenko, Anton Bolz, Carl Friedrich Univ Potsdam Hasso Plattner Inst Potsdam Germany Tech Univ Berlin Berlin Germany Kings Coll London London WC2R 2LS England

Storage strategies have been proposed as a run-time optimization for the PyPy Python implementation and have shown promising results for optimizing execution speed and memory requirements. However, it remained unclear whether the approach works equally well in other dynamic languages. Furthermore, while PyPy is based on RPython, a language to write VMs with reusable components such as a tracing just-in-time compiler and garbage collection, the strategies design itself was not generalized to be reusable across languages implemented using that same toolchain. In this paper, we present a general design and implementation for storage strategies and show how they can be reused across different RPython-based languages. We evaluate the performance of our implementation for RSqueak, an RPython-based VM for Squeak/Smalltalk and show that storage strategies may indeed off er performance benefits for certain workloads in other dynamic programming languages. We furthermore evaluate the generality of our implementation by applying it to Topaz, a Ruby VM, and Pycket, a Racket implementation.

关键词： implementation collection types memory optimization dynamic typing

来源：评论

学校读者我要写书评

暂无评论

PSYNC: A Partially Synchronous language for Fault-Tolerant Distributed Algorithms

引用

acm sigplan NOTICES 2016年第1期51卷 400-415页

作者： Dragoi, Cezara Henzinger, Thomas A. Zufferey, Damien CNRS ENS INRIA F-75700 Paris France IST Austria Vienna Austria MIT CSAIL Boston MA USA

Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.

关键词： Fault-tolerant distributed algorithms Round model Partial synchrony Automated verification Consensus

来源：评论

学校读者我要写书评

暂无评论

Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)

引用

acm sigplan NOTICES 2016年第9期51卷 117-131页

作者： Dimoulas, Christos New, Max S. Findler, Robert Bruce Felleisen, Matthias PLT Morristown NJ 07960 USA

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics. This gem presents a novel analysis of contract systems. Applied to the higher-order kind, this analysis reveals their large and clearly unappreciated software engineering potential. Three sample applications illustrate where this kind of exploration may lead.

关键词： Contracts Specifications language design

来源：评论

学校读者我要写书评

暂无评论

A Lambda-Calculus Foundation for Universal Probabilistic programming

引用

acm sigplan NOTICES 2016年第9期51卷 33-46页

作者： Borgstrom, Johannes Dal Lago, Ugo Gordon, Andrew D. Szymczak, Marcin Uppsala Univ Uppsala Sweden Univ Bologna I-40126 Bologna Italy INRIA Rocquencourt France Microsoft Res Cambridge England Univ Edinburgh Edinburgh EH8 9YL Midlothian Scotland

We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.

关键词： Probabilistic programming Lambda-calculus MCMC Machine Learning Operational Semantics

来源：评论

学校读者我要写书评

暂无评论

Dependent Types and Multi-monadic Effects in F^☆

引用

acm sigplan NOTICES 2016年第1期51卷 256-270页

作者： Swamy, Nikhil Hritcu, Catalin Keller, Chantal Rastogi, Aseem Delignat-Lavaud, Antoine Forest, Simon Bhargavan, Karthikeyan Fournet, Cedric Strub, Pierre-Yves Kohlweiss, Markulf Zinzindohoue, Jean-Karim Zanella-Beguelin, Santiago Microsoft Res Bangalore Karnataka India Inria Rennes France MSR Inria Rennes France UMD Rennes France ENS Paris Paris France IMDEA Software Inst Paris France

We present a new, completely redesigned, version of F-star, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F-star is a dependently typed, higher-order, call-by-value language with primitive effects including state, exceptions, divergence and IO. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F-star uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of SMT solving and manual proofs. Isolated from the effects, the core of F-star is a language of pure functions used to write specifications and proof terms its consistency is maintained by a semantic termination check based on a well-founded order. We evaluate our design on more than 55,000 lines of F-star we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F-star is programmed (but not verified) in F-star, and bootstraps in both OCaml and F#. Our experience confirms F-star's pay-as-you-go cost model: writing idiomatic ML-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F-star is in verifying several key modules in an implementation of the TLS-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F-star than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F-star in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even mu F-star, a sizeable fragment of F-star itself these proofs make essential use of F-star's flexible combination of SMT automation and constructiv

关键词： verification proof assistants effectful programming

来源：评论

学校读者我要写书评

暂无评论

A design and Verification Methodology for Secure Isolated Regions

引用

acm sigplan NOTICES 2016年第6期51卷 665-681页

作者： 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

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

来源：评论

学校读者我要写书评

暂无评论

End-to-End Verification of Information-Flow Security for C and Assembly Programs

引用

acm sigplan NOTICES 2016年第6期51卷 648-664页

作者： Costanzo, David Shao, Zhong Gu, Ronghui Yale Univ New Haven CT 06520 USA

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly;we verify all of the code, regardless of language.

关键词： Verification Security Reliability languages design Information Flow Control Security Policy Specification Security-Preserving Simulation Program Verification Certified OS Kernels

来源：评论

学校读者我要写书评

暂无评论

Modeling and Analysis of Remote Memory Access programming

引用

acm sigplan NOTICES 2016年第10期51卷 129-144页

作者： Dan, Andrei Marian Lam, Patrick Hoefler, Torsten Vechev, Martin Swiss Fed Inst Technol Zurich Switzerland Univ Waterloo Waterloo ON N2L 3G1 Canada

Recent advances in networking hardware have led to a new generation of Remote Memory Access (RMA) networks in which processors from different machines can communicate directly, bypassing the operating system and allowing higher performance. Researchers and practitioners have proposed libraries and programming models for RMA to enable the development of applications running on these networks, However, the memory models implied by these RMA libraries and languages are often loosely specified, poorly understood, and differ depending on the underlying network architecture and other factors. Hence, it is difficult to precisely reason about the semantics of RMA programs or how changes in the network architecture affect them. We address this problem with the following contributions: (i) a coreRMA language which serves as a common foundation, formalizing the essential characteristics of RMA programming;(ii) complete axiomatic semantics for that language;(iii) integration of our semantics with an existing constraint solver, enabling us to exhaustively generate coreRMA programs (litmus tests) up to a specified bound and check whether the tests satisfy their specification;and (iv) extensive validation of our semantics on real-world RMA systems. We generated and ran 7,441 litmus tests using each of the low-level RMA network APIs: DMAPP, VPI Verbs, and Portals 4. Our results confirmed that our model successfully captures behaviors exhibited by these networks. Moreover, we found RMA programs that behave inconsistently with existing documentation, confirmed by network experts. Our work provides an important step towards understanding existing RMA networks, thus influencing the design of future RMA interfaces and hardware.

关键词： Memory Model

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：