the proceedings contain 9 papers. the topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performanc...
ISBN:
(纸本)9781450329170
the proceedings contain 9 papers. the topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performance of Intel sandy bridge and AMD bulldozer;non-volatile memory is a broken time machine;O-structures: semantics for versioned memory;outlawing ghosts: avoiding out-of-thin-air results;and trash in cache: detecting eternally silent stores.
the proceedings contain 59 papers. the topics discussed include: automatic error elimination by horizontal code transfer across multiple applications;mechanized verification of fine-grained concurrent programs;algorit...
ISBN:
(纸本)9781450334686
the proceedings contain 59 papers. the topics discussed include: automatic error elimination by horizontal code transfer across multiple applications;mechanized verification of fine-grained concurrent programs;algorithmic debugging of real-world Haskell programs: deriving dependencies from the cost centre stack;light: replay via tightly bounded recording;provably correct peephole optimizations with alive;automatically improving accuracy for floating point expressions;diagnosing type errors with class;verification of producer-consumer synchronization in GPU programs;verification of a cryptographic primitive: SHA-256;asynchronous programming, analysis and testing with state machines;laminarIR: compile-time queues for structured streams;optimizing off-chip accesses in multicores;improving compiler scalability: optimizing large programs at small price;verifying read-copy-update in a logic for weak memory;and stateless model checking concurrent programs with maximal causality reduction.
the proceedings contain 36 papers. the topics discussed include: optimizing memory transactions;better extensibility through modular syntax;practical dynamic software updating for C;shared memory programming for large...
详细信息
ISBN:
(纸本)1595933204
the proceedings contain 36 papers. the topics discussed include: optimizing memory transactions;better extensibility through modular syntax;practical dynamic software updating for C;shared memory programming for large scale machines;SAFECode: enforcing allias analysis for weakly typed languages;pruning dynamic slices with confidence;context-sensitive domain-independent algorithm composition and selection;a global progressive register allocator;accurate, efficient, and adaptive calling context profiling;eventrons: a safe programming construct for high-frequency hard real time applications;continuations and transducer composition;effective static race detection for Java;profile-guided proactive garbage collection for locality optimization;refinement-based context-sensitive points - to analysis for Java;modular verification of assembly code with stack-based control abstractions;and termination proofs for systems code.
the proceedings contain 48 papers. the topics discussed include: into the depths of C: elaborating the de facto standards;data-driven precondition inference with learned features;Cartesian Hoare logic for verifying k-...
ISBN:
(纸本)9781450342612
the proceedings contain 48 papers. the topics discussed include: into the depths of C: elaborating the de facto standards;data-driven precondition inference with learned features;Cartesian Hoare logic for verifying k-safety properties;verifying bit-manipulations of floating-point;coverage-directed differential testing of JVM implementations;lightweight computation tree tracing for lazy functional languages;effective padding of multidimensional arrays to avoid cache conflict misses;input responsiveness: using canary inputs to dynamically steer approximation;configuration synthesis for programmable analog devices with Arco;from datalog to flix: a declarative language for fixed points on lattices;latte: a language, compiler, and runtime for elegant and efficient deep neural networks;on the complexity and performance of parsing with derivatives;and toward compositional verification of interruptible OS kernels and device drivers.
the proceedings contain 46 papers. the topics discussed include: optimizing database-backed applications with query synthesis;automated feedback generation for introductory programming assignments;fast condensation of...
ISBN:
(纸本)9781450320146
the proceedings contain 46 papers. the topics discussed include: optimizing database-backed applications with query synthesis;automated feedback generation for introductory programming assignments;fast condensation of the program dependence graph;scalable variable and data type detection in a binary rewriter;rely-guarantee references for refinement types over aliased mutable data;harmonizing classes, functions, tuples, and type parameters in Virgil III;terra: a multi-stage language for high-performance computing;SMAT: an input adaptive auto-tuner for sparse matrix-vector multiplication;when polyhedral transformations meet SIMD code generation;CLAP: recording local executions to reproduce concurrency failures;CONCURRIT: a domain specific language for reproducing concurrency bugs;compiler testing via a theory of sound optimisations in the C11/C++11 memory model;and almost-correct specifications: a modular semantic framework for assigning confidence to warnings.
the proceedings contain 56 papers. the topics discussed include: test-driven repair of data races in structured parallel programs;atomicity refinement for verified compilation;herding cats: modeling, simulation, testi...
ISBN:
(纸本)9781450327848
the proceedings contain 56 papers. the topics discussed include: test-driven repair of data races in structured parallel programs;atomicity refinement for verified compilation;herding cats: modeling, simulation, testing, and data-mining for weak memory;stochastic optimization of floating-point programs using tunable precision;a framework for enhancing data reuse via associative reordering;first-class runtime generation of high-performance types using exotypes;optimal inference of fields in row-polymorphic records;expressing and verifying probabilistic assertions;compositional solution space quantification for probabilistic software analysis;slicing probabilistic programs;adaptive, efficient parallel execution of parallel programs differentiation;globally precise-restartable execution of parallel programs;and accurate application progress analysis for large-scale parallel debugging.
the proceedings contain 47 papers. the topics discussed include: cache locality optimization for recursive programs;generalizations of the theory and deployment of triangular inequality for compiler-based strength red...
ISBN:
(纸本)9781450349888
the proceedings contain 47 papers. the topics discussed include: cache locality optimization for recursive programs;generalizations of the theory and deployment of triangular inequality for compiler-based strength reduction;DemoMatch: API discovery from demonstrations;similarity of binaries through re-optimization;BARRACUDA: binary-level analysis of runtime races in CUDA programs;bringing the web up to speed with WebAssembly;proactive and adaptive energy-aware programming with mixed typechecking;simple, fast, and safe manual memory management;efficient and precise points-to analysis: modeling the heap by merging equivalent automata;static deadlock detection for asynchronous c# programs;achieving high coverage for floating-point code via unconstrained programming;skeletal program enumeration for rigorous compiler testing;decomposition instead of self-composition for proving the absence of timing channels;automatic program inversion using symbolic transducers;rigorous analysis of software countermeasures against cache attacks;component-based synthesis of table consolidation and transformation tasks from examples;and network configuration synthesis with abstract topologies.
the proceedings contain 55 papers. the topics discussed include: BLeak: automatically debugging memory leaks in web applications;putting in all the stops: execution control for JavaScript;persistency for synchronizati...
ISBN:
(纸本)9781450356985
the proceedings contain 55 papers. the topics discussed include: BLeak: automatically debugging memory leaks in web applications;putting in all the stops: execution control for JavaScript;persistency for synchronization-free regions;write-rationing garbage collection for hybrid memories;mapping spiking neural networks onto a manycore neuromorphic architecture;static serializability analysis for causal consistency;Cuba: interprocedural context-unbounded analysis of concurrent programs;advanced automata-based algorithms for program termination checking;HHVM JIT: a profile-guided, region-based compiler for PHP and Hack;EffectiveSan: type and memory error detection using dynamically typed C/C++;calling-to-reference context translation via constraint-guided CFL-reachability;the semantics of transactions and weak memory in x86, power, ARM, and C++;MixT: a language for mixing consistency in geodistributed transactions;finding root causes of floating point error;to-many or to-one? all-in-one! efficient purely functional multi-maps with type-heterogeneous hash-tries;spatial: a language and compiler for application accelerators;enhancing computation-to-core assignment with physical location information;and SWOOP: so ware-hardware co-design for non-speculative, execute-ahead, in-order cores.
this paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune...
详细信息
ISBN:
(纸本)9781450334686
this paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune the search space. the algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.
暂无评论