In order to achieve the highest possible performance, the ray traversal and intersection routines at the core of every high-performance ray tracer are usually hand-coded, heavily optimized, and implemented separately ...
详细信息
ISBN:
(纸本)9781450355247
In order to achieve the highest possible performance, the ray traversal and intersection routines at the core of every high-performance ray tracer are usually hand-coded, heavily optimized, and implemented separately for each hardware platform-even though they share most of their algorithmic core. the results are implementations that heavily mix algorithmic aspects with hardware and implementation details, making the code non-portable and difficult to change and maintain. In this paper, we present a new approach that offers the ability to define in a functional language a set of conceptual, high-level language abstractions that are optimized away by a special compiler in order to maximize performance. Using this abstraction mechanism we separate a generic ray traversal and intersection algorithm from its low-level aspects that are specific to the target hardware. We demonstrate that our code is not only significantly more flexible, simpler to write, and more concise but also that the compiled results perform as well as state-of-the-art implementations on any of the tested CPU and GPU platforms.
this paper introduces typy, a statically typed programminglanguage embedded by reflection into Python. typy features a fragmentary semantics, i.e. it delegates semantic control over each term, drawn from Python's...
详细信息
ISBN:
(纸本)9781450344463
this paper introduces typy, a statically typed programminglanguage embedded by reflection into Python. typy features a fragmentary semantics, i.e. it delegates semantic control over each term, drawn from Python's fixed concrete and abstract syntax, to some contextually relevant user-defined semantic fragment. the delegated fragment programmatically 1) typechecks the term (following a bidirectional protocol);and 2) assigns dynamic meaning to the term by computing a translation to Python. We argue that this design is expressive with examples of fragments that express the static and dynamic semantics of 1) functional records;2) labeled sums (with nested pattern matching a la ML);3) a variation on JavaScript's prototypal object system;and 4) typed foreign interfaces to Python and OpenCL. these semantic structures are, or would need to be, defined primitively in conventionally structured languages. We further argue that this design is compositionally well-behaved. It avoids the expression problem and the problems of grammar composition because the syntax is fixed. Moreover, programs are semantically stable under fragment composition (i.e. defining a new fragment will not change the meaning of existing program components.)
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbol...
详细信息
ISBN:
(纸本)9781450349888
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbolic execution. this paper turns the challenge of testing floating-point code into the opportunity of applying unconstrained programming-the mathematical solution for calculating function minimum points over the entire search space. Our core insight is to derive a representing function from the floating-point program, any of whose minimum points is a test input guaranteed to exercise a new branch of the tested program. this guarantee allows us to achieve high coverage of the floating-point program by repeatedly minimizing the representing function. We have realized this approach in a tool called CoverMe and conducted an extensive evaluation of it on Sun's C math library. Our evaluation results show that CoverMe achieves, on average, 90.8% branch coverage in 6.9 seconds, drastically outperforming our compared tools: (1) Random testing, (2) AFL, a highly optimized, robust fuzzer released by Google, and (3) Austin, a state-of-the-art coverage-based testing tool designed to support floating-point code.
Side-channel attack utilizes side-channel leakages to extract the secret in crypto systems. Various countermeasures for different algorithms and platforms have been proposed to protect crypto systems against such atta...
详细信息
ISBN:
(纸本)9781538622544
Side-channel attack utilizes side-channel leakages to extract the secret in crypto systems. Various countermeasures for different algorithms and platforms have been proposed to protect crypto systems against such attacks. Manual countermeasure design requires deep understanding of the target algorithm and implementation, and oftentimes is platform-specific and error-prone. In this paper, we propose the construction of threshold implementation (TI), a provably secure countermeasure against power attacks, as an automated compiler pass in the open LLVM (Low Level Virtual Machine) framework. Attack results show that the automatically generated TI designs are secure against power attacks. As our proposed scheme implements the countermeasure at the intermediate representation (IR) level, our method can be applied to any cipher software in any programminglanguage, and the generated implementations can be ported to different platforms and architectures.
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.
With advances of modern multi-core processors and accelerators, many modern applications are increasingly turning to compilerassisted parallel and vector programming models such as OpenMP, OpenCL, Halide, Python and T...
详细信息
We present FLIX, a declarative programminglanguage for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone fu...
详细信息
ISBN:
(纸本)9781450342612
We present FLIX, a declarative programminglanguage for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. this semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-naive evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. the declarative nature of FLIX clearly exposes the similarity between these two algorithms.
this paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees ...
详细信息
ISBN:
(纸本)9781450342612
this paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-driven synthesis algorithm for HDT transformations. Our central insight is to reduce the problem of synthesizing tree transformers to the synthesis of list transformations that are applied to the paths of the tree. the synthesis problem over lists is solved using a new algorithm that combines SMT solving and decision tree learning. We have implemented our technique in a system called HADES and show that HADES can automatically synthesize a variety of interesting transformations collected from online forums.
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Often...
详细信息
ISBN:
(纸本)9781450342612
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's paththrough the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.
We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for prog...
详细信息
ISBN:
(纸本)9781450342612
We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification-and hence synthesis-of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a newalgorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. the tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.
暂无评论