This project is read-only.

Race conditions / memory ownership

Sep 24, 2012 at 4:00 PM
Edited Sep 24, 2012 at 4:10 PM

Hello,

 

I am using a library that allows me to do something in the spirit of

 

void foo()
{
  extern void nonBlockingSend(const int* data, int len, OperationHandle* h);
  extern void waitForCompletion(OperationHandle* h);
  int data[10]; .... ; // data array
  ...

  // start transmission of data in the background 
  // (all 10 positions) in the background (by another thread)
  nonBlockingSend(data, 10, &h); 

  // read the value of 'data[0]' while being transmitted: OK
  int value = data[5] + 1;         

  // overwrite 'data' when it is unsure whether transmission has terminated
  data[0]++ ; 

  // make sure the operation has terminated by synch. w/other thread.
  waitForCompletion(&h);  

  // afterwards it is OK to modify data
  data[2]++; 
}

 

So, essentially, there is a race condition in  "data[0]++ " between nonBlockingSend() (supposed to be reading data from position 0 and 10) and waitForCompletion() that I would like vcc to report as an error.

For that purpose, what kind of concepts/annotations would apply to:

  1. nonBlockingSend(), excluding pre-conditions for \thread_local_array((int*) data, 10) which I am already aware of.
  2. waitForOperation()
  3. the code between the above two operations (preferably none if possible)
  4. and maybe even before  nonBlockingSend() or after waitForCompletion() (preferably none if possible again)

I hope the example is general enough. I have a little trouble yet understanding the ownership concepts from the VCC tutorial, I guess it will have something to do with it. My guess is I need to relinquish ownership of data in the send operation and get it back in the wait operation.  

Another detail:  "data" is local to the stack of "foo" intentionally, but I guess it will make a difference if it is a global variable (which I find already a bit tricky to handle in other respects) or if it is heap-allocated with malloc. What are the implications for each of these variations? I would prefer to have 'data' as local to the stack of "foo" hopefully. 

Thanks, best regards,

Eduardo

Oct 10, 2012 at 7:09 AM
Edited Oct 10, 2012 at 7:13 AM

Hello Eduardo,

Let's first imagine that the data was in an object, rather than on the stack. NonBlockingSend basically needs to take some permission on the object, to keep it from changing while it sends the data. Since this thread is concurrently reading this data, both threads must essentially have a read permission. waitForCompletion() returns the  permission passed into nonBlockingSend() back to the caller. Once the caller has the total permission on the data, he can use it to write the data.

Now, there is a problem: we don't want to allow waitForCompletion to be called twice (since it can only return the permission once). So nonBLockingSend should act like a lockAcquire, in the sense that it gives the caller possession of a token, and only a token holder can call waitForCompletion() and get the permission back out (but the token stays in). If you want to allow only one nonBLockingSend to be in flight at a time, you have a singleton pattern for this object; otherwise, you can think of nonBLockingSend as creating a new ghost object, which can also serve as the token if you like.

Now, in VCC there are a lot of ways to handle the permission accounting, but the most natural one is to pass into NonBlockingSend a (\wrapped0) \claim that claims the data object is closed (and hence the data is not changing); waitForCompletion() will return the same \claim (again, \wrapped0). The main thread can keep ownership of the data object, which will have a claim count of 1 while the send is going on. This will make it impossible for the main thread to modify the data (since to do so would require unwrapping the data object, and this unwrapping cannot be done while the object\s \claim_count is nonzero). (I assume this is what you mean by wanting VCC to report an error.) However, after the waitForCOmpletion(), the caller has ownership on the sole claim on the data, so he can destroy the claim, unwrap the data object, and write it to his heart's content.

Regarding the data being on the stack: if you take the address of an object (which is essentially what you are doing when use the array object without indexing into it), it is essentially allocated on the heap (as if with malloc) when it comes into scope, and destroyed (as if with free()) when it goes out of scope. So it doesn't matter whether it is in the stack of the heap. However, the fact that x isn't inside a data object means that you have to jump through some hoops: you have to turn the data into an array object (so that it can be owned by another object), and then , since array objects are not claimable, wrap that in a claimable ghost object, something like this:

#include <vcc.h> 

// a ghost object used to represent a claimable chunk of data
_(typedef _(claimable) struct Data {
    int *data;
    size_t size;
    _(invariant \mine((int[size]) data))
} Data;)

typedef struct Handle {
    _(ghost \claim c)
    _(ghost Data ^data)
    int dummy;
    // some invariants and data
} Handle;

void sendData(int *data, size_t size, Handle *h _(ghost Data ^d) _(ghost \claim c))
    _(always c, d->\closed)
    _(requires d->data == data)
    _(requires d->size == size)
    _(requires \wrapped0(c))
    _(requires \extent_mutable(h)) 
    _(writes c) // gives up ownership of c
    _(writes h)
    _(ensures \wrapped(h))
    _(ensures h->c == c && h->data == d)
    ;

void waitCompletion(Handle *h)
    _(requires \wrapped(h))
    _(writes h)
    _(ensures \extent_mutable(h))
    _(ensures \wrapped0(\old(h->c)))
    ;

void test() {
    int x[10];
    Handle h;
    _(ghost Data d)
    _(wrap _(int[10]) x)
    _(ghost d.data = x)
    _(ghost d.size = 10)
    _(wrap &d)
    _(ghost \claim c = \make_claim({&d},(&d)->\closed))
    sendData(x,10,&h, _(ghost &d) _(ghost c));
    waitCompletion(&h);
    _(ghost \destroy_claim(c,{&d}))
    _(unwrap &d)
    _(unwrap (int[10]) x)
    x[2] = 3;
}

Hope this helps,

ernie

 

Oct 16, 2012 at 6:37 PM

Thanks a lot, I will try your advice.