C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

Comments below:

On Thu, Jun 23, 2011 at 1:47 PM, Derek M Jones 
<derek AT knosof.co.uk>
 wrote:
> Chucky,
>
>> I'm going to go ahead and add volatile support to KCC and I thought I
>> would get some feedback first.
>
> This could be real hard.  What output does the following produce?
>
> volatile int x;
> int y = 0;
>
> while (x != 99)
>    y++;
>
> printf("%d", y);

- read of 'unknown' from memory location [wherever x is]
- read of 'unknown' from memory location [wherever x is]
...
- read of 'unknown' from memory location [wherever x is]
- write of "99" to stdout

I think for the first phase of adding volatiles, all reads would
return 'unknown'.  This may suggest dealing with actual values makes
more sense, like your "file of values" idea below.  Whatever I do
first should be simple since John's idea of hooking it up to some
other code/simulation would be necessary in the long run.


>> Also, is it undefined to have unsequenced reads from two different
>> volatiles?  E.g.,
>> volatile int v1 = 0, v2 = 0;
>> v1 + v2;
>
> Subtraction is more of a problem if they both map to the same input
> device.

Why is subtraction more of a problem?  Simply because you could get
two different behaviors?  Does that mean v1 + v2 is a problem, but
only a little problem?

In fact, wouldn't v1 - v1 be undefined?  Let's say the first read from
v1 will be 5, but the read causes the value ot be changed to 4.
Evaluating R to L results in -1, but evaluating L to R results in 1.
Is this defined nondeterminism, or is it undefined?  If this is
undefined, then I imagine v1 + v1 would be as well.

It looks like you have an example on digital page 279 under sentence 194.
int a;
volatile int b, c;
void f(void)  {
    int t;
    a = b + c;
    a = ((t = b), t + c);
}
I assume if you have this example, it isn't undefined; I just don't
understand how.

>> I'm wondering since there is that sentence "What constitutes an access
>> to an object that has volatile-qualified type is
>> implementation-defined."    I've also heard casually that "a volatile
>> access can be thought of as a potential access anywhere in memory".  I
>> suppose it means "anywhere in volatile memory".  Is this correct?
>
> Sentence 1488.

I can't believe bit fields can be volatile...  I guess it doesn't
matter since people who use volatiles are probably doing something
that isn't portable anyway.


>
> --
> Derek M. Jones                         tel: +44 (0) 1252 520 667
> Knowledge Software Ltd                 
> mailto:derek AT knosof.co.uk
> Source code analysis                   http://www.knosof.co.uk
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>