RE: [sv-ac] P1800-2009 Page 350 "threads do not have to have consistent valuations for the local variables"

Hi Ben:
 
Your s6_MODIFIED_SLIGHTLY example is legal per LRM.
 
The subevaluation of each operand of the "or" has its own copy of the
local variables.
 
The "or" subevaluations never "join".  That is why inconsistency of
values in separate threads is allowed.
In your example, the reference "x==data2" will be evaluated separately
for the two "or" subevaluations, and
each of those will use its own value stored in "x".  The two values
stored in "x" in these subevaluations may be
different.
 
I can see how you may be getting hung up on the fact that "x" is
assigned at the same cycle of evaluation in
each of s5 and s6.  These two examples are really illustrating the rules
about which variables may be referenced 
after an "or", not the rule that says that the values assigned on the
subevaluations do not have to be consistent.
 
J.H.

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Sunday, March 01, 2009 9:31 AM
To: sv-ac@eda.org
Subject: [sv-ac] P1800-2009 Page 350 "threads do not have to have
consistent valuations for the local variables"


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 <http://www.mailscanner.info/> , and is

believed to be clean. 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.