Re: JavaMemoryModel: Performing speculative writes ahead of loops that may not terminate

From: Bill Pugh (pugh@cs.umd.edu)
Date: Fri May 28 2004 - 13:44:52 EDT


I found a paper that discusses exactly the issue we are talking
about, in terms of control dependences.

        Bill

From:
        http://iss.cs.cornell.edu/Publications/Papers/PLDI1996.pdf

Podgurski and Clarke have introduced weak control
dependence [PC90] which is more appropriate than
the classical one for proving total correctness of programs.
   In this paper we call it loop control dependence because
we give an alternative definition of it based on the concept of
loop postdominance given below Figure 1 shows a program in
which classical and loop control dependence differ.
   Consider node k in the
CFG. In the classical notion k is control dependent on
g -> a. However to prove that k will be executed it is
necessary to prove that the loop a -> b -> a terminates.
Therefore in the context of proving total correctness of
programs it is more appropriate to make k loop control dependent
on the exit of the loop namely the
edge b -> k In programs without cycles the classical
and loop control dependence relations are identical.




[PC90] Andy Podgurski and Lori Clarke A formal
model of program dependences and its implications
for software testing debugging and maintenance
IEEE Transactions on Software Engineering,
Septmeber, 1990.

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:08 EDT