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

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Singh, Rishabh Gulwani, Sumit Solar-Lezama, Armando MIT CSAIL Cambridge MA USA Microsoft Res Redmond WA USA

ISBN: (纸本)9781450320146

We present a new method for automatically providing feedback for introductory programming problems. In order to use this method, we need a reference implementation of the assignment, and an error model consisting of potential corrections to errors that students might make. Using this information, the system automatically derives minimal corrections to student's incorrect solutions, providing them with a measure of exactly how incorrect a given solution was, as well as feedback about what they did wrong. We introduce a simple language for describing error models in terms of correction rules, and formally define a rule-directed translation strategy that reduces the problem of finding minimal corrections in an incorrect program to the problem of synthesizing a correct program from a sketch. We have evaluated our system on thousands of real student attempts obtained from the Introduction to programming course at MIT (6.00) and MITx (6.00x). Our results show that relatively simple error models can correct on average 64% of all incorrect submissions in our benchmark set.

关键词： Automated Grading Computer-Aided Education Program Synthesis

来源：评论

学校读者我要写书评

暂无评论

Reconciling Exhaustive Pattern Matching with Objects

Reconciling Exhaustive Pattern Matching with Objects

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Isradisaikul, Chinawat Myers, Andrew C. Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

ISBN: (纸本)9781450320146

Pattern matching, an important feature of functional languages, is in conflict with data abstraction and extensibility, which are central to object-oriented languages. Modal abstraction offers an integration of deep pattern matching and convenient iteration abstractions into an object-oriented setting;however, because of data abstraction, it is challenging for a compiler to statically verify properties such as exhaustiveness. In this work, we extend modal abstraction in the JMatch language to support static, modular reasoning about exhaustiveness and redundancy. New matching specifications allow these properties to be checked using an SMT solver. We also introduce expressive pattern-matching constructs. Our evaluation shows that these new features enable more concise code and that the performance of checking exhaustiveness and redundancy is acceptable.

关键词： JMatch pattern matching named constructor equality constructor matching specification exhaustiveness redundancy modal abstraction Java data abstraction subtyping design Verification languages

来源：评论

学校读者我要写书评

暂无评论

Functional Reactive programming with Liveness Guarantees As relations are to set-valued functions, so event sources are to behaviours

引用

acm sigplan NOTICES 2013年第9期48卷 233-243页

作者： Jeffrey, Alan Alcatel Lucent Bell Labs Murray Hill NJ USA

Functional Reactive programming (FRP) is an approach to the development of reactive systems which provides a pure functional interface, but which may be implemented as an abstraction of an imperative event-driven layer. FRP systems typically provide a model of behaviours (total time-indexed values, implemented as pull systems) and event sources (partial time-indexed values, implemented as push systems). In this paper, we investigate a type system for event-driven FRP programs which provide liveness guarantees, that is every input event is guaranteed to generate an output event. We show that FRP can be implemented on top of a model of sets and relations, and that the isomorphism between event sources and behaviours corresponds to the isomorphism between relations and set-valued functions. We then implement sets and relations using a model of continuations using the usual double-negation CPS transform. The implementation of behaviours as pull systems based on futures, and of event sources as push systems based on the observer pattern, thus arises from first principles. We also discuss a Java implementation of the FRP model.

关键词： design Theory Functional Reactive programming Concurrency Liveness

来源：评论

学校读者我要写书评

暂无评论

Correctness of an STM Haskell implementation 13

Correctness of an STM Haskell Implementation

引用

18th acm sigplan International conference on Functional programming

作者： Schmidt-Schauss, Manfred Sabel, David Goethe Univ Frankfurt Frankfurt Germany

ISBN: (纸本)9781450323260

A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a bigstep semantics.

关键词： languages Theory Verification Functional programming Concurrent programming Semantics Software Transactional Memory Haskell

来源：评论

学校读者我要写书评

暂无评论

CONCURRIT: A Domain Specific language for Reproducing Concurrency Bugs

CONCURRIT: A Domain Specific Language for Reproducing Concur...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Elmas, Tayfun Burnim, Jacob Necula, George Sen, Koushik Univ Calif Berkeley Dept Elect Engn & Comp Sci Berkeley CA 94720 USA

ISBN: (纸本)9781450320146

We present CONCURRIT, a domain-specific language (DSL) for reproducing concurrency bugs. Given some partial information about the nature of a bug in an application, a programmer can write a CONCURRIT script to formally and concisely specify a set of thread schedules to explore in order to find a schedule exhibiting the bug. Further, the programmer can specify how these thread schedules should be searched to find a schedule that reproduces the bug. We implemented CONCURRIT as an embedded DSL in C++, which uses manual or automatic source instrumentation to partially control the scheduling of the software under test. Using CONCURRIT, we were able to write concise tests to reproduce concurrency bugs in a variety of benchmarks, including the Mozilla's Spider-Monkey JavaScript engine, Memcached, Apache's HTTP server, and MySQL.

关键词： Concurrency Errors Domain-Specific languages Software Testing

来源：评论

学校读者我要写书评

暂无评论

P: Safe Asynchronous Event-Driven programming

P: Safe Asynchronous Event-Driven Programming

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Desai, Ankush Gupta, Vivek Jackson, Ethan Qadeer, Shaz Rajamani, Sriram Zufferey, Damien Microsoft Corp Redmond WA 98052 USA

ISBN: (纸本)9781450320146

We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to "close" the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code;a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhandled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P);we have more confidence in the robustness of its design due to the language abstractions and verification provided by P.

