I'm struggling to prove Lemma 3 and Lemma 4 from an article about parallel version of push-relabel algorithm: A lock-free multi-threaded algorithm for the maximum flow problem.

Lemma 3. Any trace of two push and/or lift operations is equivalent to either a stage-clean trace or a stage-stepping trace.


Lemma 4. For any trace of three or more push and/or lift operations, there exists an equivalent trace consisting of a sequence of non-overlapping traces, each of which is either stage-clean or stage-stepping.

Pdf version of the article can be found here

  • $\begingroup$ "The proof of Lemma 3 is straightforward. We simply need to enumerate all the possible pairs of operations that might be interleaved and derive an equivalent trace (either stage-clean or stage-stepping) for each such pair.", reads the article. Have you tried enumerating all the possible pairs of operations? $\endgroup$ – John L. Jun 23 '19 at 18:35
  • $\begingroup$ The way I see it: we have a list of instructions that are executed in parallel, the number of possible traces (the author uses the term trace to define the order in which instructions from the threads are executed in real time) is pretty big and impractical to be analyzed one by one. I don't understand how to approach the problem by looking at operations. So lets take (push, push) pair, how can I prove that all the possible traces of two pushes on two different threads are equivalent (have the same consequence) to either a stage-clean trace or a stage-stepping trace? What am I missing? $\endgroup$ – byznass Jun 24 '19 at 18:40
  • $\begingroup$ You may write a computer program that lists all possible cases. $\endgroup$ – John L. Jun 24 '19 at 20:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.