vcc(atomic_inline)

Dec 16, 2010 at 2:52 PM

Hi,

If I declare one function with vcc(atomic_inline), will it ensure that the update of that funtion is atomic?

Looking for your suggestions.

Thanks.

Coordinator
Dec 19, 2010 at 8:03 AM

Hi,

  vcc(atomic_inline) does not ensure that a function update is atomic. It's effects are that the body of the function is inlined when the function is called inside of an atomic() {} block. This is typically used for the specification of interlocked compiler intrinsics (e.g., InterlockedCompareExchange()), cf. Section 7 of the tutorial, http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-1col.pdf.

  Hope that helps, Mark

Jan 20, 2011 at 12:40 PM
Edited Jan 22, 2011 at 3:06 PM

Hi Mark,

What is the malloc notations for the new version of the Vcc?

Coordinator
Feb 11, 2011 at 8:36 AM

Hi,

  malloc() is the same in old and new VCC syntax: 

#include "vcc.h"
#include <stdlib.h>

struct S {
  int a;
};

void foo() {
  struct S *s = (struct S *)malloc(sizeof(struct S));
  _(assume s!=NULL) // assume enough memory
  // old syntax version: assume(s!=NULL);
  s->a = 42;
}

Best, Mark