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

Pluggable AOP: designing aspect mechanisms for third-party composition 05

Pluggable AOP: designing aspect mechanisms for third-party c...

proceedings of the 20th annual acm sigplan conference on Object-oriented programming, systems, languages, and applications

作者： Sergei Kojarski David H. Lorenz University of Virginia Charlottesville VA

ISBN: (纸本)9781595930316

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.

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

来源：评论

学校读者我要写书评

暂无评论

EXOCHI: Architecture and programming environment for a heterogeneous multi-core multithreaded system

引用

acm sigplan NOTICES 2007年第6期42卷 156-166页

作者： Wang, Perry H. Collins, Jamison D. Chinya, Gautham N. Hong Jiang Xinmin Tian Girkar, Milind Yang, Nick Y. Lueh, Guei-Yuan Wang, Hong Intel Corp Microprocessor Technol Labs Microarchitecture Res Lab Santa Clara CA 95051 USA Intel Corp Chipset Grp Santa Clara CA 95051 USA Intel Corp Software Solut Corp Intel Compiler Lab Santa Clara CA 95051 USA

Future mainstream microprocessors will likely integrate specialized accelerators, such as GPUs, onto a single die to achieve better performance and power efficiency. However, it remains a keen challenge to program such a heterogeneous multi-core platform, since these specialized accelerators feature ISAs and functionality that are significantly different from the general purpose CPU cores. In this paper, we present EXOCHI: (1) Exoskeleton Sequencer (EXO), an architecture to represent heterogeneous accelerators as ISA-based MIMD architecture resources, and a shared virtual memory heterogeneous multithreaded program execution model that tightly couples specialized accelerator cores with general purpose CPU cores, and (2) C for Heterogeneous Integration (CHI), an integrated C/C++ programming environment that supports accelerator-specific inline assembly and domain-specific languages. The CHI compiler extends the OpenMP pragma for heterogeneous multithreading programming, and produces a single fat binary with code sections corresponding to different instruction sets. The runtime can judiciously spread parallel computation across the heterogeneous cores to optimize performance and power. We have prototyped the EXO architecture on a physical heterogeneous platform consisting of an Intel (R) Core (TM) 2 Duo processor and an 8-core 32-thread Intel (R) Graphics Media Accelerator X3000. In addition, we have implemented the CHI integrated programming environment with the Intel (R) C++ Compiler, runtime toolset, and debugger. On the EXO prototype system, we have enhanced a suite of production-quality media kernels for video and image processing to utilize the accelerator through the CHI programming interface, achieving significant speedup (1.41X to 10.97X) over execution on the IA32 CPU alone.

关键词： performance design languages heterogeneous multi-cores GPU OpenMP

来源：评论

学校读者我要写书评

暂无评论

The design and implementation of a certifying compiler 98

The design and implementation of a certifying compiler

引用

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

作者： George C. Necula Peter Lee School of Computer Science Carnegie Mellon University Pittsburgh Pennsylvania

ISBN: (纸本)9780897919876

This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programming language into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the target program. The ensemble of the compiler and the certifier is called a certifying *** advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

CAPSULE: language and system support for efficient state sharing in distributed stream processing systems 12

CAPSULE: Language and system support for efficient state sha...

引用

6th acm International conference on Distributed Event-Based Systems, DEBS'12

作者： Losa, Giuliano Kumar, Vibhore Andrade, Henrique Gedik, Buǧra Hirzel, Martin Soulé, Robert Wu, Kun-Lung Ecole Polytechnique Fédérale de Lausanne Lausanne Switzerland Thomas J. Watson Research Center IBM Research 19 Skyline Drive Hawthorne NY 10532 United States Department of Computer Engineering Bilkent University Bilkent Ankara 06800 Turkey

ISBN: (纸本)9781450313155

