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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

238 篇 会议
3 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

196 篇 工学
- 191 篇 软件工程
- 79 篇 计算机科学与技术...
- 6 篇 电气工程
- 1 篇 机械工程
- 1 篇 动力工程及工程热...
- 1 篇 控制科学与工程
- 1 篇 生物工程
6 篇 理学
- 5 篇 数学
- 1 篇 生物学
- 1 篇 系统科学
2 篇 教育学
- 2 篇 教育学
2 篇 管理学
- 1 篇 管理科学与工程(可...
- 1 篇 图书情报与档案管...

主题

46 篇 design
38 篇 languages
22 篇 performance
15 篇 algorithms
14 篇 probabilistic pr...
12 篇 verification
12 篇 functional progr...
11 篇 program synthesi...
10 篇 reliability
9 篇 object oriented ...
9 篇 experimentation
9 篇 programming lang...
8 篇 domain-specific ...
8 篇 concurrency
7 篇 type systems
7 篇 java
6 篇 optimization
5 篇 compilers
5 篇 metaprogramming
5 篇 theory

机构

8 篇 purdue univ w la...
7 篇 carnegie mellon ...
5 篇 harvard univ cam...
4 篇 univ wisconsin m...
4 篇 princeton univ p...
4 篇 univ calif davis...
4 篇 northeastern uni...
4 篇 cornell univ ith...
4 篇 univ penn philad...
4 篇 stanford univ st...
4 篇 univ washington ...
3 篇 microsoft res re...
3 篇 swiss fed inst t...
3 篇 mit cambridge ma...
3 篇 yale univ new ha...
3 篇 rice univ housto...
3 篇 univ calif berke...
3 篇 univ texas austi...
2 篇 microsoft corp r...
2 篇 oracle labs pots...

作者

5 篇 foster nate
5 篇 gulwani sumit
5 篇 walker david
4 篇 shao zhong
4 篇 dillig isil
3 篇 huang jeff
3 篇 vechev martin
3 篇 su zhendong
3 篇 chaudhuri swarat
3 篇 myers andrew c.
3 篇 zhang xiangyu
3 篇 mansinghka vikas...
2 篇 hirschfeld rober...
2 篇 flatt matthew
2 篇 gupta gagan
2 篇 shull thomas
2 篇 yahav eran
2 篇 rajamani sriram
2 篇 niephaus fabio
2 篇 choi jiho

语言

240 篇 英文
1 篇 中文

检索条件"任意字段=Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation"

共 241 条记录，以下是11-20 订阅

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

详细简洁

排序：

Profile- Guided Meta-programming 15

Profile- Guided Meta-Programming

引用

36th acm sigplan conference on programming language design and implementation

作者： Bowman, William J. Miller, Swaha St-Amour, Vincent Dybvig, R. Kent Northeastern Univ Boston MA 02115 USA Cisco Syst Inc San Jose CA USA

ISBN: (纸本)9781450334686

Contemporary compiler systems such as GCC,. NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems-the syntactic extensions systems of Chez Scheme and Racket- and provide several profile-guided meta-programs as usability case studies.

关键词： design Performance languages Optimization profiling profile-guided optimization PGO meta-programming

来源：评论

学校读者我要写书评

暂无评论

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO 15

Relaxing Safely: Verified On-the-Fly Garbage Collection for ...

引用

36th acm sigplan conference on programming language design and implementation

作者： Gammie, Peter Hosking, Antony L. Engelhardt, Kai Purdue Univ W Lafayette IN 47907 USA UNSW Sydney NSW Australia

ISBN: (纸本)9781450334686

We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. the proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. the abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.

关键词： Algorithms design languages Reliability Verification formal verification machine-checked proof relaxed memory TSO

来源：评论

学校读者我要写书评

暂无评论

A Simpler, Safer programming and Execution Model for Intermittent Systems 15

A Simpler, Safer Programming and Execution Model for Intermi...

引用

36th acm sigplan conference on programming language design and implementation

作者： Lucia, Brandon Ransford, Benjamin Carnegie Mellon Univ Pittsburgh PA 15213 USA Univ Washington Seattle WA 98195 USA

ISBN: (纸本)9781450334686

Energy harvesting enables novel devices and applications without batteries, but intermittent operation under energy harvesting poses new challenges to memory consistency that threaten to leave applications in failed states not reachable in continuous execution. this paper presents analytical models that aid in reasoning about intermittence. Using these, we develop DINO (Death Is Not an Option), a programming and execution model that simplifies programming for intermittent systems and ensures volatile and nonvolatile data consistency despite near-constant interruptions. DINO is the first system to address these consistency problems in the context of intermittent execution. We evaluate DINO on three energy-harvesting hardware platforms running different applications. the applications fail and exhibit error without DINO, but run correctly with DINO's modest 1.8-2.7x run-time overhead. DINO also dramatically simplifies programming, reducing the set of possible failure-related control transfers by 5-9x.

关键词： Intermittent computing

来源：评论

学校读者我要写书评

暂无评论

Asynchronous programming, analysis and testing with state machines 15

Asynchronous programming, analysis and testing with state ma...

引用

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

作者： Deligiannis, Pantazis Donaldson, Alastair F. Ketema, Jeroen Lal, Akash thomson, Paul Imperial College London United Kingdom Microsoft Research India

ISBN: (纸本)9781450334686

programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. © 2015 acm.

关键词： Testing

来源：评论

学校读者我要写书评

暂无评论

Stateless Model Checking Concurrent Programs with Maximal Causality Reduction 15

Stateless Model Checking Concurrent Programs with Maximal Ca...

引用

36th acm sigplan conference on programming language design and implementation

作者： Huang, Jeff Texas A&M Univ College Stn TX 77843 USA

ISBN: (纸本)9781450334686

We present maximal causality reduction (MCR), a new technique for stateless model checking. MCR systematically explores the state-space of concurrent programs with a provably minimal number of executions. Each execution corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent executions. Moreover, MCR is embarrassingly parallel by shifting the runtime exploration cost to offline analysis. We have designed and implemented MCR using a constraint-based approach and compared with iterative context bounding (ICB) and dynamic partial order reduction (DPOR) on both benchmarks and real-world programs. MCR reduces the number of executions explored by ICB and ICB+DPOR by orders of magnitude, and significantly improves the scalability, efficiency, and effectiveness of the state-of-the-art for both state-space exploration and bug finding. In our experiments, MCR also revealed several new data races and null pointer dereference errors in frequently studied real-world programs.

关键词： Algorithms design theory Maximal Causality Reduction Model Checking

来源：评论

学校读者我要写书评

暂无评论

Interactive Parser Synthesis by Example 15

Interactive Parser Synthesis by Example

引用

36th acm sigplan conference on programming language design and implementation

作者： Leung, Alan Sarracino, John Lerner, Sorin Univ Calif San Diego San Diego CA 92103 USA

ISBN: (纸本)9781450334686

Despite decades of research on parsing, the construction of parsers remains a painstaking, manual process prone to subtle bugs and pitfalls. We present a programming-by-example framework called Parsify that is able to synthesize a parser from input/output examples. the user does not write a single line of code. To achieve this, Parsify provides: (a) an iterative algorithm for synthesizing and refining a grammar one example at a time, (b) an interface that provides immediate visual feedback in response to changes in the grammar being refined, and (c) a graphical mechanism for specifying example parse trees using only textual selections. We empirically demonstrate the viability of our approach by using Parsify to construct parsers for source code drawn from Verilog, SQL, Apache, and Tiger.

关键词： Algorithms Human Factors languages Parsing programming by Example Program Synthesis

来源：评论

学校读者我要写书评

暂无评论

Defining the Undefinedness of C 15

Defining the Undefinedness of C

引用

36th acm sigplan conference on programming language design and implementation

作者： Hathhorn, Chris Ellison, Chucky Rosu, Grigore Univ Missouri Columbia MO 65211 USA Univ Illinois Urbana IL 61801 USA

ISBN: (纸本)9781450334686

We present a "negative" semantics of the C11 language-a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. the amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself.

关键词： Undefined behavior programming language semantics C11 K Framework

来源：评论

学校读者我要写书评

暂无评论

Declarative programming over Eventually Consistent Data Stores 15

Declarative Programming over Eventually Consistent Data Stor...

引用

36th acm sigplan conference on programming language design and implementation

作者： Sivaramakrishnan, K. C. Kaki, Gowtham Jagannathan, Suresh Univ Cambridge Cambridge CB2 1TN England Purdue Univ W Lafayette IN 47907 USA

ISBN: (纸本)9781450334686

User-facing online services utilize geo-distributed data stores to minimize latency and tolerate partial failures, with the intention of providing a fast, always-on experience. However, geo-distribution does not come for free;application developers have to contend with weak consistency behaviors, and the lack of abstractions to composably construct high-level replicated data types, necessitating the need for complex application logic and invariably exposing inconsistencies to the user. Some commercial distributed data stores and several academic proposals provide a lattice of consistency levels, with stronger consistency guarantees incurring increased latency and throughput costs. However, correctly assigning the right consistency level for an operation requires subtle reasoning and is often an error-prone task. In this paper, we present QUELEA, a declarative programming model for eventually consistent data stores (ECDS), equipped with a contract language, capable of specifying fine-grained application-level consistency properties. A contract enforcement system analyses contracts, and automatically generates the appropriate consistency protocol for the method protected by the contract. We describe an implementation of QUELEA on top of an off-the-shelf ECDS that provides support for coordination-free transactions. Several benchmarks including two large web applications, illustrate the effectiveness of our approach.

关键词： languages Performance Eventual Consistency Availability CRDTs Axiomatic Contracts Contract Classification Distributed Transactions SMT solvers Decidable Logic Quelea Cassandra Haskell

来源：评论

学校读者我要写书评

暂无评论

Concurrency Debugging with Differential Schedule Projections 15

Concurrency Debugging with Differential Schedule Projections

引用

36th acm sigplan conference on programming language design and implementation

作者： Machado, Nuno Lucia, Brandon Rodrigues, Luis Univ Lisbon Inst Super Tecn INESC ID P-1699 Lisbon Portugal Carnegie Mellon Univ Pittsburgh PA 15213 USA

ISBN: (纸本)9781450334686

We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% fewer data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix.

关键词： Algorithms design Reliability Concurrency Debugging Symbolic Execution Constraint Solving Differential Schedule Projection

来源：评论

学校读者我要写书评

暂无评论

Synthesizing Racy Tests 15

Synthesizing Racy Tests

引用

36th acm sigplan conference on programming language design and implementation

作者： Samak, Malavika Ramanathan, Murali Krishna Jagannathan, Suresh Indian Inst Sci Bangalore 560012 Karnataka India Purdue Univ W Lafayette IN 47907 USA

ISBN: (纸本)9781450334686

Subtle concurrency errors in multithreaded libraries that arise because of incorrect or inadequate synchronization are often difficult to pinpoint precisely using only static techniques. On the other hand, the effectiveness of dynamic race detectors is critically dependent on multithreaded test suites whose execution can be used to identify and trigger races. Usually, such multithreaded tests need to invoke a specific combination of methods with objects involved in the invocations being shared appropriately to expose a race. Without a priori knowledge of the race, construction of such tests can be challenging. In this paper, we present a lightweight and scalable technique for synthesizing precisely these kinds of tests. Given a multithreaded library and a sequential test suite, we describe a fully automated analysis that examines sequential execution traces, and produces as its output a concurrent client program that drives shared objects via library method calls to states conducive for triggering a race. Experimental results on a variety of well-tested Java libraries yield 101 synthesized multithreaded tests in less than four minutes. Analyzing the execution of these tests using an off-the-shelf race detector reveals 187 harmful races, including several previously unreported ones.

关键词： design Reliability Verification Race detection dynamic analysis concurrency

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共25页 << < 1 2 3 4 5 6 7 8 9 10 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：