This project is read-only.

Meaning of assertions in concurrent context

The only place where actions of other threads of execution are taken into account is the beginning of the atomic statement, where the call to atomic_havoc() happens. Thus if you update the state inside of an atomic statement, this information is only lost after the beginning of the next atomic statement (or a function call, as it can contain an atomic statement). Because the only place where one can physically read memory is in the atomic block, the physical reads are modelled correctly, with interference from other threads. However we do not require that for assertions, i.e. they can access volatile memory also outside of atomic blocks. This has the not so nice side effect that:

assert(E);


and

bool tmp = E;
assert(tmp);


are somewhat different, in the sense that the second one will force you to use an atomic(...) block.

Thus the assertions are not really evaluated in the physical current state, but rather in the state that got out of the last atomic block amended with modification of the current thread. Thus VCC behaves as if each thread had it own copy of the entire memory and they only synced with the real memory at the beginning of atomic block. This allows us to reason about the programs sequentially, except for the atomic blocks.

This is actually useful in some situations, for example you can take a claim outside the atomic block, based on the state you created in the atomic block.

Last edited Nov 13, 2009 at 1:02 PM by stobies, version 2

Comments

No comments yet.