C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

I'm going to go ahead and add volatile support to KCC and I thought I
would get some feedback first.

My plan is to have a record of "observable behavior", which will
reflect all the external side effects, which include volatile
accesses.  After you run a program, you'd get something like

- write of 3227 to volatile at location 4
- write to stdout 'a'
- write of 691 to volatile at location 3
- read of 212 from volatile at location 4
- write of 'q' to ~/file.txt at offset 722
- read of 'y' from stdin
- write to stdout 'b'

Currently there is only an output cell with writes to standard out.  I
imagine the interleaving of these side effects are important, which is
why I'm suggesting this mechanism.

After I add this mechanism, I think most of the semantics can stay
unchanged.  Our semantics already acts as "abstract machine", so the
normal rules for nondeterminism will play out and we will record all
possible interleavings.

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?  I
imagine if someone wanted to use KCC to model a device driver, and the
volatiles changed in particular ways (e.g., a read from volatile loc
500 causes a write of 0 at volatile loc 501 behind the scenes), they
would want this mechanism.

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

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

-Chucky