Showing 1–3 of 3 results for author: Behrens, D

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: Develo** 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 Develo** 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.

VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)

Authors: Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis

Abstract: This technical report contains material accompanying our work with same title published at ASPLOS'21. We start in Sec. 1 with a detailed presentation of the core innovation of this work, Await Model Checking (AMC). The correctness proofs of AMC can be found in Sec. 2. Next, we discuss three study cases in Sec. 3, presenting bugs found and challenges encountered when applying VSync to existing code… ▽ More This technical report contains material accompanying our work with same title published at ASPLOS'21. We start in Sec. 1 with a detailed presentation of the core innovation of this work, Await Model Checking (AMC). The correctness proofs of AMC can be found in Sec. 2. Next, we discuss three study cases in Sec. 3, presenting bugs found and challenges encountered when applying VSync to existing code bases. Finally, in Sec. 4 we describe the setup details of our evaluation and report further experimental results. △ Less

Submitted 12 February, 2021; originally announced February 2021.

Job Selection in a Network of Autonomous UAVs for Delivery of Goods

Authors: Pasquale Grippa, Doris A. Behrens, Christian Bettstetter, Friederike Wall

Abstract: This article analyzes two classes of job selection policies that control how a network of autonomous aerial vehicles delivers goods from depots to customers. Customer requests (jobs) occur according to a spatio-temporal stochastic process not known by the system. If job selection uses a policy in which the first job (FJ) is served first, the system may collapse to instability by removing just one… ▽ More This article analyzes two classes of job selection policies that control how a network of autonomous aerial vehicles delivers goods from depots to customers. Customer requests (jobs) occur according to a spatio-temporal stochastic process not known by the system. If job selection uses a policy in which the first job (FJ) is served first, the system may collapse to instability by removing just one vehicle. Policies that serve the nearest job (NJ) first show such threshold behavior only in some settings and can be implemented in a distributed manner. The timing of job selection has significant impact on delivery time and stability for NJ while it has no impact for FJ. Based on these findings we introduce a methodological approach for decision-making support to set up and operate such a system, taking into account the trade-off between monetary cost and service quality. In particular, we compute a lower bound for the infrastructure expenditure required to achieve a certain expected delivery time. The approach includes three time horizons: long-term decisions on the number of depots to deploy in the service area, mid-term decisions on the number of vehicles to use, and short-term decisions on the policy to operate the vehicles. △ Less

Submitted 26 May, 2017; v1 submitted 14 April, 2016; originally announced April 2016.