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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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

分类表

所选分类

>> <<

限定检索结果

文献类型

2,277 篇 会议
296 篇 期刊文献
2 册 图书

馆藏范围

2,575 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

2,280 篇 工学
- 2,149 篇 软件工程
- 1,702 篇 计算机科学与技术...
- 85 篇 控制科学与工程
- 57 篇 信息与通信工程
- 55 篇 电气工程
- 23 篇 电子科学与技术（可...
- 17 篇 机械工程
- 14 篇 建筑学
- 14 篇 土木工程
- 13 篇 材料科学与工程（可...
- 13 篇 生物工程
- 10 篇 光学工程
- 9 篇 安全科学与工程
- 8 篇 化学工程与技术
- 5 篇 动力工程及工程热...
- 5 篇 生物医学工程（可授...
- 4 篇 力学（可授工学、理...
278 篇 理学
- 217 篇 数学
- 30 篇 系统科学
- 18 篇 统计学（可授理学、...
- 16 篇 物理学
- 16 篇 生物学
- 8 篇 化学
- 6 篇 地质学
207 篇 管理学
- 112 篇 图书情报与档案管...
- 107 篇 管理科学与工程(可...
- 48 篇 工商管理
22 篇 教育学
- 22 篇 教育学
17 篇 法学
- 15 篇 社会学
9 篇 经济学
- 9 篇 应用经济学
2 篇 农学
2 篇 艺术学
1 篇 军事学

主题

390 篇 design
369 篇 languages
187 篇 computer program...
182 篇 performance
162 篇 object oriented ...
89 篇 algorithms
88 篇 java programming...
81 篇 experimentation
78 篇 functional progr...
71 篇 computer program...
71 篇 theory
65 篇 java
63 篇 verification
61 篇 reliability
48 篇 semantics
47 篇 software design
45 篇 domain-specific ...
38 篇 parallel program...
37 篇 concurrency
35 篇 measurement

机构

25 篇 carnegie mellon ...
22 篇 univ washington ...
18 篇 univ penn philad...
17 篇 princeton univ p...
17 篇 stanford univ st...
16 篇 univ texas austi...
15 篇 harvard univ cam...
14 篇 purdue univ w la...
13 篇 microsoft res re...
13 篇 microsoft resear...
13 篇 rice univ housto...
12 篇 univ wisconsin m...
12 篇 mit cambridge ma...
12 篇 cornell univ ith...
12 篇 microsoft res ca...
11 篇 univ michigan an...
11 篇 swiss fed inst t...
11 篇 univ calif berke...
10 篇 microsoft res re...
10 篇 yale univ new ha...

作者

19 篇 hirschfeld rober...
16 篇 walker david
15 篇 visser eelco
15 篇 felleisen matthi...
14 篇 findler robert b...
13 篇 grossman dan
13 篇 bacon david f.
12 篇 chlipala adam
11 篇 flatt matthew
11 篇 sarkar vivek
11 篇 myers andrew c.
11 篇 mezini mira
11 篇 morrisett greg
10 篇 mckinley kathryn...
10 篇 bockisch christo...
10 篇 adl-tabatabai al...
10 篇 van der storm ti...
10 篇 de moor oege
10 篇 dillig isil
9 篇 lumsdaine a

语言

2,354 篇 英文
216 篇 其他
4 篇 中文
1 篇 葡萄牙文

检索条件"任意字段=ACM SIGPLAN Conference on Programming Language Design and Implementation"

共 2575 条记录，以下是751-760 订阅

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

详细简洁

排序：

Deterministic Parallelism via Liquid Effects 12

Deterministic Parallelism via Liquid Effects

引用

33rd acm sigplan conference on programming language design and implementation

作者： Kawaguchi, Ming Rondon, Patrick Bakst, Alexander Jhala, Ranjit Univ Calif San Diego San Diego CA 92103 USA

ISBN: (纸本)9781450312059

Shared memory multithreading is a popular approach to parallel programming, but also fiendishly hard to get right. We present Liquid Effects, a type-and-effect system based on refinement types which allows for fine-grained, low-level, shared memory multithreading while statically guaranteeing that a program is deterministic. Liquid Effects records the effect of an expression as a formula in first-order logic, making our type-and-effect system highly expressive. Further, effects like Read and Write are recorded in Liquid Effects as ordinary uninterpreted predicates, leaving the effect system open to extension by the user. By building our system as an extension to an existing dependent refinement type system, our system gains precise value- and branch-sensitive reasoning about effects. Finally, our system exploits the Liquid Types refinement type inference technique to automatically infer refinement types and effects. We have implemented our type-and-effect checking techniques in CSOLVE, a refinement type inference system for C programs. We demonstrate how CSOLVE uses Liquid Effects to prove the determinism of a variety of benchmarks.

关键词： languages Reliability Verification Liquid Types Type Inference Dependent Types C Safe Parallel programming Determinism

来源：评论

学校读者我要写书评

暂无评论

Static Analysis and Compiler design for Idempotent Processing 12

Static Analysis and Compiler Design for Idempotent Processin...

引用

33rd acm sigplan conference on programming language design and implementation

作者： de Kruijf, Marc Sankaralingam, Karthikeyan Jha, Somesh Univ Wisconsin Madison WI 53706 USA

ISBN: (纸本)9781450312059

Recovery functionality has many applications in computing systems, from speculation recovery in modern microprocessors to fault recovery in high-reliability systems. Modern systems commonly recover using checkpoints. However, checkpoints introduce overheads, add complexity, and often save more state than necessary. This paper develops a novel compiler technique to recover program state without the overheads of explicit checkpoints. The technique breaks programs into idempotent regions-regions that can be freely re-executed-which allows recovery without checkpointed state. Leveraging the property of idempotence, recovery can be obtained by simple re-execution. We develop static analysis techniques to construct these regions and demonstrate low overheads and large region sizes for an LLVM-based implementation. Across a set of diverse benchmark suites, we construct idempotent regions close in size to those that could be obtained with perfect runtime information. Although the resulting code runs more slowly, typical performance overheads are in the range of just 2-12%. The paradigm of executing entire programs as a series of idempotent regions we call idempotent processing, and it has many applications in computer systems. As a concrete example, we demonstrate it applied to the problem of compiler-automated hardware fault recovery. In comparison to two other state-of-the-art techniques, redundant execution and checkpoint-logging, our idempotent processing technique outperforms both by over 15%.

关键词： Algorithms design Performance Reliability Idempotent processing idempotent regions

来源：评论

学校读者我要写书评

暂无评论

design and implementation of Sparse Global Analyses for C-like languages 12

Design and Implementation of Sparse Global Analyses for C-li...

引用

33rd acm sigplan conference on programming language design and implementation

作者： Oh, Hakjoo Heo, Kihong Lee, Wonchan Lee, Woosuk Yi, Kwangkeun Seoul Natl Univ Seoul 151 South Korea

ISBN: (纸本)9781450312059

In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework;we present that existing sparse analyses are all restricted instances of our framework;we show more semantically elaborate design examples of sparse non-relational and relational static analyses;we present their implementation results that scale to analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.

关键词： Static analysis abstract interpretation sparse analysis

来源：评论

学校读者我要写书评

暂无评论

The Implicit Calculus A New Foundation for Generic programming 12

The Implicit Calculus A New Foundation for Generic Programmi...

引用

33rd acm sigplan conference on programming language design and implementation

作者： Oliveira, Bruno C. d. S. Schrijvers, Tom Choi, Wontae Lee, Wonchan Yi, Kwangkeun Seoul Natl Univ Seoul 151 South Korea Univ Ghent Ghent Belgium

ISBN: (纸本)9781450312059

Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces;and 2) implicit instantiation of implementations of those interfaces. Scala implicits are a GP language mechanism, inspired by type classes, that break with the tradition of coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit instantiation, which is generalized to work for any types. This turns out to be quite powerful and useful to address many limitations that show up in other GP mechanisms. This paper synthesizes the key ideas of implicits formally in a minimal and general core calculus called the implicit calculus (lambda(double right arrow)), and it shows how to build source languages supporting implicit instantiation on top of it. A novelty of the calculus is its support for partial resolution and higher-order rules (a feature that has been proposed before, but was never formalized or implemented). Ultimately, the implicit calculus provides a formal model of implicits, which can be used by language designers to study and inform implementations of similar mechanisms in their own languages.

