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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

17 篇 会议

馆藏范围

17 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

13 篇 工学
- 13 篇 计算机科学与技术...
- 13 篇 软件工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 安全科学与工程
3 篇 理学
- 2 篇 数学
- 2 篇 系统科学
3 篇 管理学
- 2 篇 图书情报与档案管...
- 1 篇 管理科学与工程(可...
- 1 篇 工商管理

主题

2 篇 parallel program...
1 篇 program synthesi...
1 篇 runtime verifica...
1 篇 interactive proo...
1 篇 garbage collecti...
1 篇 computer archite...
1 篇 debugging
1 篇 low-level progra...
1 篇 software archite...
1 篇 user intent
1 篇 optimal systems
1 篇 observers
1 篇 implicit paralle...
1 篇 static analysis
1 篇 spreadsheet prog...
1 篇 computational mo...
1 篇 non-interference
1 篇 runtime monitori...
1 篇 use-site varianc...
1 篇 variance

机构

2 篇 university of to...
2 篇 kyushu institute...
2 篇 kyushu universit...
1 篇 univ wisconsin d...
1 篇 institute for co...
1 篇 department of co...
1 篇 simon fraser uni...
1 篇 university colle...
1 篇 princeton univ p...
1 篇 univ massachuset...
1 篇 electrical and c...
1 篇 school of electr...
1 篇 department of co...
1 篇 google inc. unit...
1 篇 harvard univ cam...
1 篇 university of br...
1 篇 university of ca...
1 篇 computer science...
1 篇 department of co...
1 篇 univ illinois de...

作者

1 篇 kashyap vineeth
1 篇 fedorova alexand...
1 篇 best micah j.
1 篇 nomura jun
1 篇 erlingsson ulfar
1 篇 sherwood timothy
1 篇 lee tsung-hsien
1 篇 tamai tetsuo
1 篇 michelle mills s...
1 篇 jens palsberg
1 篇 yee bennet
1 篇 hassaan m. amber
1 篇 pingali keshav
1 篇 tetsuo tamai
1 篇 roth mark
1 篇 prabhu prakash
1 篇 prountzos dimitr...
1 篇 sui xin
1 篇 naoyasu ubayashi
1 篇 chong frederic t...

语言

17 篇 英文

检索条件"任意字段=32nd ACM Conference on Programming Language Design and Implementation, PLDI 2011"

共 17 条记录，以下是1-10 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

Exadapt'11 - Proceedings of the 1st International Workshop on Adaptive Self-Tuning Computing Systems for the Exaflop Era - In Cooperation with the 32nd acm SIGPLAN conference on programming language design and implementation, pldi 2011

Exadapt'11 - Proceedings of the 1st International Workshop o...

引用

1st acm SIGPLAN International Workshop on Adaptive Self-Tuning Computing Systems for the Exaflop Era, Exadapt 2011 - Co-located with 32nd acm SIGPLAN conference on programming language design and implementation, pldi 2011 at FCRC 2011

ISBN: (纸本)9781450307086

The proceedings contain 7 papers. The topics discussed include: AARTS: low overhead online adaptive auto-tuning;contentiousness vs. sensitivity: improving contention aware runtime systems on multicore architectures;probabilistic auto-tuning for architectures with complex constraints;efficiently exploring compiler optimization sequences with pair-wise pruning;adapt or become extinct!;loaf: a framework and infrastructure for creating online adaptive solutions;and using a codelet program execution model for exascale machines.

关键词： Software architecture

来源：评论

学校读者我要写书评

暂无评论

pldi'11 - Proceedings of the 2011 acm conference on programming language design and implementation

PLDI'11 - Proceedings of the 2011 ACM Conference on Programm...

引用

32nd acm conference on programming language design and implementation, pldi 2011

ISBN: (纸本)9781450306638

The proceedings contain 55 papers. The topics discussed include: commutative set: a language extension for implicit parallel programming;the Tao of parallelism in algorithms;data representation synthesis;synthesizing geometry constructions;synthesis of loop-free programs;generalized just-in-time trace compilation using a parallel task farm in a dynamic binary translator;brainy: effective selection of data structures;an SSA-based algorithm for optimal speculative code motion under an execution profile;caisson: a hardware description language for secure information flow;steno: automatic optimization of declarative queries;languages as libraries;automatic CPU-GPU communication management and optimization;automatic compilation of MATLAB programs for synergistic execution on heterogeneous processors;partial-coherence abstractions for relaxed memory models;and probabilistic, modular and scalable inference of typestate specifications.

关键词： Optimal systems

来源：评论

学校读者我要写书评

暂无评论

Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic 11

Mostly-Automated Verification of Low-Level Programs in Compu...

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Chlipala, Adam Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781450306638

Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems. The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is computational, in the sense that function specifications are usually written in terms of reference implementations in a purely functional language. Logical quantifiers are the most challenging feature for most automated verifiers;by relying on functional programs (written in the expressive language of the Coq proof assistant), we are able to avoid quantifiers almost entirely. This leads to some dramatic improvements compared to both past work in classical verification, which we compare against with implementations of data structures like binary search trees and hash tables;and past work in verified programming with code pointers, which we compare against with examples like function memoization and a cooperative threading library.

关键词： interactive proof assistants separation logic low-level programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

Caisson: A Hardware Description language for Secure Information Flow 11

Caisson: A Hardware Description Language for Secure Informat...

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Li, Xun Tiwari, Mohit Oberg, Jason K. Kashyap, Vineeth Chong, Frederic T. Sherwood, Timothy Hardekopf, Ben Univ Calif Santa Barbara Dept Comp Sci Santa Barbara CA 93106 USA

ISBN: (纸本)9781450306638

Information flow is an important security property that must be incorporated from the ground up, including at hardware design time, to provide a formal basis for a system's root of trust. We incorporate insights and techniques from designing information-flow secure programming languages to provide a new perspective on designing secure hardware. We describe a new hardware description language, Caisson, that combines domain-specific abstractions common to hardware design with insights from type-based techniques used in secure programming languages. The proper combination of these elements allows for an expressive, provably-secure HDL that operates at a familiar level of abstraction to the target audience of the language, hardware architects. We have implemented a compiler for Caisson that translates designs into Verilog and then synthesizes the designs using existing tools. As an example of Caisson's usefulness we have addressed an open problem in secure hardware by creating the first-ever provably information-flow secure processor with micro-architectural features including pipelining and cache. We synthesize the secure processor and empirically compare it in terms of chip area, power consumption, and clock frequency with both a standard (insecure) commercial processor and also a processor augmented at the gate level to dynamically track information flow. Our processor is competitive with the insecure processor and significantly better than dynamic tracking.

关键词： Hardware Description language Non-interference State Machine

来源：评论

学校读者我要写书评

暂无评论

Commutative Set: A language Extension for Implicit Parallel programming 11

Commutative Set: A Language Extension for Implicit Parallel ...

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Prabhu, Prakash Ghosh, Soumyadeep Zhang, Yun Johnson, Nick P. August, David I. Princeton Univ Princeton NJ 08544 USA

ISBN: (纸本)9781450306638

Sequential programming models express a total program order, of which a partial order must be respected. This inhibits parallelizing tools from extracting scalable performance. Programmer written semantic commutativity assertions provide a natural way of relaxing this partial order, thereby exposing parallelism implicitly in a program. Existing implicit parallel programming models based on semantic commutativity either require additional programming extensions, or have limited expressiveness. This paper presents a generalized semantic commutativity based programming extension, called Commutative Set (COMMSET), and associated compiler technology that enables multiple forms of parallelism. COMMSET expressions are syntactically succinct and enable the programmer to specify commutativity relations between groups of arbitrary structured code blocks. Using only this construct, serializing constraints that inhibit parallelization can be relaxed, independent of any particular parallelization strategy or concurrency control mechanism. COMMSET enables well performing parallelizations in cases where they were inapplicable or non-performing before. By extending eight sequential programs with only 8 annotations per program on average, Comm S ET and the associated compiler technology produced a geomean speedup of 5.7x on eight cores compared to 1.5x for the best non-COMMSET parallelization.

关键词： Implicit parallelism semantic commutativity programming model automatic parallelization static analysis

来源：评论

学校读者我要写书评

暂无评论

Spreadsheet Table Transformations from Examples 11

Spreadsheet Table Transformations from Examples

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Harris, William R. Gulwani, Sumit Univ Wisconsin Dept Comp Sci Madison WI 53706 USA

ISBN: (纸本)9781450306638

Every day, millions of computer end-users need to perform tasks over large, tabular data, yet lack the programming knowledge to do such tasks automatically. In this work, we present an automatic technique that takes from a user an example of how the user needs to transform a table of data, and provides to the user a program that implements the transformation described by the example. In particular, we present a language of programs TableProg that can describe transformations that real users require. We then present an algorithm ProgFrornEx that takes an example input and output table, and infers a program in TableProg that implements the transformation described by the example. When the program is applied to the example input, it reproduces the example output. When the program is applied to another, potentially larger, table with a "similar" layout as the example input table, then the program produces a corresponding table with a layout that is similar to the example output table. A user can apply ProgFrornEx interactively, providing multiple small examples to obtain a program that implements the transformation that the user desires. Moreover, ProgFromEx can help identify "noisy" examples that contain errors. To evaluate the practicality of TableProg and ProgFromEx, we implemented ProgFromEx as a module for the Microsoft Excel spreadsheet program. We applied the module to automatically implement over 50 table transformations specified by end-users through examples on online Excel help forums. In seconds, ProgFromEx found programs that satisfied the examples and could be applied to larger input tables. This experience demonstrates that TableProg and ProgFromEx can significantly automate the tasks over tabular data that users need to perform.

关键词： Program Synthesis End-user programming programming by Example Spreadsheet programming Table Manipulation User Intent

来源：评论

学校读者我要写书评

暂无评论

Synchronization via scheduling: Techniques for efficiently managing shared state 11

Synchronization via scheduling: Techniques for efficiently m...

引用

32nd acm conference on programming language design and implementation, pldi 2011

作者： Best, Micah J. Mottishaw, Shane Mustard, Craig Roth, Mark Fedorova, Alexandra Brownsword, Andrew University of British Columbia Canada Simon Fraser University Canada Electronic Arts Inc. Canada

ISBN: (纸本)9781450306638

Shared state access conflicts are one of the greatest sources of error for fine grained parallelism in any domain. Notoriously hard to debug, these conflicts reduce reliability and increase development time. The standard task graph model dictates that tasks with potential conflicting accesses to shared state must be linked by a dependency, even if there is no explicit logical ordering on their execution. In cases where it is difficult to understand if such implicit dependencies exist, the programmer often creates more dependencies than needed, which results in constrained graphs with large monolithic tasks and limited parallelism. We propose a new technique, Synchronization via Scheduling (SvS), that uses the results of static and dynamic code analysis to manage potential shared state conflicts by exposing the data accesses of each task to the scheduler. We present an in-depth performance analysis of SvS via examples from video games, our target domain, and show that SvS performs well in comparison to software transactional memory (TM) and fine grained mutexes. © 2011 acm.

关键词： Parallel programming

来源：评论

学校读者我要写书评

暂无评论

Garbage Collection for Monitoring Parametric Properties 11

Garbage Collection for Monitoring Parametric Properties

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Jin, Dongyun Meredith, Patrick O'Neil Griffith, Dennis Rosu, Grigore Univ Illinois Dept Comp Sci Urbana IL USA

ISBN: (纸本)9781450306638

Parametric properties are behavioral properties over program events that depend on one or more parameters. Parameters are bound to concrete data or objects at runtime, which makes parametric properties particularly suitable for stating multi-object relationships or protocols. Monitoring parametric properties independently of the employed formalism involves slicing traces with respect to parameter instances and sending these slices to appropriate non-parametric monitor instances. The number of such instances is theoretically unbounded and tends to be enormous in practice, to an extent that how to efficiently manage monitor instances has become one of the most challenging problems in runtime verification. The previous formalism-independent approach was only able to do The obvious, namely to garbage collect monitor instances when all bound parameter objects were garbage collected. This led to pathological behaviors where unnecessary monitor instances were kept for the entire length of a program. This paper proposes a new approach to garbage collecting monitor instances. Unnecessary monitor instances are collected lazily to avoid creating undue overhead. This lazy collection, along with some careful engineering, has resulted in RV, the most efficient parametric monitoring system to date. Our evaluation shows that the average overhead of RV in the DaCapo benchmark is 15%, which is two times lower than that of Java MOP and orders of magnitude lower than that of Tracematches.

关键词： runtime verification runtime monitoring testing debugging aspect-oriented programming garbage collection

来源：评论

学校读者我要写书评

暂无评论

Taming the Wildcards: Combining Definition- and Use-Site Variance 11

Taming the Wildcards: Combining Definition- and Use-Site Var...

引用

32nd acm SIGPLAN conference on programming language design and implementation (pldi 11)

作者： Altidor, John Huang, Shan Shan Smaragdakis, Yannis Univ Massachusetts Dept Comp Sci Amherst MA 01003 USA

ISBN: (纸本)9781450306638

Variance allows the safe integration of parametric and subtype polymorphism. Two flavors of variance, definition-site versus use-site variance, have been studied and have had their merits hotly debated. Definition-site variance (as in Scala and C#) offers simple type-instantiation rules, but causes fractured definitions of naturally invariant classes;Use-site variance (as in Java) offers simplicity in class definitions, yet complex type-instantiation rules that elude most programmers. We present a unifying framework for reasoning about variance. Our framework is quite simple and entirely denotational, that is, it evokes directly the definition of variance with a small core calculus that does not depend on specific type systems. This general framework can have multiple applications to combine the best of both worlds: for instance, it can be used to add use-site variance annotations to the Scala type system. We show one such application in detail: we extend the Java type system with a mechanism that modularly infers the definition-site variance of type parameters, while allowing use-site variance annotations on any type-instantiation. Applying our technique to six Java generic libraries (including the Java core library) shows that 20-58% (depending on the library) of generic definitions are inferred to have single-variance;8-63% of method signatures can be relaxed through this inference, and up to 91% of existing wildcard annotations are unnecessary and can be elided.

关键词： variance definition-site variance use-site variance wildcards language extensions

来源：评论

学校读者我要写书评

暂无评论

AARTS: Low overhead online adaptive auto-tuning 11

AARTS: Low overhead online adaptive auto-tuning

引用

作者： Teodoro, George Sussman, Alan Department of Computer Science University of Maryland College Park MD 20742 United States

ISBN: (纸本)9781450307086

We present an online lightweight auto-tuning system for shared-memory parallel programs. We employ an online adaptive tuning algorithm that is based on performance measurements, to adapt to performance variability that arises during program execution. We address the impact of synchronous vs. asynchronous interactions between the application and the tuning system, and describe an adaptive approach that benefits from the improvements provided by both options. We presented a performance study of the online tuning system, and compared it to synchronous tuning systems. Finally, AARTS is evaluated under different scenarios, showing the potential benefits of using online tuning and the ability of AARTS to exploit those benefits. © 2011 acm.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共2页 << < 1 2 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：