This project is read-only.

volatile

Jan 28, 2011 at 1:28 PM

Hi,

I use volatile variables to model read-only data that can be modified outside of the program.

I can verify a function that reads a volatile field x using _(writes &This->x), but not without these annotations. Since x is not written and a read-only access to a volatile field is not different from a call to an impure function, I don't see why this is necessary. Is there an easier way to read volatile fields?

Boris

Feb 1, 2011 at 10:05 AM

This is the corresponding code. Fields a and b are volatile.

bool foo(X_t* This) 

_(maintains \wrapped(This))

_(writes &This->a)

_(writes &This->b)

{

	return This->a > This->b;

}


Are the writes clauses necessary, since foo doesn't write anything?
Feb 1, 2011 at 7:04 PM

You can also say:

bool foo(X_t* This) 
_(maintains \mutable(This))
{
        return This->a > This->b;

}

Requiring stuff to be mutable doesn’t give you rights to actually write it, so after the call you will be able to prove that values of This->a are unchanged. If the object is wrapped, other threads can go and write its volatile fields, so in general you wouldn’t be able to prove that This->a is unchanged after the call.

If other threads can indeed write these fields, you will need to use _(atomic ...) to read them.

Hope this helps,

Michal

Feb 1, 2011 at 8:59 PM

Please note that the original snippet has inconsistent requirements, as "vcc /smoke" or an added "_(assert 0)" shows:

#include "vcc.h"

typedef struct X_t {
  volatile int a;
  volatile int b;
} X_t;

bool foo(X_t* This) 
  _(maintains \wrapped(This))
  _(writes &This->a)
  _(writes &This->b)
{
  _(assert 0);
  return This->a > This->b;
}

(Same thing as in one of the cases in http://vcc.codeplex.com/Thread/View.aspx?ThreadId=241287).
Best, Mark
Feb 3, 2011 at 8:33 AM
MichalMoskal wrote:

You can also say:

 

bool foo(X_t* This) 
_(maintains \mutable(This))
{
        return This->a > This->b;

}

What exactly does mutable mean and does it imply !wrapped?

Boris

Feb 3, 2011 at 8:37 AM
MarkHillebrand wrote:

Please note that the original snippet has inconsistent requirements, as "vcc /smoke" or an added "_(assert 0)" shows:

I see. How do you specify several VCC options in Verify->Settings? I can verify the faulty code with "/2 /smoke" in the text field, either separated by a blank or a newline.
Boris
Feb 3, 2011 at 8:49 AM

Hi Boris,

  multiple options should be separated by spaces, as you suggest. With "/2 /smoke" and when you actually remove the "_(assert 0)" there should be complaints about unreachable code in VCC's outputs (note that "_(assert 0)" / "_(assert \false)" has a special meaning with "/smoke" in that it can be used to defuse some smoke checks explicitly -  for example, a function might have genuine unreachable code, which you do not want to remove.).

  Best, Mark

Feb 3, 2011 at 9:23 PM

mutable() means owned by the current thread and not closed. wrapped() means owned by the current thread and closed.

Michal