English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

As Graphics Processing Units (GPUs) have gained in capability and GPUdevelopment environments have matured, developers are increasingly turning tothe GPU to off-load the main host CPU of numerically-intensive, parallelizablecomputations. Modern GPUs feature hundreds of cores, and offer programmingniceties such as double-precision floating point, and even limited recursion.This shift from CPU to GPU, however, raises the question: how do we know thatthese new GPU-based algorithms are correct?  In order to explore this new verification frontier, we formalized aparallelizable all-pairs shortest path (APSP) algorithm for weighted graphs,originally coded in NVIDIA's CUDA language, in ACL2. The ACL2 specification iswritten using a single-threaded object (stobj) and tail recursion, as thestobj/tail recursion combination yields the most straightforward translationfrom imperative programming languages, as well as efficient, scalableexecutable specifications within ACL2 itself. The ACL2 version of the APSPalgorithm can process millions of vertices and edges with little to no garbagegeneration, and executes at one-sixth the speed of a host-based version of APSPcoded in C- a very respectable result for a theorem prover.  In addition to formalizing the APSP algorithm (which uses Dijkstra's shortestpath algorithm at its core), we have also provided capability that the originalAPSP code lacked, namely shortest path recovery. Path recovery is accomplishedusing a secondary ACL2 stobj implementing a LIFO stack, which is provencorrect. To conclude the experiment, we ported the ACL2 version of the APSPkernels back to C, resulting in a less than 5% slowdown, and also performed apartial back-port to CUDA, which, surprisingly, yielded a slight performanceincrease.

ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2