Search arXiv⌕ Search

arXiv · 2009.03846

On Architecture to Architecture Mapping for Concurrency

Abstract

Mapping programs from one architecture to another plays a key role in technologies such as binary translation, decompilation, emulation, virtualization, and application migration. Although multicore architectures are ubiquitous, the state-of-the-art translation tools do not handle concurrency primitives correctly. Doing so is rather challenging because of the subtle differences in the concurrency models between architectures. In response, we address various aspects of the challenge. First, we develop correct and efficient translations between the concurrency models of two mainstream architecture families: x86 and ARM (versions 7 and 8). We develop direct mappings between x86 and ARMv8 and ARMv7, and fence elimination algorithms to eliminate redundant fences after direct mapping. Although our mapping utilizes ARMv8 as an intermediate model for mapping between x86 and ARMv7, we argue that it should not be used as an intermediate model in a decompiler because it disallows common compiler transformations. Second, we propose and implement a technique for inserting memory fences for safely migrating programs between different architectures. Our technique checks robustness against x86 and ARM, and inserts fences upon robustness violations. Our experiments demonstrate that in most of the programs both our techniques introduce significantly fewer fences compared to naive schemes for porting applications across these architectures.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Soham Chakraborty. 2020-09-08. On Architecture to Architecture Mapping for Concurrency. https://arxiv.org/abs/2009.03846

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators

To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code to operations in specialized hardware accelerators. However, most of these frameworks do not verify these mappings down to the hardware level, potentially resulting in functional mismatches. In this paper we propose BOLT, the first framework for formally verifying the correctness of compiler-to-accelerator mappings for coarse-grained intrinsics in ML accelerators, with respect to a formal hardware semantics. BOLT does not require additional information from the compiler, and verifies the functional equivalence of the application code and the code for the mapped hardware accelerator intrinsic, including handling of complex loop nests and tensor data layouts in hardware. It effectively utilizes a pattern of *aligning* software loops with the hardware, followed by *relating* corresponding data layouts, to enable verification using well-aligned product programs. To support these steps, we propose two custom templates --- the sync-skeleton and the layout-sketch --- to guide users in aligning loops and specifying data layout relationships, respectively. We have developed a proof-of-concept prototype for BOLT and use it to successfully verify the correctness of several complex mappings for two recent open-source ML accelerators.

cs.PL↗

Schedules Are Solvable Symbols: Tuning-Free Compilation of Tile Programs on Dataflow Architectures

Modern AI and HPC accelerators increasingly expose dataflow features: software-visible mechanisms for data movement and overlap, such as inter-core communication through the on-chip network and intra-core asynchronous pipelining. These features shift scheduling responsibility from hardware to the compiler, and because placement, movement, and synchronization become software-visible, they also make the performance of static schedules predictable. Yet high performance on such hardware still relies on vendor-engineered kernel libraries or profile-based auto-tuning, whose embedded expert knowledge transfers poorly across architectures and algorithms. We present Loom, a tuning-free symbolic compiler framework for tile-based SPMD programs on spatial dataflow architectures. The central idea is to treat tile-based SPMD compilation as a hardware-explicit static optimization problem. Loom enumerates discrete spatial-mapping and communication candidates while keeping value parameters, such as tiling factors and pipeline knobs, symbolic within each candidate. From an explicit hardware description, it derives symbolic legality constraints and latency expressions, formulates one CP-SAT problem per schedule candidate, and jointly solves inter-core dataflow, intra-core asynchronous scheduling, and block sizes at compile time. On two Tenstorrent generations, Wormhole and Blackhole, Loom matches or exceeds the vendor-optimized TTNN library on GEMM, Flash Attention, and Flash Decode, out of the box and without per-shape profiling or profile-based platform-specific schedule tuning. These results suggest that hardware-derived symbolic compilation provides a retargetable alternative to profiling-based tuning for spatial dataflow architectures while remaining interpretable by keeping optimization decisions traceable to source-level symbols.

cs.PL↗

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited insight into models' step-level formal reasoning. Evaluating this capability separately enables finer-grained diagnosis of model limitations than theorem-level evaluation alone. To fill this evaluation gap, we introduce ProofGap, a fine-grained benchmark for step-level formal reasoning. ProofGap is constructed through a natural-language proof-processing pipeline that decomposes each reasoning step into one or more aligned proof gaps. Applying this pipeline to natural-language solutions to 3,015 exercises in B. P. Demidovich's Problems in Mathematical Analysis yields 26,116 gaps. The benchmark focuses on mathematical analysis, a domain that remains challenging for current models. By supplying the local context and target explicitly, gap completion isolates local formal proof construction from end-to-end proof composition, enabling more precise localization of model failures. Natural-language solutions serve as the provenance of these obligations, while the benchmark task itself starts from an already formalized local context and goal. Beyond benchmarking, the same pipeline may support future proof-verification systems, provided that semantic translation and sequential proof composition are handled reliably.

cs.PL↗