[sv-ec] RE: determinism of fork/join_none processes

I filed this as Mantis 4176.

Shalom

From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of Bresticker, Shalom
Sent: Wednesday, May 23, 2012 14:16
To: Steven Sharp; Rich, Dave; sv-ec@eda.org
Subject: [sv-ec] RE: determinism of fork/join_none processes

I looked at this a little. As far as I can see, Mantis 652 was the result of a ballot comment on SV-2005. The proposal appearing in the Mantis Additional Information field was apparently only a proposal and the comment deletion did not appear in the final proposal that was approved by the Working Group and implemented in the Recirculation Ballot.

Regards,
Shalom

From: owner-sv-ec@eda.org<mailto:owner-sv-ec@eda.org> [mailto:owner-sv-ec@eda.org]<mailto:[mailto:owner-sv-ec@eda.org]> On Behalf Of Steven Sharp
Sent: Tuesday, May 22, 2012 22:25
To: Rich, Dave; sv-ec@eda.org<mailto:sv-ec@eda.org>
Subject: [sv-ec] RE: determinism of fork/join_none processes

Your understanding matches mine. The value of m may be unexpected and not useful, but is not undetermined.

From: owner-sv-ec@eda.org<mailto:owner-sv-ec@eda.org> [mailto:owner-sv-ec@eda.org]<mailto:[mailto:owner-sv-ec@eda.org]> On Behalf Of Rich, Dave
Sent: Tuesday, May 22, 2012 2:39 PM
To: sv-ec@eda.org<mailto:sv-ec@eda.org>
Subject: [sv-ec] determinism of fork/join_none processes

This is from: http://verificationguild.com/modules.php?name=Forums&file=viewtopic&p=20425#20425

In this example from 9.3.2

initial
    for( int j = 1; j <= 3; ++j )
      fork
         automatic int k = j; // local copy, k, for each value of j
         #k $write( "%0d", k );
         begin
             automatic int m = j; // the value of m is undetermined
             ...
         end
      join_none

I think the value for all variables called m is deterministically 4 because the for loop must end, leaving j at 4 before any process can start. Mantis 652<http://www.eda.org/svdb/view.php?id=652> suggested that comment be deleted, but it was not. Am I missing something?

Dave Rich
Verification Technologist
Mentor Graphics Corporation
[Description: Description: Twitter-32]<http://www.twitter.com/dave_59>[Description: Description: Technorati-32]<http://go.mentor.com/drich>

--
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<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.
--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.