关键词： domain-specific language device driver event-driven programming state machine verification systematic testing

来源：评论

学校读者我要写书评

暂无评论

A General Constraint-centric Scheduling Framework for Spatial Architectures

A General Constraint-centric Scheduling Framework for Spatia...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Nowatzki, Tony Sartin-Tarm, Michael De Carli, Lorenzo Sankaralingam, Karthikeyan Estan, Cristian Robatmili, Behnam Univ Wisconsin Madison WI 53706 USA

ISBN: (纸本)9781450320146

Specialized execution using spatial architectures provides energy efficient computation, but requires effective algorithms for spatially scheduling the computation. Generally, this has been solved with architecture-specific heuristics, an approach which suffers from poor compiler/architect productivity, lack of insight on optimality, and inhibits migration of techniques between architectures. Our goal is to develop a scheduling framework usable for all spatial architectures. To this end, we expresses spatial scheduling as a constraint satisfaction problem using Integer Linear programming (ILP). We observe that architecture primitives and scheduler responsibilities can be related through five abstractions: placement of computation, routing of data, managing event timing, managing resource utilization, and forming the optimization objectives. We encode these responsibilities as 20 general ILP constraints, which are used to create schedulers for the disparate TRIPS, DySER, and PLUG architectures. Our results show that a general declarative approach using ILP is implementable, practical, and typically matches or outperforms specialized schedulers.

关键词： Spatial Architectures Spatial Architecture Scheduling Integer Linear programming

来源：评论

学校读者我要写书评

暂无评论

Fast Algorithms for Dyck-CFL-Reachability with Applications to Alias Analysis

Fast Algorithms for Dyck-CFL-Reachability with Applications ...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Zhang, Qirun Lyu, Michael R. Yuan, Hao Su, Zhendong Chinese Univ Hong Kong Hong Kong Hong Kong Peoples R China Univ Calif Davis Davis CA 95616 USA City Univ Hong Kong Hong Kong Hong Kong Peoples R China

ISBN: (纸本)9781450320146

The context-free language (CFL) reachability problem is a well-known fundamental formulation in program analysis. In practice, many program analyses, especially pointer analyses, adopt a restricted version of CFL-reachability, Dyck-CFL-reachability, and compute on edge-labeled bidirected graphs. Solving the all-pairs Dyck-CFL-reachability on such bidirected graphs is expensive. For a bidirected graph with n nodes and m edges, the traditional dynamic programming style algorithm exhibits a subcubic time complexity for the Dyck language with k kinds of parentheses. When the underlying graphs are restricted to bidirected trees, an algorithm with O(n log n log k) time complexity was proposed recently. This paper studies the Dyck-CFL-reachability problems on bidirected trees and graphs. In particular, it presents two fast algorithms with O(n) and O(n+m log m) time complexities on trees and graphs respectively. We have implemented and evaluated our algorithms on a state-of-the-art alias analysis for Java. Results on standard benchmarks show that our algorithms achieve orders of magnitude speedup and consume less memory.

关键词： Algorithms design Experimentation languages Dyck-CFL-reachability alias analysis

来源：评论

学校读者我要写书评

暂无评论

Storage Strategies for Collections in Dynamically Typed languages

引用

acm sigplan NOTICES 2013年第10期48卷 167-182页

作者： Bolz, Carl Friedrich Diekmann, Lukas Tratt, Laurence Univ Dusseldorf Dusseldorf Germany Hasso Plattner Inst Potsdam Potsdam Germany Kings Coll London London WC2R 2LS England

Dynamically typed language implementations often use more memory and execute slower than their statically typed cousins, in part because operations on collections of elements are unoptimised. This paper describes storage strategies, which dynamically optimise collections whose elements are instances of the same primitive type. We implement storage strategies in the PyPy virtual machine, giving a performance increase of 18% on wide-ranging benchmarks of real Python programs. We show that storage strategies are simple to implement, needing only 1500LoC in PyPy, and have applicability to a wide range of virtual machines.

关键词： Algorithms languages Performance implementation collection types memory optimization dynamic typing

来源：评论

学校读者我要写书评

暂无评论

Harmonizing Classes, Functions, Tuples, and Type Parameters in Virgil III 13

Harmonizing Classes, Functions, Tuples, and Type Parameters ...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Titzer, Ben L. Google Mountain View CA USA

ISBN: (纸本)9781450320146

languages are becoming increasingly multi-paradigm. Subtype polymorphism in statically-typed object-oriented languages is being supplemented with parametric polymorphism in the form of generics. Features like first-class functions and lambdas are appearing everywhere. Yet existing languages like Java, C#, C++, D, and Scala seem to accrete ever more complexity when they reach beyond their original paradigm into another;inevitably older features have some rough edges that lead to nonuniformity and pitfalls. Given a fresh start, a new language designer is faced with a daunting array of potential features. Where to start? What is important to get right first, and what can be added later? What features must work together, and what features are orthogonal? We report on our experience with Virgil III, a practical language with a careful balance of classes, functions, tuples and type parameters. Virgil intentionally lacks many advanced features, yet we find its core feature set enables new species of design patterns that bridge multiple paradigms and emulate features not directly supported such as interfaces, abstract data types, ad hoc polymorphism, and variant types. Surprisingly, we find variance for function types and tuple types often replaces the need for other kinds of type variance when libraries are designed in a more functional style.

关键词： Multi-paradigm languages parametric types object-oriented programming functional programming monomorphization variance closures tuples flattening unboxing static compilation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：