Hi Everyone,

I am currently struggling with understanding the semantics of atomic_read. I have the following program:

#include <vcc.h>

volatile unsigned int value;
_(ghost unsigned int last_value;)

unsigned int bar(void)
_(writes &last_value,\gemb(&value))
_(maintains \wrapped(\gemb(&value)))
_(ensures \result==value)
_(ensures value==last_value)
{
    _(atomic \gemb(&value)){
         value=0;
         _(bump_volatile_version \gemb(&value))
     }
    
    while(_(atomic_read \gemb(&value)) value==0)
    _(invariant \wrapped(\gemb(&value)))
    {}

    _(ghost last_value=value;)
    return _(atomic_read \gemb(&value)) value;
}

So far, I understand that I can use volatile variables as shared memory, e.g. between different threads or between a program and memory-mapped inputs and outputs. I just have to make sure those variables stay closed and I read and write them with the help of atomic and atomic_read. I would expect that volatile variables have a fresh value after every atomic block, function call and function entry. In th program above, I set value to zero and then use a busy-waiting while-loop to wait until some other thread or the environment changes the variable. I use atomic_read to obtain a fresh value for every iteration. This works as expected, as I can reach the end of the loop.

Then, I save the value of the volatile to a ghost variable, obtain another fresh value via atomic_read, and return this value.

Now I am somewhat puzzled that VCC can prove the postconditions \result == value == last_value. I would expect that value and last_value are different.

Can you explain what I did wrong? Is this perhaps related to the ownership of value and I should go for \closed only instead of \wrapped in the precondition and the loop invariant?

Best regards,

Daniel

<EDIT>

PS: I am currently using vcc /version
Microsoft Research Vcc Version 2.1.41221.1
Microsoft Research Boogie Version 2.1.31207.0
Microsoft Research Z3 Version Z3 version 3.2

</EDIT>

Can no one help me or are my questions that basic?

I am not completely up to date on atomic_read, but this looks like it is more likely related to the fact that you are using a global volatile variable of primitive type.

For example, take a look at the following, where the volatile global is stuck into a global structure, but nothing else changes.

#include <vcc.h> 

struct {
  volatile unsigned int value;
} val;
_(ghost unsigned int last_value;)

unsigned int bar(void)
_(writes &last_value)
_(maintains \wrapped(&val))
_(ensures \result==val.value)
_(ensures val.value==last_value)
{
  _(atomic &val) val.value=0;
  while(_(atomic_read &val) val.value==0)
  _(invariant \wrapped(&val))
  {}

  _(ghost last_value=val.value;)
  return _(atomic_read &val) val.value;
}

This gives you the expected behaviour. If you want to get back the behaviour you get with your code, you will need to add an invariant to the type of val, stating that the owner needs to approve all changes made to value (_(invariant \approves(\this->\owner,value))), which essentially means, when the owner is the thread (which is the case here), that no other thread can modify the volatile variable (which therefore essentially behaves sequentially).

I suspect that the global embedding structure does have such an approval invariant for all global volatiles.

My rule of thumb is "if VCC complains that there's a missing \bump_volatile_version() then the variable behaves sequentially".

Apologies if this is unclear: I am only inferring the inner workings of VCC from its superficial behaviour (which is also why I failed to comment earlier). Maybe someone with a bit more insight will come help?

Cheers,
Francois

PS: I am not aware of any way to prevent VCC from generating an approval invariant for volatile globals. However, you can make this approval invariant a bit less restrictive by not having the \wrapped(\gemb(&value)) pre-condition, but instead having another structure (a lock?) that owns the object. The owner approval invariant will then simply ensure that all changes to value made whilst its owner remains closed respect the owner's two-state invariant. Message me or reply to this if you want an example of this.

Thank you Francois,

this helps. Perhaps someone can confirm that embedded structs always contain approval invariants? If so, it is somewhat unfortunate, because it would require actual changes to the code for verification.

I will also give the idea with the additional struct a try and report back.

Best Regards,

Daniel

Hi Daniel,

(Sorry for the slow response.)

We do indeed tacitly owner-approve volatile globals. The reason for this is that without some invariant governing changes to the global, we could know nothing about its value, making it useless for programming. For a global primitive, there is nowhere to put such an invariant, so the only reasonable option is to put it in the owner.

