Linear temporal logic (LTL) is widely used in industrial verification. LTL
formulae can be learned from traces. Scaling LTL formula learning is an open
problem. We implement the first GPU-based LTL learner using a novel form of
enumerative program synthesis. The learner is sound and complete. Our
benchmarks indicate that it handles traces at least 2048 times more numerous,
and on average at least 46 times faster than existing state-of-the-art
learners. This is achieved with, among others, novel branch-free LTL semantics
that has $O(\log n)$ time complexity, where $n$ is trace length, while previous
implementations are $O(n^2)$ or worse (assuming bitwise boolean operations and
shifts by powers of 2 have unit costs -- a realistic assumption on modern
processors).

使用 GPU 加速的基于枚举程序合成的 LTL 学习器在处理追踪数据时比现有技术要快 46 倍，并且可以处理比现有学习器多 2048 倍的追踪数据。

GPU 上的 LTL 学习

LTL learning on GPUs

Systems for serving inference requests on graph neural networks (GNN) must
combine low latency with high throughout, but they face irregular computation
due to skew in the number of sampled graph nodes and aggregated GNN features.
This makes it challenging to exploit GPUs effectively: using GPUs to sample
only a few graph nodes yields lower performance than CPU-based sampling; and
aggregating many features exhibits high data movement costs between GPUs and
CPUs. Therefore, current GNN serving systems use CPUs for graph sampling and
feature aggregation, limiting throughput.
We describe Quiver, a distributed GPU-based GNN serving system with
low-latency and high-throughput. Quiver's key idea is to exploit workload
metrics for predicting the irregular computation of GNN requests, and governing
the use of GPUs for graph sampling and feature aggregation: (1) for graph
sampling, Quiver calculates the probabilistic sampled graph size, a metric that
predicts the degree of parallelism in graph sampling. Quiver uses this metric
to assign sampling tasks to GPUs only when the performance gains surpass
CPU-based sampling; and (2) for feature aggregation, Quiver relies on the
feature access probability to decide which features to partition and replicate
across a distributed GPU NUMA topology. We show that Quiver achieves up to 35
times lower latency with an 8 times higher throughput compared to
state-of-the-art GNN approaches (DGL and PyG).

本研究讨论了基于图神经网络 (GNN) 的推理系统如何结合低延迟和高吞吐量，提出了一个分布式 GPU-based GNN 服务系统 靠工作负载指标预测 GNN 请求的不规则计算特征并管理 GPU 的使用，利用概率性采样来提高 GPU 的采样性能并指导特征聚合。通过与现有的 GNN 方法（DGL 和 PyG）的比较，Quiver 取得了高达 35 倍的低延迟和 8 倍的高吞吐量。

Quiver：支持工作负载感知的低延迟、高吞吐量 GNN 服务 GPU 支持

Quiver: Supporting GPUs for Low-Latency, High-Throughput GNN Serving  with Workload Awareness

Large-scale Bundle Adjustment (BA) requires massive memory and computation
resources which are difficult to be fulfilled by existing BA libraries. In this
paper, we propose MegBA, a GPU-based distributed BA library. MegBA can provide
massive aggregated memory by automatically partitioning large BA problems, and
assigning the solvers of sub-problems to parallel nodes. The parallel solvers
adopt distributed Precondition Conjugate Gradient and distributed Schur
Elimination, so that an effective solution, which can match the precision of
those computed by a single node, can be efficiently computed. To accelerate BA
computation, we implement end-to-end BA computation using high-performance
primitives available on commodity GPUs. MegBA exposes easy-to-use APIs that are
compatible with existing popular BA libraries. Experiments show that MegBA can
significantly outperform state-of-the-art BA libraries: Ceres (41.45$\times$),
RootBA (64.576$\times$) and DeepLM (6.769$\times$) in several large-scale BA
benchmarks. The code of MegBA is available at
this https URL

本文介绍了 MegBA—— 一种基于 GPU 的分布式大规模相机捆绑优化库，相较于目前现有的 Ceres、RootBA 和 DeepLM 等大规模相机捆绑优化库，它在一些大规模测试中表现出了更高的性能，可以提供巨大的聚合内存，可以自动划分大的 BA 问题，并将子问题的求解器分配到并行节点上。

MegBA：基于 GPU 的大规模束调整分布式库

MegBA: A GPU-Based Distributed Library for Large-Scale Bundle Adjustment

We introduce GRay, a massively parallel integrator designed to trace the
trajectories of billions of photons in a curved spacetime. This GPU-based
integrator employs the stream processing paradigm, is implemented in CUDA
C/C++, and runs on nVidia graphics cards. The peak performance of GRay using
single precision floating-point arithmetic on a single GPU exceeds 300 GFLOP
(or 1 nanosecond per photon per time step). For a realistic problem, where the
peak performance cannot be reached, GRay is two orders of magnitude faster than
existing CPU-based ray tracing codes. This performance enhancement allows more
effective searches of large parameter spaces when comparing theoretical
predictions of images, spectra, and lightcurves from the vicinities of compact
objects to observations. GRay can also perform on-the-fly ray tracing within
general relativistic magnetohydrodynamic algorithms that simulate accretion
flows around compact objects. Making use of this algorithm, we calculate the
properties of the shadows of Kerr black holes and the photon rings that
surround them. We also provide accurate fitting formulae of their dependencies
on black hole spin and observer inclination, which can be used to interpret
upcoming observations of the black holes at the center of the Milky Way, as
well as M87, with the Event Horizon Telescope.

介绍了一种基于 GPU 的并行积分器 GRay，它能够在弯曲空间中追踪数十亿光子的轨迹，并且其单 GPU 峰值性能超过 300 GFLOP，可用于黑洞精确成像，提供黑洞旋转和观察者倾角的精确拟合公式，可以用于解释事件视界望远镜的数据。