Global analysis of C concurrency in high-level synthesis

When mapping C programs to hardware, high-level synthesis (HLS) tools reorder independent instructions, aiming to obtain a schedule that requires as few clock cycles as possible. However, when synthesising multi-threaded C programs, reordering opportunities are limited by the presence ofatomicoperations(‘atomics’), the fundamental concurrency primitivesin C. Existing HLS tools analyse and schedule each thread inisolation. In this article, we argue that thread-local analysisis conservative, especially since HLS compilers have access to the entire program. Hence, we propose a global analysis that exploits information about memory accesses by all threads when scheduling each thread. Implemented in the Leg Up HLS tool, our analysis is sensitive to sequentially-consistent (SC) and weak atomics, and supports loop pipelining. Since the semantics of C atomics is complicated, we formally verify that our analysis correctly implements the C memory model using the Alloy modelchecker. Compared to thread-local analysis, our global analysis achieves a 2.3× average speedup on a set of lock-free datastructures and data-flow patterns. We also apply our analysis to a larger application: a lock-free, streamed, and load-balanced implementation of Google’s PageRank, where we see a 1.3× average speedup compared to thread-local analysis