Note that this follows a general VCC principal of programming with concurrent objects: if you have a general-purpose concurrent object (such as a concurrent set), it is useless without further invariants constraining how its behavior is tied to other parts of the system. So when you build such an object, you always make its abstract value approved by its owner (or, alternatively, approved by some object explicitly engineered into the abstact spec, e.g. the "operation" object currently partying on it). For a global volatile primitive, there is no place to define an alternate approver, so it must be approved by its owner. Since there is no place to put this approval invariant yourself, we build it in. Note that this does not introduce unsoundness, in the sense that if you were to add to your system another function (possibly modelling a piece of hardware) concurrently partying on the variable without owning it, that function would fail to verify.

But don't be alarmed; this tacit approval does not force you to change your code to verify it. (Indeed, it is precisely to avoid having to rewrite code that this tacit approval is in place.) Instead of having the volatile owned by the thread operating on it, you introduce a new ghost object as its owner, and give this ghost object an invariant that suitably constrains the bahvior of the global. If it doesn't constrain the variable, you get the same effect as if the variable wasn't approved at all (except for some extra annotation overhead).

Hope this helps,

ernie

Ernie, thank you for your reply. As far as I understand it now, going with a ghost struct as owner of the global volatile primitive would be a way.

Essentially, the example would then look like:

volatile unsigned int value;
_(ghost unsigned int last_value;)

_(ghost _(volatile_owns) _(claimable) struct _A {
    int dummy;
    _(invariant \mine(\gemb(&value)))
} A;)

unsigned int bar(_(ghost \claim c))
_(always c , (&A)->\closed)
_(writes &last_value)
_(ensures \result==value)
_(ensures value==last_value)
{
    _(atomic c,\gemb(&value)){
        value=0;
    }
          
    while(_(atomic_read c,\gemb(&value)) value==0)
    {}
    
    _(ghost last_value=value;)
    return _(atomic_read c,\gemb(&value)) value;
}

Indeed, VCC now reports as expected that the postcondition value==last_value does not hold.

My original intend was to simulate environmental changes in programs for memory-mapped systems through another thread. Am I right to assume that this cannot be expressed correctly without using claims? I am asking because claims force changes to lecacy code that are visible to developers (e.g. the passing of claims to methods).

Best regards,
Daniel

I'm not sure whether ghost arguments count as "changing" legacy code (i.e., it doesn't show up as a change by the time it gets to the compiler). However, for functions that don't modify the claims they use (in particular, claiming them), you can in principle replace the use of a ghost argument with a precondition that demands existence of a suitable claim. I'm not sure this isn't even better methodologically; the main advantage of passing the claim explicitly today is that it gives the claim a name, whereas an existential quantification requires use of a choice function. A feature that has been proposed on occasion is a way to find a global skolem function to an instance of an existential quantifier, which would eliminate the need for most claim passing.

If the shared object is guaranteed to never open up, you don't need to pass a claim at all; you can just pass it being closed as a precondition, and form your own claim internally.

You are right, ghost arguments don't change the code from the compilers point of view, but they need to be included in calls and I am concerned this would confuse developers unaware of VCC.

Regarding the first alternative you proposed: I don't know how to use a choice function. Can you elaborate on this?

For the second alternative: Wouldn't I need an additional precondition stating that I can write the shared object in order to be able to form the claim? If I call such a function from other functions, I would again need to ensure that I can write the object, forcing me to take the ownership again.

Best regards,

Daniel

If the client code isn't being verified, you don't have to put in the ghost arguments in the calls.

Choice functions are not yet included in VCC (there is a bug report requesting them), but roughly speaking, a choice function for type T has the following spec:

_(ghost typedef bool Pred<T>[T])
T choose<T:(Pred<T> p)
_(requires \exists T x; p[x])
_(ensures p[\result])
;

With such a function, you could replace a function ofr the form foo(... _(ghost \claim c)) with code like this:

foo(...)
_(requires \exists \claim c; ...)
{
   _(ghost \claim c = choose<\claim>(\lambda \claim c; ...))
   ...

In the second alternative, if you know that the shared object is closed, and it has the invariant _(invariant \on_unwrap(\this, \false)), you can form a claim that claims that the shared object is closed without claiming the object (i.e., you can use an empty set of dependents), so the object does not need to be writable.