Data stream processing applications are often expressed as data flow graphs, composed of operators connected via streams. This structured representation provides a simple yet powerful paradigm for building large-scale, distributed, high-performance applications. However, there are many tasks that require sharing data across operators, and across operators and the runtime using a less structured mechanism than point-to-point data flows. Examples include updating control variables, sending notifications, collecting metrics, building collective models, etc. In this paper we describe CAPSULE, which fills this gap. CAPSULE is a code generation and runtime framework that offers an easy to use and highly flexible framework for developers to realize shared variables (CAPSULE term for shared state) by specifying a data structure (at the programming-language level), and a few associated configuration parameters that qualify the expected usage scenario. Besides the easy of use and flexibility, CAPSULE offers the following important benefits: (1) Custom Code Generation - CAPSULE makes use of user-specified configuration parameters and information from the runtime to generate shared variable servers that are tailored for the specific usage scenario, (2) Composability - CAPSULE supports deployment time composition of the shared variable servers to achieve desired levels of scalability, performance and fault-tolerance, and (3) Extensibility - CAPSULE provides simple interfaces for extending the CAPSULE framework with more protocols, transports, caching mechanisms, etc. We describe the motivation for CAPSULE and its design, report on its implementation status, and then present experimental results. Copyright © 2012 acm.

关键词： Fault tolerance

来源：评论

学校读者我要写书评

暂无评论

CLAP: Recording Local Executions to Reproduce Concurrency Failures 13

CLAP: Recording Local Executions to Reproduce Concurrency Fa...

引用

acm sigplan conference on programming language design and implementation

作者： Jeff Huang Charles Zhang Julian Dolby Hong Kong University of Science and Technology IBM Thomas J. Watson Research Center

ISBN: (纸本)9781450320146

We present CLAP, a new technique to reproduce concurrency bugs. CLAP has two key steps. First, it logs thread local execution paths at runtime. Second, offline, it computes memory dependencies that accord with the logged execution and are able to reproduce the observed bug. The second step works by combining constraints from the thread paths and constraints based on a memory model, and computing an execution with a constraint solver. CLAP has four major advantages. First, logging purely local execution of each thread is substantially cheaper than logging memory interactions, which enables CLAP to be efficient compared to previous approaches. Second, our logging does not require any synchronization and hence with no added memory barriers or fences; this minimizes perturbation and missed bugs due to extra synchronizations foreclosing certain racy behaviors. Third, since it uses no synchronization, we extend CLAP to work on a range of relaxed memory models, such as TSO and PSO, in addition to sequential consistency. Fourth, CLAP can compute a much simpler execution than the original one, that reveals the bug with minimal thread context switches. To mitigate the scalability issues, we also present an approach to parallelize constraint solving, which theoretically scales our technique to programs with arbitrary execution length. Experimental results on a variety of multithreaded benchmarks and real world concurrent applications validate these advantages by showing that our technique is effective in reproducing concurrency bugs even under relaxed memory models; furthermore, it is significantly more efficient than a state-of-the-art technique that records shared memory dependencies, reducing execution time overhead by 45% and log size by 88% on average.

关键词： Concurrency Bug Reproduction Local Execution Constraint Solving Algorithms design Performance Theory

来源：评论

学校读者我要写书评

暂无评论

Behind Every Great Deep Learning Framework Is an Even Greater programming languages Concept (Keynote) 2018

Behind Every Great Deep Learning Framework Is an Even Greate...

引用

26th acm Joint Meeting on European Software Engineering conference (ESEC) / Symposium on the Foundations of Software Engineering (FSE)

作者： Meijer, Erik Delft Univ Technol Software Engn Res Grp Cloud Programming Delft Netherlands Facebook Infra Struct Org Menlo Pk CA 94025 USA

ISBN: (纸本)9781450355735

In many areas, such as image recognition, natural language processing, search, recommendation, autonomous cars, systems software and infrastructure, and even Software Engineering tools themselves, Software 2.0 (= programming using learned models) is quickly swallowing Software 1.0 (= programming using handcrafted algorithms). Where the Software 1.0 Engineer formally specifies their problem, carefully designs algorithms, composes systems out of subsystems or decomposes complex systems into smaller components, the Software 2.0 Engineer amasses training data and simply feeds it into an ML algorithm that will synthesize an approximation of the function whose partial extensional definition is that training data. Instead of code as the artifact of interest, in Software 2.0 it is all about the data where compilation of source code is replaced by training models with data. This new style of programming has far-reaching consequences for traditional software engineering practices. Everything we have learned about life cycle models, project planning and estimation, requirements analysis, program design, construction, debugging, testing, maintenance and implementation, ... runs the danger of becoming obsolete. One way to try to prepare for the new realities of software engineering is not to zero in on the differences between Software 1.0 and Software 2.0 but instead focus on their similarities. If you carefully look at what a neural net actually represents, you realize that in essence it is a pure function, from multi-dimensional arrays of floating point numbers to multi-dimensional arrays of floating point numbers (tensors). What is special about these functions is that they are differentiable (yes, exactly as you remember from middle school calculus), which allows them to be trained using back propagation. The programming language community has also discovered that there is a deep connection between back propagation and continuations. Moreover, when you look closely at how So

