Lithium-ion batteries demonstrate two kinds of non-linear behavior: rate capacity effects and recovery effects. These effects are dual to each other and show the dependency between the power consumption profile and ba...
详细信息
ISBN:
(纸本)9781728133737
Lithium-ion batteries demonstrate two kinds of non-linear behavior: rate capacity effects and recovery effects. These effects are dual to each other and show the dependency between the power consumption profile and battery utilization, i.e., the fraction of the battery charge that can be withdrawn. We propose a static analysis for computing the lower bound of battery utilization based on the Kinetic Battery Model (KiBaM), an analytical model capturing nonlinear battery behavior. Our method does not depend on the battery charge level and can be composed with other flow analyses and model checking techniques for improved accuracy. We propose a modification to the worklist algorithm for totally ordered semilattices with computable fixed-points of transfer functions, which is necessary for computing our analysis. We prove the termination and correctness of our algorithm and introduce a nonforgetful extension to it for speeding up convergence. We implement the battery-utilization in the software verification tool CPAchecker by encoding the analysis together with our algorithm in a relaxed instance of a configurable program analysis (CPA). Our experiments show that the convergence speed up is sometimes achievable, but does not necessarily lead to a performance improvement.
Many popular vetting tools for Android applications use static code analysis techniques. In particular, Interprocedural Data-Flow Graph (IDFG) construction is the computation at the core of Android static data-flow an...
详细信息
ISBN:
(纸本)9781728168760
Many popular vetting tools for Android applications use static code analysis techniques. In particular, Interprocedural Data-Flow Graph (IDFG) construction is the computation at the core of Android static data-flow analysis and consumes most of the analysis time. Many analysis tools use a worklist algorithm, an iterative fixed-point approach, to construct the IDFG. In this paper, we observe that a straightforward GPU parallelization of the worklist algorithm leads to significant underutilization of the GPU resources. We identify four performance bottlenecks, namely, frequent dynamic memory allocations, high branch divergence, workload imbalance, and irregular memory access patterns. Accordingly, we propose GDroid, a GPU-based worklist algorithm implementation with multiple fine-grained optimizations tailored to common characteristics of Android applications. The optimizations considered are: matrix-based data structure, memory access-based node grouping, and worklist merging. Our experimental evaluation, performed on 1000 Android applications, shows that the proposed optimizations are beneficial to performance, and GDroid can achieve up to 128X speedups against a plain GPU implementation.
暂无评论