This project is read-only.

thread_locality of ownership domains

Nov 3, 2010 at 8:58 AM

I have a simple confusing doubt. Please clear it.

suppose in a function specification i have

func( struct example *G, unsigned *arr)

requires(wrapped(G))

requires(wrapped(as_array(arr, G->n)

writes(as_arraY(arr,G->n)

{

unsigned curr;

unwrap(as_array(arr,G->n));

 // reading some variable in ownership domain of G

if(G->es[index].s == curr){

}

}

 can i do so even though the  array 'es'  is owned by G and not by the current thread?  even though i know that G is wrapped and cannot be changed by some other thread

I am asking this because I am getting an error for the 'thread_locality' of G->es[index].s

I have asserted that 'index' lies in the range of array bounds of 'es', then what are the possible reasons I got this error?

I read in the tutorial, that unwrapping other objects might disturb the thread locality of some variables. How? Is this could be the possible reason?

 

 

 

 

Nov 4, 2010 at 10:29 AM

It looks to me as if 'es' is array of objects, not a primitive one (as suggested by the use of .s). Unlike arrays of primitive types, objects of arrays are not individual objects by themselves, so you would need to specify that G owns each of the elements of es; then it should just work. Maybe you will need to assert an in_domain to make the verifier see it, though.