Questions about atomic blocks

Jan 13, 2011 at 11:04 AM

Hi all,

I have a couple of questions about atomic blocks.

If I have an axiom of the form axiom(forall(state_t s; in_state(s, P()))); where P() is a simple predicate over the state (or spec(ispure bool P() reads(set_universe());)), does it also hold in middle-of-the-atomic-block states, or can it only be enforced in full_stop states? Is there a way of expressing that a state is full_stop at source VCC level?

Atomic blocks have changed, and I can't seem to figure out what kind of function, if any, can be called inside one of them. Currently, VCC does not complain when I call a pure spec function that reads the whole universe (such as P() above). Is this sound? Would it be sound to call a pure spec function that only reads objects that appear within the atomic block's header (and are thus closed by claim)?

I'll give more details about my specific applications if needed.


Jan 13, 2011 at 6:01 PM

I don’t think full_stop() is exposed. I guess we should have a mechanism for referencing arbitrary boogie functions from C header files, but currently the list of these functions is hardcoded in VCC translator sources.

It is sound to read anything you want in ghost code. As concurrency goes, you may imagine that each thread operators on a copy of the entire memory. The ghost code is allowed to read whatever it wants. It’s only the physical code, that can only read stuff we know will agree with other threads.