-
Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models
Authors:
Antonio Paolillo,
Hernán Ponce-de-León,
Thomas Haas,
Diogo Behrens,
Rafael Chehab,
Ming Fu,
Roland Meyer
Abstract:
Developing concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory op…
▽ More
Developing concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory operations.
While WMM architectures are growing in popularity, identifying the necessary and sufficient barriers of complex synchronization primitives is notoriously difficult. Unfortunately, publications often consider barriers to be just implementation details and omit them. In this technical note, we report our efforts in verifying the correctness of the Compact NUMA-Aware (CNA) lock algorithm on WMMs. The CNA lock is of special interest because it has been proposed as a new slowpath for Linux qspinlock, the main spinlock in Linux. Besides determining a correct and efficient set of barriers for the original CNA algorithm on WMMs, we investigate the correctness of Linux qspinlock and the latest Linux CNA patch (v15) on the memory models LKMM, ARMv8, and Power. Surprisingly, we have found that Linux qspinlock and, consequently, Linux CNA are incorrect according to LKMM, but are still correct when compiled to ARMv8 or Power.
△ Less
Submitted 9 July, 2022; v1 submitted 30 November, 2021;
originally announced November 2021.
-
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Authors:
Kittiphon Phalakarn,
Toru Takisaka,
Thomas Haas,
Ichiro Hasuo
Abstract:
Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an efficient iterative method. However, BVI's performance is often impeded by costly end component (EC) computation that is needed to ensure convergence. Our contribution is a novel BVI algori…
▽ More
Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an efficient iterative method. However, BVI's performance is often impeded by costly end component (EC) computation that is needed to ensure convergence. Our contribution is a novel BVI algorithm that conducts, in addition to local propagation by the Bellman update that is typical of BVI, global propagation of upper bounds that is not hindered by ECs. To conduct global propagation in a computationally tractable manner, we construct a weighted graph and solve the widest path problem in it. Our experiments show the algorithm's performance advantage over the previous BVI algorithms that rely on EC computation.
△ Less
Submitted 18 September, 2020; v1 submitted 14 July, 2020;
originally announced July 2020.
-
Event Indexing Systems for Efficient Selection and Analysis of HERA Data
Authors:
L. A. T. Bauerdick,
Adrian Fox-Murphy,
Tobias Haas,
Stefan Stonjek,
Enrico Tassi
Abstract:
The design and implementation of two software systems introduced to improve the efficiency of offline analysis of event data taken with the ZEUS Detector at the HERA electron-proton collider at DESY are presented. Two different approaches were made, one using a set of event directories and the other using a tag database based on a commercial object-oriented database management system. These are…
▽ More
The design and implementation of two software systems introduced to improve the efficiency of offline analysis of event data taken with the ZEUS Detector at the HERA electron-proton collider at DESY are presented. Two different approaches were made, one using a set of event directories and the other using a tag database based on a commercial object-oriented database management system. These are described and compared. Both systems provide quick direct access to individual collision events in a sequential data store of several terabytes, and they both considerably improve the event analysis efficiency. In particular the tag database provides a very flexible selection mechanism and can dramatically reduce the computing time needed to extract small subsamples from the total event sample. Gains as large as a factor 20 have been obtained.
△ Less
Submitted 3 April, 2001;
originally announced April 2001.
