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

11th International conference on Architectural Support for programming languages and Operating Systems

作者： Budiu, M Venkataramani, G Chelcea, T Goldstein, SC Carnegie Mellon Univ Pittsburgh PA 15213 USA

this paper describes a computer architecture, Spatial Computation (SC), which is based on the translation of high-level language programs directly into hardware structures. SC program implementations are completely distributed, with no centralized control. SC circuits are optimized for wires at the expense of computation units. In this paper we investigate a particular implementation of SC: ASH (Application-Specific Hardware). Under the assumption that computation is cheaper than communication, ASH replicates computation units to simplify interconnect, building a system which uses very simple, completely dedicated communication channels. As a consequence, communication on the datapath never requires arbitration;the only arbitration required is for accessing memory. ASH relies on very simple hardware primitives, using no associative structures, no multiported register files, no scheduling logic, no broadcast, and no clocks. As a consequence, ASH hardware is fast and extremely power efficient. In this work we demonstrate three features of ASH: (1) that such architectures can be built by automatic compilation of C programs;(2) that distributed computation is in some respects fundamentally different from monolithic superscalar processors;and (3) that ASIC implementations of ASH use three orders of magnitude less energy compared to high-end superscalar processors, while being on average only 33% slower in performance (3.5x worst-case).

关键词： measurement performance design spatial computation dataflow machine application-specific hardware low-power

来源：评论

学校读者我要写书评

暂无评论

Implicitly-threaded parallelism in Manticore

引用

acm sigplan NOTICES 2008年第9期43卷 119-130页

作者： Fluet, Matthew Rainey, Mike Reppy, John Shaw, Adam Toyota Technol Inst Chicago IL 60637 USA Univ Chicago Chicago IL 60637 USA

the increasing availability of commodity multicore processors is making parallel computing available to the masses. Traditional parallel languages are largely intended for large-scale scientific computing and tend not to be well-suited to programming the applications one typically finds on a desktop system. thus we need new parallel-language designs that address a broader spectrum of applications. In this paper, we present Manticore, a language for building parallel applications on commodity multicore hardware including a diverse collection of parallel constructs for different granularities of work. We focus on the implicitly-threaded parallel constructs in our high-level functional language. We concentrate on those elements that distinguish our design from related ones, namely, a novel parallel binding form, a nondeterministic parallel case form, and exceptions in the presence of data parallelism. these features differentiate the present work from related work on functional data parallel language designs, which has focused largely on parallel problems with regular structure and the compiler transformations - most notably, flattening - that make such designs feasible. We describe our implementation strategies and present some detailed examples utilizing various mechanisms of our language.

关键词： design languages implicitly-threaded parallelism data parallelism parallel binding parallel case exceptions

来源：评论

学校读者我要写书评

暂无评论

Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs

引用

acm sigplan NOTICES 2011年第2期46卷 127-136页

作者： Rompf, Tiark Odersky, Martin Ecole Polytech Fed Lausanne CH-1015 Lausanne Switzerland

Software engineering demands generality and abstraction, performance demands specialization and concretization. Generative programming can provide both, but developing high-quality program generators takes a large effort, even if a multi-stage programming language is used. We present lightweight modular staging, a library-based multi-stage programming approach that breaks with the tradition of syntactic quasi-quotation and instead uses only types to distinguish between binding times. through extensive use of component technology, lightweight modular staging makes an optimizing compiler framework available at the library level, allowing programmers to tightly integrate domain-specific abstractions and optimizations into the generation process. We argue that lightweight modular staging enables a form of language virtualization, i.e. allows to go from a pure-library embedded language to one that is practically equivalent to a stand-alone implementation with only modest effort.

关键词： design languages Code Generation Multi-stage programming Domain-specific languages language Virtualization

来源：评论

学校读者我要写书评

暂无评论

Pluggable AOP - designing aspect mechanisms for third-party composition

引用

acm sigplan NOTICES 2005年第10期40卷 247-263页

作者： Kojarski, S Lorenz, DH Univ Virginia Dept Comp Sci Charlottesville VA 22904 USA

Studies of Aspect-Oriented programming (AOP) usually focus on a language in which a specific aspect extension is integrated with a base language. languages specified in this manner have a fixed, non-extensible AOP functionality. this paper argues the need for AOP to support the integration and use of multiple domain-specific aspect extensions together. We study the more general case of integrating a base language with a set of third-party aspect extensions for that language. We present a general mixin-based semantic framework for implementing dynamic aspect extensions in such a way that multiple, independently developed aspect mechanisms can be subject to third-party composition and work collaboratively. Principles governing the design of a collaborative aspect mechanism are aspectual effect exposure and implementation hiding.

关键词： design languages theory AOP AOSD domain-specific aspect language aspect extension aspect mechanism aspectual effect granularity software components CBSE third-party composition collaboration reuse mixin semantics AspectJ AspectWerkz COOL

