C Semantics in K Framework

[John Regehr <regehr AT cs.utah.edu>]

Your plan sounds solid.

> unchanged.  Our semantics already acts as "abstract machine", so the
> normal rules for nondeterminism will play out and we will record all
> possible interleavings.

Sounds exactly right.

> One thing I'm worried about is that this doesn't address the fact that
> volatile variables can change "behind the scenes".  Would we need a
> way to allow the user to specify how volatiles might change?

Yes, though initially I'd suggest you just go with the model where these 
locations do not change.

In the long run I think you need to shell out to arbitrary code (device 
simulator or whatever) to determine the next value read.  Also you need 
to call the external code on writes, since these can trigger device 
state transitions too.

> Also, is it undefined to have unsequenced reads from two different
> volatiles?  E.g.,
> volatile int v1 = 0, v2 = 0;
> v1 + v2;

Perfectly well defined, as far as I know.

> I'm wondering since there is that sentence "What constitutes an access
> to an object that has volatile-qualified type is
> implementation-defined."

Yes that sentence caused Eric and me much angst.  I suggest you just go 
and look at what some implementations define this to be.

My understanding is that this language is in the standard to give 
implementors an escape hatch for example on architectures that have 
large minimum memory access sizes that might force a read from volatile 
A to also read from nearby volatile B, even when the abstract machine 
would not have read B.

>    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?
> Should I worry about this?

I think you should not take this literally, and not worry about it.  It 
doesn't even really make sense that I can see.

John