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

37th acm sigplan conference on programming language design and implementation

作者： Laurenzano, Michael A. Hill, Parker Samadi, Mehrzad Mahlke, Scott Mars, Jason Tang, Lingjia Univ Michigan Dept Elect Engn & Comp Sci Ann Arbor MI 48109 USA

ISBN: (纸本)9781450342612

This paper introduces Input Responsive Approximation ( IRA), an approach that uses a canary input - a small program input carefully constructed to capture the intrinsic properties of the original input - to automatically control how program approximation is applied on an input-by-input basis. Motivating this approach is the observation that many of the prior techniques focusing on choosing how to approximate arrive at conservative decisions by discounting substantial differences between inputs when applying approximation. The main challenges in overcoming this limitation lie in making the choice of how to approximate both effectively (e.g., the fastest approximation that meets a particular accuracy target) and rapidly for every input. With IRA, each time the approximate program is run, a canary input is constructed and used dynamically to quickly test a spectrum of approximation alternatives. Based on these runtime tests, the approximation that best fits the desired accuracy constraints is selected and applied to the full input to produce an approximate result. We use IRA to select and parameterize mixes of four approximation techniques from the literature for a range of 13 image processing, machine learning, and data mining applications. Our results demonstrate that IRA significantly outperforms prior approaches, delivering an average of 10.2x speedup over exact execution while minimizing accuracy losses in program outputs.

关键词： Performance Runtime Systems Compilers Approximate Computing Performance Experimentation design

来源：评论

学校读者我要写书评

暂无评论

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers 16

Toward Compositional Verification of Interruptible OS Kernel...

引用

37th acm sigplan conference on programming language design and implementation

作者： Chen, Hao Wu, Xiongnan (Newman) Shao, Zhong Lockerman, Joshua Gu, Ronghui Univ Elect Sci & Technol China UESTC Chengdu Peoples R China Yale Univ New Haven CT 06520 USA

ISBN: (纸本)9781450342612

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.

关键词： Verification Reliability Security languages design Program Verification Certified OS Kernels Interrupts Device Drivers Abstraction Layer Modularity

来源：评论

学校读者我要写书评

暂无评论

Disjoint Intersection Types 2016

Disjoint Intersection Types

引用

21st acm sigplan International conference on Functional programming (ICFP)

作者： Oliveira, Bruno C. d. S. Shi, Zhiyuan Alpuim, Joao Univ Hong Kong Hong Kong Hong Kong Peoples R China

ISBN: (纸本)9781450342193

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programming languages, as the semantics of the programming language becomes implementation-dependent. This paper presents lambda(i) : a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of lambda(i), with three variants of disjointness. In the simplest variant, which does not allow inverted perpendicular types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce inverted perpendicular types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with inverted perpendicular types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.

关键词： Intersection Types Type System design languages Theory

来源：评论

学校读者我要写书评

暂无评论

SLE 2016 - proceedings of the 2016 acm sigplan International conference on Software language Engineering, co-located with SPLASH 2016

SLE 2016 - Proceedings of the 2016 ACM SIGPLAN International...

引用

9th acm sigplan International conference on Software language Engineering, SLE 2016

ISBN: (纸本)9781450344470

The proceedings contain 23 papers. The topics discussed include: parsing and reflective printing, bidirectionally;taming context-sensitive languages with principled stateful parsing;efficient development of consistent projectional editors using grammar cells;experiences of Models@run-time with EMF and CDO;runtime support for rule-based access-control evaluation through model-transformation;object-oriented design pattern for DSL program monitoring;execution framework of the GEMOC studio;language design and implementation for the domain of coding conventions;BSML-mbeddr: integrating semantically configurable state-machine models in a C programming environment;adding uncertainty and units to quantity types in software models;FRaMED: full-fledge role modeling editor;towards a universal code formatter through machine learning;the IDE portability problem and its solution in Monto;principled syntactic code completion using placeholders;automated testing support for reactive domain-specific modelling languages;symbolic execution of high-level transformations;and raincode assembler compiler.

关键词：

来源：评论

学校读者我要写书评

暂无评论

GPCE 2016 - proceedings of the 2016 acm sigplan International conference on Generative programming: Concepts and Experiences, co-located with SPLASH 2016