关键词： languages Implicit parameters type classes C plus plus concepts generic programming Haskell Scala

来源：评论

学校读者我要写书评

暂无评论

And Then There Were None: A Stall-Free Real-Time Garbage Collector for Reconfigurable Hardware 12

And Then There Were None: A Stall-Free Real-Time Garbage Col...

引用

33rd acm sigplan conference on programming language design and implementation

作者： Bacon, David F. Cheng, Perry Shukla, Sunil IBM Research Hawthorne NY USA

ISBN: (纸本)9781450312059

Programmers are turning to radical architectures such as reconfigurable hardware (FPGAs) to achieve performance. But such systems, programmed at a very low level in languages with impoverished abstractions, are orders of magnitude more complex to use than conventional CPUs. The continued exponential increase in transistors, combined with the desire to implement ever more sophisticated algorithms, makes it imperative that such systems be programmed at much higher levels of abstraction. One of the fundamental high-level language features is automatic memory management in the form of garbage collection. We present the first implementation of a complete garbage collector in hardware (as opposed to previous "hardware-assist" techniques), using an FPGA and its on-chip memory. Using a completely concurrent snapshot algorithm, it provides single-cycle access to the heap, and never stalls the mutator for even a single cycle, achieving a deterministic mutator utilization (MMU) of 100%. We have synthesized the collector to hardware and show that it never consumes more than 1% of the logic resources of a high-end FPGA. For comparison we also implemented explicit (malloc/free) memory management, and show that real-time collection is about 4% to 17% slower than malloc, with comparable energy consumption. Surprisingly, in hardware real-time collection is superior to stop-the-world collection on every performance axis, and even for stressful micro-benchmarks can achieve 100% MMU with heaps as small as 1.01 to 1.4 times the absolute minimum.

