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 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 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 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.
Application-level energy management is an important dimension of energy optimization. In this paper, we introduce ENT, a novel programminglanguage for enabling proactive and adaptive mode-based energy management at t...
详细信息
ISBN:
(纸本)9781450349888
Application-level energy management is an important dimension of energy optimization. In this paper, we introduce ENT, a novel programminglanguage for enabling proactive and adaptive mode-based energy management at the application level. the proactive design allows programmers to apply their application knowledge to energy management, by characterizing the energy behavior of different program fragments with modes. the adaptive design allows such characterization to be delayed until run time, useful for capturing dynamic program behavior dependent on program states, configuration settings, external battery levels, or CPU temperatures. the key insight is both proactiveness and adaptiveness can be unified under a type system combined with static typing and dynamic typing. ENT has been implemented as an extension to Java, and successfully ported to three energy-conscious platforms: an Intel-based laptop, a Raspberry Pi, and an Android phone. Evaluation shows ENT improves the programmability, debuggability, and energy efficiency of battery-aware and temperature-aware programs.
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 ...
详细信息
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.
暂无评论