GPCE 2016 - Proceedings of the 2016 ACM SIGPLAN Internationa...

引用

15th acm sigplan International conference on Generative programming: Concepts and Experiences, GPCE 2016

ISBN: (纸本)9781450344463

The proceedings contain 20 papers. The topics discussed include: Recaf: Java dialects as libraries;classless Java;extensible modeling with managed data in Java;actor profiling in virtual execution environments;bootstrapping domain-specific meta-languages in language workbenches;dependence-driven delimited CPS transformation for JavaScript;synthesizing regular expressions from examples for introductory automata assignments;programmable semantic fragments: the design and implementation of typy;delaying decisions in variable concern hierarchies;automatic code generation in practice: experiences with embedded robot controllers;a change-centric approach to compile configurable systems with #ifdefs;a feature-based personalized recommender system for product-line configuration;IncLing: efficient product-line testing using incremental pairwise sampling;towards a software product line of trie-based collections;tool demo: testing configurable systems with FeatureIDE;automated regression testing of BPMN 2.0 processes: a capture and replay framework for continuous delivery;a vision for online verification-validation;and automatic non-functional testing of code generators families.

关键词：

来源：评论

学校读者我要写书评

暂无评论

An Experience in Ada Multicore programming: Parallelisation of a Model Checking Engine 21st

An Experience in Ada Multicore Programming: Parallelisation ...

引用

21st Ada-Europe International conference on Reliable Software Technologies (Ada-Europe)

作者： Mazzanti, Franco CNR ISTI Ist Sci & Tecnol Informaz A Faedo Pisa Italy

ISBN: (纸本)9783319390833;9783319390826

Even if multicore architectures are nowadays extremely wide- spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine- tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.

关键词： Model checking Parallel programming Multicore processor architectures Ada programming language

来源：评论

学校读者我要写书评

暂无评论

acm International conference Proceeding Series

ACM International Conference Proceeding Series

引用

28th Symposium on the implementation and Application of Functional programming languages, IFL 2016

ISBN: (纸本)9781450347679

The proceedings contain 11 papers. The topics discussed include: signal rate inference for multidimensional Faust;type directives and type graphs in elm;towards the layout of things;a portable VM-based implementation platform for non-strict functional programming languages;contractive functions on infinite data structures;design and implementation of probabilistic programming language Anglican;a lazy language needs a lazy type system: introducing polymorphic contexts;Eliom: tierless web programming from the ground up;synthesis of railway-signaling plans using reachability games;a lightweight hat: simple type-preserving instrumentation for self-tracing lazy functional programs;and identifying and introducing interfaces and callbacks using wrangler.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Memory Systems Performance and Correctness, MSPC 2014 - In Conjunction with the 35th acm sigplan conference on programming language design and implementation, PLDI 2014

Memory Systems Performance and Correctness, MSPC 2014 - In C...

引用

2014 Workshop on Memory Systems Performance and Correctness, MSPC 2014 - In Conjunction with the 35th acm sigplan conference on programming language design and implementation, PLDI 2014

ISBN: (纸本)9781450329170

The proceedings contain 9 papers. The topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performance of Intel sandy bridge and AMD bulldozer;non-volatile memory is a broken time machine;O-structures: semantics for versioned memory;outlawing ghosts: avoiding out-of-thin-air results;and trash in cache: detecting eternally silent stores.

关键词：

来源：评论

学校读者我要写书评

暂无评论

From Datalog to FLIX: A Declarative language for Fixed Points on Lattices

引用

acm sigplan NOTICES 2016年第6期51卷 194-208页

作者： Madsen, Magnus Yee, Ming-Ho Lhotak, Ondrej Univ Waterloo Waterloo ON N2L 3G1 Canada

We present FLIX, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-naive evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of FLIX clearly exposes the similarity between these two algorithms.

关键词： logic programming static analysis Datalog Logic programming Static Analysis

来源：评论

学校读者我要写书评

暂无评论

Temporal NetKAT

引用

acm sigplan NOTICES 2016年第6期51卷 386-401页

作者： Beckett, Ryan Greenberg, Michael Walker, David Princeton Univ Princeton NJ 08544 USA Pomona Coll Claremont CA 91711 USA

Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.

关键词： Software-defined networking Network programming languages Domain-specific languages Kleene algebra with tests NetKAT Temporal logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：