Inter-procedural data-flow analyses are slow. We parallelize these predicate propagation fixpoint algorithms efficiently on a GPU. Our approach is (mostly) synchronization free even though the processed graphs in gene...
详细信息
ISBN:
(纸本)9781450362771
Inter-procedural data-flow analyses are slow. We parallelize these predicate propagation fixpoint algorithms efficiently on a GPU. Our approach is (mostly) synchronization free even though the processed graphs in general are cyclic and have nodes with fan-in and fan-out degrees above 1. We detect and fix any data races that occur while propagating predicates in a SIMD fashion. Additionally, we solve the parallel termination problem by means of heuristics. The GPU-codes of five data-flow analyses are up to 89.8 times faster than their sequential LLVM variants. Offloading the analyses to the GPU saves up to 26.5% of the total compilation time.
Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated ...
详细信息
Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated within a few components, and it is desirable to reuse as much as possible previous analysis results. This has been achieved to date through incremental global analysis fixpoint algorithms that achieve cost reductions at fine levels of granularity, such as changes in program lines. However, these fine-grained techniques are neither directly applicable to modular programs nor are they designed to take advantage of modular structures. This paper describes, implements, and evaluates an algorithm that performs efficient context-sensitive analysis incrementally on modular partitions of programs. The experimental results show that the proposed modular algorithm shows significant improvements, in both time and memory consumption, when compared to existing non-modular, fine-grain incremental analysis techniques. Furthermore, thanks to the proposed intermodular propagation of analysis information, our algorithm also outperforms traditional modular analysis even when analyzing from scratch.
We present an algorithm for computing the uniquely determined least fixpoints of self-maps on (with ) that are point-wise maximums of finitely many monotone and order-concave self-maps. This natural problem occurs in ...
详细信息
We present an algorithm for computing the uniquely determined least fixpoints of self-maps on (with ) that are point-wise maximums of finitely many monotone and order-concave self-maps. This natural problem occurs in the context of systems analysis and verification. As an example application we discuss how our method can be used to compute template-based quadratic invariants for linear systems with guards. The focus of this article, however, lies on the discussion of the underlying theory and the properties of the algorithm itself.
暂无评论