关键词： design languages Experimentation Performance Block RAM FPGA High Level Synthesis Garbage Collection Real Time

来源：评论

学校读者我要写书评

暂无评论

Speculative Separation for Privatization and Reductions 12

Speculative Separation for Privatization and Reductions

引用

33rd acm sigplan conference on programming language design and implementation

作者： Johnson, Nick P. Kim, Hanjun Prabhu, Prakash Zaks, Ayal August, David I. Princeton Univ Princeton NJ 08544 USA Intel Corp Haifa Israel

ISBN: (纸本)9781450312059

Automatic parallelization is a promising strategy to improve application performance in the multicore era. However, common programming practices such as the reuse of data structures introduce artificial constraints that obstruct automatic parallelization. Privatization relieves these constraints by replicating data structures, thus enabling scalable parallelization. Prior privatization schemes are limited to arrays and scalar variables because they are sensitive to the layout of dynamic data structures. This work presents Privateer, the first fully automatic privatization system to handle dynamic and recursive data structures, even in languages with unrestricted pointers. To reduce sensitivity to memory layout, Privateer speculatively separates memory objects. Privateer's lightweight runtime system validates speculative separation and speculative privatization to ensure correct parallel execution. Privateer enables automatic parallelization of general-purpose C/C++ applications, yielding a geomean whole-program speedup of 11.4x over best sequential execution on 24 cores, while non-speculative parallelization yields only 0.93x.

关键词： languages Performance design Experimentation Automatic parallelization Separation Speculation

来源：评论

学校读者我要写书评

暂无评论

programming with Binders and Indexed Data-Types 12

Programming with Binders and Indexed Data-Types

引用

39th Annual acm sigplan-SIGACT Symposium on Principles of programming languages

作者： Cave, Andrew Pientka, Brigitte McGill Univ Montreal PQ H3A 2T5 Canada

ISBN: (纸本)9781450310833

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. This allows the user to specify formal systems within the logical framework LF and index ML types with contextual LF objects. Our language design keeps the index language generic only requiring decidability of equality of the index language providing a modular design. To illustrate the elegance and effectiveness of our language, we give programs for closure conversion and normalization by evaluation. Our three key technical contribution are: 1) We give a bidirectional type system for our core language which is centered around refinement substitutions instead of constraint solving. As a consequence, type checking is decidable and easy to trust, although constraint solving may be undecidable. 2) We give a big-step environment based operational semantics with environments which lends itself to efficient implementation. 3) We prove our language to be type safe and have mechanized our theoretical development in the proof assistant Coq using the fresh approach to binding.

关键词： Logical frameworks higher-order abstract syntax dependent types recursive types

来源：评论

学校读者我要写书评

暂无评论

Parcae: A System for Flexible Parallel Execution 12

Parcae: A System for Flexible Parallel Execution

引用

33rd acm sigplan conference on programming language design and implementation

作者： Raman, Arun Zaks, Ayal Lee, Jae W. August, David I. Intel Res Santa Clara CA USA Intel Corp Haifa Israel Sungkyunkwan Univ Suwon South Korea Princeton Univ Princeton NJ 08544 USA

ISBN: (纸本)9781450312059

