Using Pthread

Jul 17, 2011 at 3:59 PM

Hi,

I have used pthread_create() in the following example. As VCC was complaining (cannot convert claim to void *) while passing the claim pointer using pthread_create(), I have used one structure thread_data , consisting the claim c_t and then passed the thread_data object. However, it still has some errors. The example and the errors are given below:

#include <vcc.h>

#include <pthread.h>

#define NUM_THREADS 2

 _(claimable) typedef struct _X

{    

      int dummy ;

}X;

struct thread_data{

      int d;

      _(ghost \claim c_t;)

};

struct thread_data thread_data_array[NUM_THREADS];

void test(X *x _(ghost \claim c))

_(always c, x->\consistent)

{}

void *start_thread (void *param)

_(requires \wrapped(((struct thread_data *) param)))

_(always ((struct thread_data *) param)->c_t, (&x)->\consistent)

{

      test( &x _(ghost ((struct thread_data *) param)->c_t));

}

X x;

int main()

_(writes \universe())

_(requires \program_entry_point())

{          

            pthread_t threads[NUM_THREADS];          

            x.dummy = 0;

            _(wrap &x);

            int t, rc;

            t = 0;           

            _(ghost thread_data_array[t].c_t = \make_claim({&x}, (&x)->\consistent);)

            rc = pthread_create(&threads[t], NULL, start_thread, (void *) &thread_data_array[t]);

            return 1;

}

 :error VC9502: Call 'start_thread' did not verify.

: error VC9599: (related information) Precondition: '\wrapped(((struct thread_data *) param))'.

Exiting with 3 (1 error(s).)

Any suggestions about how to get this to verify would be greatly appreciated.

Thanks,

Saimon.

Aug 15, 2011 at 12:44 PM

I apologize if i wrote something wrong here. I didn't get any reply for almost like one month.

I will be grateful if I can know whether my problem is irrelevant.

 

Thanks.   

Coordinator
Aug 18, 2011 at 8:04 PM

Hi,

  I am assuming the error is on the line "rc = pthread_create(&threads[t], NULL, start_thread, (void *) &thread_data_array[t]);" line? Is pthreads_create() a macro? Could you expand it for us?

  Cheers, Mark

Aug 19, 2011 at 3:02 PM

Yes.  That's the line with the error. pthread_create is a C function, not a macro.Its declaration in the header file we are using is

PTW32_DLLPORT int PTW32_CDECL pthread_create (pthread_t * tid,
                            const pthread_attr_t * attr,
                            void *(*start) (void *),
                            void *arg);

It seemed to us that VCC might have some special knowledge of pthreads, because the error actually makes sense.  The precondition of start_thread says that it owns an object, but we have no way to give a thread ownership on start up.

 

The deeper problem is that when we start a thread, it seems that the thread needs to own something of its own, even it is only a claim that says some other object is consistent. If we can avoid the need for start_thread to own an object in order to know that some other object is consistent, then we can likely get past this problem.

 

Cheers,

Theo

Coordinator
Aug 21, 2011 at 10:19 AM

Hi,

  the issue here is that VCC generates a type-check condition for the function pointer, to prove that the "start" functions satisfies the contract of the function pointer type used in pthread_create(). This proof works by assuming the requirements of the function pointer type, then doing a call to the specific function ("start" here), and then proving that the postconditions of the function pointer type hold. In this case, there is no contract for the function pointer type, and proving the requirements of start() just fails. The following example might clarify this:

//`/newsyntax
#include <vcc.h>

#define NULL ((void*)0)

typedef void *(*F) (void *);

typedef void *(*G) (void *x) _(requires x != NULL);

void *foo(void *x) _(requires x != NULL);

void bar(int x, F fn);

void baz(int x, G fn);

void call_bar() { // doesn't work
  bar(42, foo);
}

void call_baz() { // work
  baz(42, foo);
}

  Note that these proofs have names of the form "$fnptr_foo_to_fnptr#X", and may be a little difficult to track.

  Cheers, Mark