Below is LRM statements with highlighted points of concern or clarification: LRM states that These threads do not have to have consistent valuations for the local variables. But, example does show a consistent valuation for "x". According to those rules, the following example would pass the LRM requirements, but I think that it should not: sequence s6_MODIFIED_SLIGHTLY; int x,y; ((a ##1 (b, x = data, y = data1) ##3 c && x==10 ) // Thread1: or (d ##2 (`true, x = data) ##3 (e==x))) ##1 (x==data2); // Thread2: // legal because x is in the intersection endsequence Assume a==d==b==1 @ cycle 2, ##1 (b, x = data) causes x=data @ cycle2 for thread 1 (x==dataT1@cy2 // data thread1 @ cycle2) @ cycle 3, ##2 (`true, x = data) causes x=data @ cycle3. (x==dataT2@cy3) This is different than what thread1 expects later on. Thus, Thread 1 now has a different value of x , the one written at cycle 2, @ cycle 5 (c && x==10), we're expecting x to be 10, the value thought to have been captured at cycle 2 (i.e., dataT1@cy2), but x was re-evaluated at cycle 3 with the value dataT2@cy3. Thus, the rule "These threads do not have to have consistent valuations for the local variables." does not stand. In your LRM example, x is updated in both threads at cycle 2 with the same data if a==b==d==1. So here it works. The only way I see the statement "These threads do not have to have consistent valuations for the local variables". to be true is if there are 2 versions of the local variable x, one for each thread. I don't believe that this is the intent. Comments? Thanks for clarifying this. ------------------------------------------------LRM ------------------------ c) Each thread for an operand of an or that matches its operand sequence continues as a separate thread, carrying with it its own latest assignments to the local variables that flow out of the composite sequence. These threads do not have to have consistent valuations for the local variables. For example: sequence s5; int x,y; ((a ##1 (b, x = data, y = data1) ##1 c) or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2); // illegal because y is not in the intersection endsequence sequence s6; int x,y; ((a ##1 (b, x = data, y = data1) ##1 c) or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (x==data2); // legal because x is in the intersection endsequence -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Sun Mar 1 07:32:10 2009
This archive was generated by hypermail 2.1.8 : Sun Mar 01 2009 - 07:33:09 PST