M.Sc Student | Ben-Shoshan Yaron |
---|---|
Subject | Labeling Fork-Join Task Graphs for Data Race Detection |
Department | Department of Electrical Engineering | Supervisor | Professor Yoram Moses |
Labeling schemes
are a central tool in dynamic data race detection. The
space complexity of the labels and the time complexity of comparing two labels
are a crucial factor in the time and space complexity of data race detection
methods that use that scheme. This work establishes two tight lower bounds on
the space complexity of a single label produced by a labeling method in a fork-join
run. Consider the following parameters of a fork-join structured run :
- The maximal nesting
level of fork-join pairs in r.
- The size of a maximal
set containing pairwise parallel blocks.
- The maximal number of
fork-join pairs within the same nesting level.
- The maximal number of
threads forked form a “fork” operation.
One lower bound,
which is given in term of the parameters N, S and L is , and
the other, which is given in term of T and L alone, is
. We also prove that methods exist whose space complexity meets the lower
bounds. The first method to be mentioned under this context is called DTN
(Decomposition Tree Numbering), and it matches the lower bound of
.
Instead of presenting a labeling method that meets the lower bound of
, we
present a general translation between labeling methods. Assume we are given a
labeling method with a space complexity of
. The result of translating this method is a new labeling method
with a space complexity of
. In this manner we conclude that the conversion of DTN meets
the
lower
bound. This work extends, generalizes, and unifies the analysis of labeling
schemes presented in a number of previous works.