来源：评论

学校读者我要写书评

暂无评论

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

引用

acm sigplan NOTICES 2016年第6期51卷 431-447页

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

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

来源：评论

学校读者我要写书评

暂无评论

the Bedrock Structured programming System Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier

引用

acm sigplan NOTICES 2013年第9期48卷 391-402页

作者： Chlipala, Adam MIT CSAIL United States

We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. the abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language;but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.

关键词： generative metaprogramming interactive proof assistants low-level programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

Linearity and PCF: a Semantic Insight! 11

Linearity and PCF: a Semantic Insight!

引用

16th acm sigplan International conference on Functional programming (ICFP 11)

作者： Gaboardi, Marco Paolini, Luca Piccolo, Mauro Univ Bologna INRIA Focus Team Dip Sci Informaz I-40127 Bologna Italy Univ Turin Dipartimento Informat I-10149 Turin Italy

ISBN: (纸本)9781450308656

Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces. We introduce a language, named SlPCF(star), that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF(star) allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler. Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. the first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. the second one is more concrete and it prunes such a space, by exploiting the linear assumptions. this can also be regarded as a base for an implementation.

关键词： languages theory design PCF Linear Logic Denotational Semantics Operational Semantics

来源：评论

学校读者我要写书评

暂无评论

Acute: High-level programming language design for distributed computation

引用

acm sigplan NOTICES 2005年第9期40卷 15-26页

作者： Sewell, P Leifer, JJ Wansbrough, K Nardelli, FZ Allen-Williams, M Habouzit, P Vafeiadis, V Univ Cambridge Cambridge CB2 1TN England

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. the main features are: (1) type-safe marshalling of arbitrary values;(2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system;(3) expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g. values carried on named channels;(4) controlled dynamic rebinding of marshalled values to local resources;and (5) thunkification of threads and mutexes to support computation mobility. these features are a large part of what is needed for typeful distributed programming. they are a relatively lightweight extension of M L, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. this disentangles the language runtime from communication intricacies. this paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.

关键词： languages design programming languages distributed programming marshalling serialisation abstract types modules rebinding version control type theory ML

来源：评论

学校读者我要写书评

暂无评论

Sapper: A language for hardware-level security policy enforcement 14

Sapper: A language for hardware-level security policy enforc...

引用

19th International conference on Architectural Support for programming languages and Operating Systems, ASPLOS 2014

作者： Li, Xun Kashyap, Vineeth Oberg, Jason K. Tiwari, Mohit Rajarathinam, Vasanth Ram Kastner, Ryan Sherwood, Timothy Hardekopf, Ben Chong, Frederic T. Facebook United States University of California Santa Barbara United States University of California San Diego United States University of Texas Austin United States AMD United States

ISBN: (纸本)9781450323055

Privacy and integrity are important security concerns. these concerns are addressed by controlling information flow, i.e., restricting how information can flow through a system. Most proposed systems that restrict information flow make the implicit assumption that the hardware used by the system is fully " correct" and that the hardware's instruction set accurately describes its behavior in all circumstances. the truth is more complicated: modern hardware designs defy complete verification, many aspects of the timing and ordering of events are left totally unspecified, and implementation bugs present themselves with surprising frequency. In this work we describe Sapper, a novel hardware description language for designing security-critical hardware components. Sapper seeks to address these problems by using static analysis at compile-time to automatically insert dynamic checks in the resulting hardware that provably enforce a given information flow policy at execution time. We present Sapper's design and formal semantics along with a proof sketch of its security. In addition, we have implemented a compiler for Sapper and used it to create a non-trivial secure embedded processor with many modern microarchitectural features. We empirically evaluate the resulting hardware's area and energy over-head and compare them with alternative designs. Copyright © 2014 acm.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Adding delimited and composable control to a production programming environment

引用

acm sigplan NOTICES 2007年第9期42卷 165-176页

作者： Flatt, Matthew Yu, Gang Findler, Robert Bruce Felleisen, Matthias Univ Utah Salt Lake City UT 84112 USA Chinese Acad Sci Inst Software Beijing 100864 Peoples R China Univ Chicago Chicago IL 60637 USA Northeastern Univ Boston MA 02115 USA

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs-such as exceptions and dynamic binding-remains relatively unexplored. In this paper, we report on our effort of translating the theory of delimited and composable control into a viable implementation for a production system. the report shows how this effort involved a substantial design element, including work with a formal model, as well as significant practical exploration and engineering. the resulting version of PLT Scheme incorporates the expressive combination of delimited and composable control alongside dynamic-wind, dynamic binding, and exception handling. None of the additional operators subvert the intended benefits of existing control operators, so that programmers can freely mix and match control operators.

关键词： design languages

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：