The proceedings contain 46 papers. The topics discussed include: exploring and improving code completion for test code;on the generalizability of deep learning-based code completion across programminglanguage version...
ISBN:
(纸本)9798400705861
The proceedings contain 46 papers. The topics discussed include: exploring and improving code completion for test code;on the generalizability of deep learning-based code completion across programminglanguage versions;ESGen: commit message generation based on edit sequence of code change;capturing and understanding the drift between design, implementation, and documentation;towards summarizing code snippets using pre-trained transformers;improving AST-level code completion with graph retrieval and multi-field attention;HyperCRX: a browser extension for insights into GitHub projects and developers;innovating coding: evaluating the impact of innovative thinking in programming;and MESIA: understanding and leveraging supplementary nature of method-level comments for automatic comment generation.
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;pr...
详细信息
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.
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 ...
详细信息
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.
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 fo...
详细信息
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.
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 a...
详细信息
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 programminglanguages 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 programminglanguages. 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.
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 commutativit...
详细信息
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.
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 f...
详细信息
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.
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 stand...
详细信息
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 su...
详细信息
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.
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-sit...
详细信息
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.
暂无评论