Workload, platform, and available resources constitute a parallel program's execution environment. Most parallelization efforts statically target an anticipated range of environments, but performance generally degrades outside that range. Existing approaches address this problem with dynamic tuning but do not optimize a multiprogrammed system holistically. Further, they either require manual programming effort or are limited to array-based data-parallel programs. This paper presents Parcae, a generally applicable automatic system for platform-wide dynamic tuning. Parcae includes (i) the Nona compiler, which creates flexible parallel programs whose tasks can be efficiently reconfigured during execution;(ii) the Decima monitor, which measures resource availability and system performance to detect change in the environment;and (iii) the Morta executor, which cuts short the life of executing tasks, replacing them with other functionally equivalent tasks better suited to the current environment. Parallel programs made flexible by Parcae outperform original parallel implementations in many interesting scenarios.

关键词： design Performance automatic parallelization code generation compiler flexible multicore parallel performance portability run-time adaptivity tuning

来源：评论

学校读者我要写书评

暂无评论

Logical Inference Techniques for Loop Parallelization 12

Logical Inference Techniques for Loop Parallelization

引用

33rd acm sigplan conference on programming language design and implementation

作者： Oancea, Cosmin E. Rauchwerger, Lawrence Univ Copenhagen HIPERFIT Dept Comp Sci DK-1168 Copenhagen Denmark Texas A&M Univ Parasol Lab College Stn TX 77843 USA

ISBN: (纸本)9781450312059

This paper presents a fully automatic approach to loop parallelization that integrates the use of static and run-time analysis and thus overcomes many known difficulties such as nonlinear and indirect array indexing and complex control flow. Our hybrid analysis framework validates the parallelization transformation by verifying the independence of the loop's memory references. To this end it represents array references using the USR (uniform set representation) language and expresses the independence condition as an equation, S = empty set, where S is a set expression representing array indexes. Using a language instead of an array-abstraction representation for S results in a smaller number of conservative approximations but exhibits a potentially-high runtime cost. To alleviate this cost we introduce a language translation F from the USR set-expression language to an equally rich language of predicates (F(S) double right arrow S = empty set). Loop parallelization is then validated using a novel logic inference algorithm that factorizes the obtained complex predicates (F(S)) into a sequence of sufficient-independence conditions that are evaluated first statically and, when needed, dynamically, in increasing order of their estimated complexities. We evaluate our automated solution on 26 benchmarks from PERFECT-CLUB and SPEC suites and show that our approach is effective in parallelizing large, complex loops and obtains much better full program speedups than the Intel and IBM Fortran compilers.

关键词： Performance design Algorithms auto-parallelization USR independence predicates

来源：评论

学校读者我要写书评

暂无评论

Adaptive Input-aware Compilation for Graphics Engines 12

Adaptive Input-aware Compilation for Graphics Engines

引用

33rd acm sigplan conference on programming language design and implementation

作者： Samadi, Mehrzad Hormati, Amir Mehrara, Mojtaba Lee, Janghaeng Mahlke, Scott Univ Michigan Ann Arbor MI 48109 USA Microsoft Res Redmond WA USA NVIDIA Res Santa Clara CA USA

ISBN: (纸本)9781450312059

While graphics processing units (GPUs) provide low-cost and efficient platforms for accelerating high performance computations, the tedious process of performance tuning required to optimize applications is an obstacle to wider adoption of GPUs. In addition to the programmability challenges posed by GPU's complex memory hierarchy and parallelism model, a well-known application design problem is target portability across different GPUs. However, even for a single GPU target, changing a program's input characteristics can make an already-optimized implementation of a program perform poorly. In this work, we propose Adaptic, an adaptive input-aware compilation system to tackle this important, yet overlooked, input portability problem. Using this system, programmers develop their applications in a high-level streaming language and let Adaptic undertake the difficult task of input portable optimizations and code generation. Several input-aware optimizations are introduced to make efficient use of the memory hierarchy and customize thread composition. At runtime, a properly optimized version of the application is executed based on the actual program input. We perform a head-to-head comparison between the Adaptic generated and hand-optimized CUDA programs. The results show that Adaptic is capable of generating codes that can perform on par with their hand-optimized counterparts over certain input ranges and outperform them when the input falls out of the hand-optimized programs' "comfort zone". Furthermore, we show that input-aware results are sustainable across different GPU targets making it possible to write and optimize applications once and run them anywhere.

关键词： design languages Performance Streaming Compiler GPU Optimization Portability

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共258页 << < 72 73 74 75 76 77 78 79 80 81 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：