Graphics Processing Units (GPUs) are the accelerator of choice for performance-critical applications, yet optimizing for performance requires mastery of the complex interactions between its memory architecture and its execution model. Existing static analysis tools for GPU kernels either identify performance bugs without quantifying costs or cannot handle thread-divergent control flow, leading to significant over-approximations. We present the first static relational-cost analysis for GPU warp-level parallelism that can give exact bounds even in the presence of thread divergence. Our analysis is general and flexible, as it is parametric on the resource metric (uncoalesced accesses, bank conflicts) and on the cost relation (=, ≤, ≥). We establish a soundness theorem for our technique, provide mechanized proofs in Rocq and implement our theory in a tool called Pico . In a reproducibility experiment, Pico produced the tightest bounds in every input, outperforming the state-of-the-art tool RaCUDA in 10 kernels (1.7× better), while RaCUDA produced 4 incorrect bounds and crashed on 2 kernels. In an experiment to measure the accuracy of Pico , we studied the impact of threaddivergence in control-flow in a dataset of 226 kernels. We found that at least 75.3% of conditionals and 85.4% of loops can be captured exactly, without introducing approximation.

Generating visualizations of Formal Languages and Automata (FLA) is often a laborious and error prone task. Existing tools either offer the ability to fully customize the appearance of the artifacts, or offer reusability and abstraction, but do not offer both at the same time. In this paper, we introduce a system called Gidayu for creating mathematical diagrams of automata, of their computations, and of their transformations. Many kinds of automata are supported: (non)deterministic finite automata, generalized nondeterministic finite automata, and (non)-deterministic pushdown automata. Gidayu fosters experimentation and rapid prototyping, as diagrams are generated automatically. The specification language includes directives to fine tune the presentation of each element; and, users can customize the visual notation used by our system. We discuss various parameters Gidayu offers to visualize diagrams and their importance in the instruction of FLA.