RE: [sv-bc] Mantis 1345: 10.4: "illegal" unique if/case issues

From: Steven Sharp <sharp_at_.....>
Date: Tue Feb 21 2006 - 12:22:05 PST
>From: "Bresticker, Shalom" <shalom.bresticker@intel.com>

>The LRM says that if it finds an 'illegal' interleaving, it shall issue
>a warning unless it also finds a 'legal' interleaving. That is, if it
>finds both a 'legal' and an 'illegal' interleaving, it is not required
>to issue a warning.

In practice, when a simulator finds an 'illegal' interleaving, it will
issue a warning.  It won't go searching for a 'legal' one.  If it
happens to find a 'legal' one on its only try, it won't issue a warning.
This text allows that.

The text is confusing because it is trying not to specify exactly how
the implementation must interleave, but just the constraints on the
results.  But it specifies those constraints in terms of hypothetical
ways of interleaving.  The constraints come down to

1. If all interleavings are 'illegal', the tool shall issue a warning.
   In practice, the one interleaving it implements will end up being
   'illegal' in this case, so it issues a warning.

2. If all interleavings are 'legal', the tool shall not issue a warning.
   In practice, the one interleaving it implements will end up being
   'legal' in this case, so it doesn't issue a warning.

3. If there are both 'legal' and 'illegal' interleavings, the tool may
   or may not issue a warning.  In practice, this will depend on whether
   the one interleaving it implements happens to be 'legal' or 'illegal'.
   But since the LRM does not want to specify the interleaving, it has
   to allow for any possible interleaving.  That includes even the worst
   cases of actually trying all combinations and warning if any is bad,
   or not warning if any is OK.  That is the most extreme possible case,
   and the LRM is trying to say that even that is allowed.  It would have
   been simpler if the LRM had just used something like the first sentence
   in this paragraph.


>If it finds (by chance or by intention) an 'illegal' ordering, why
>should it not be required to issue a warning even if it happens to find
>another ordering which is 'legal'?

All the LRM can specify is the externally visible behavior of a tool.
Any tool that meets that must be considered compliant.  How can you
make this a requirement when there is no way to look at the behavior
of a tool and determine whether it has complied with it?  If it can
pick any order it wants any time it evaluates, how can you prove that
it didn't happen to pick the 'legal' ordering the first time?  If two
implementations get identical results, how can you claim that one is
compliant but the other isn't, just because it used a different internal
algorithm to get those results?

Steven Sharp
sharp@cadence.com
Received on Tue Feb 21 12:22:21 2006

This archive was generated by hypermail 2.1.8 : Tue Feb 21 2006 - 12:23:39 PST