关键词： Machine Learning programming languages Functional programming Automatic Differentiation Differentiable programming Deep Learning Continuation Passing Style

来源：评论

学校读者我要写书评

暂无评论

Taming the IXP network processor 03

引用

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

作者： Lal George Matthias Blume Network Speed Technologies Inc Toyota Technological Institute at Chicago

ISBN: (纸本)9781581136623

We compile Nova, a new language designed for writing network processing applications, using a back end based on integer-linear programming (ILP) for register allocation, optimal bank assignment, and spills. The compiler's optimizer employs CPS as its intermediate representation; some of the invariants that this IR guarantees are essential for the formulation of a practical ILP *** and George used a similar ILP-based technique for the IA32 to decide which variables reside in registers but deferred the actual assignment of colors to a later phase. We demonstrate how to carry over their idea to an architecture with many more banks, register aggregates, variables with multiple simultaneous register assignments, and, very importantly, one where bank- and register-assignment cannot be done in isolation from each other. Our approach performs well in practise---without causing an explosion in size or solve time of the generated integer linear programs.

关键词： bank assignment network processors integer linear programming programming languages code generation Intel IXA register allocation

来源：评论

学校读者我要写书评

暂无评论

Mechanizing the meta-theory of programming languages 05

Mechanizing the meta-theory of programming languages

引用

proceedings of the tenth acm sigplan international conference on Functional programming

作者： Robert Harper Carnegie Mellon University Pittsburgh PA

ISBN: (纸本)9781595930644

What does it mean for a programming language to exist? Usually languages are defined by an informal description augmented by a reference compiler whose behavior is regarded as normative. This approach works well so long as the one true implementation suffices, but as soon as we wish to have multiple compilers for the same language, we must agree on what the language is independently of its implementations. Most often this is accomplished through social processes such as standardization committees for building *** processes have served us well, and will continue to be important for language design. But they are not sufficient to support the level of rigor required to prove theorems about languages and programs written in them. For that we need a semantics, which provides an objective foundation for such analyses, typically in the form of a type system and an operational semantics. But merely having such a rigorous definition for a language is not enough — it must be validated by a body of meta-theory that establishes its coherence and its consistency with *** how are we to develop and maintain this body of theory? For full-scale languages the task is so onerous as to inhibit innovation and foster stagnation. The way forward is to take advantage of the recent advances in mechanized reasoning. By representing a language definition within a logical framework we may subject it to formal analysis, much as we use types to express and enforce crucial invariants in our programs. I will describe our use of the Twelf implementation of the LF logical framework, and discuss our successes and difficulties in using it as a tool for mechanizing the meta-theory of programming languages.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Modular interprocedural pointer analysis using access paths: design, implementation, and evaluation 00

Modular interprocedural pointer analysis using access paths:...

引用

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

作者： Ben-Chung Cheng Wen-Mei W. Hwu Department of Computer Science University of Illinois Department of Electrical and Computer Engineering University of Illinois

ISBN: (纸本)9781581131994

In this paper we present a modular interprocedural pointer analysis algorithm based on access-paths for C programs. We argue that access paths can reduce the overhead of representing context-sensitive transfer functions and effectively distinguish non-recursive heap objects. And when the modular analysis paradigm is used together with other techniques to handle type casts and function pointers, we are able to handle significant programs like those in the SPECcint92 and SPECcint95 suites. We have implemented the algorithm and tested it on a Pentium II 450 PC running Linux. The observed resource consumption and performance improvement are very encouraging.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：