The Effect Race in Fine-Grained Concurrency

TL;DR

This paper introduces effect race and effect equivalence relations to better analyze fine-grained concurrency, providing formal foundations, theorems, and experimental validation for understanding internal execution steps and their impact on histories.

Contribution

It defines effect race and effect equivalence relations, proves key theorems linking them to histories, and formalizes linearization points, advancing the analysis of fine-grained concurrent executions.

Findings

Effect race relation accurately captures internal execution steps.

Theorems relate effect race to chaotic histories.

Experimental results confirm the effectiveness of the proposed definitions.

Abstract

Most existed work require knowledge about the effect of program instructions (or statements) to analyze and verify algorithms. In this paper, by revealing some findings on executions of object programs, we define two basic concepts -- effect equivalence relation and effect race relation. Further, we show three effect theorems about the race and histories. The core result is that the effect race relation is the accurate relation to capture the internal steps, of which precedence orders are the reason to cause chaotic histories. In addition, the concept -- linearization points -- widely used in the object verification, is defined formally as the typical effect race relation. These results provide a clear basis for analyzing intricate fine-grained executions. We conduct a lot of experiments on real object algorithms to show the accuracy and efficiency of these definitions in practice. A simple quantitative analysis method for these algorithms is also proposed.