[cpp-threads] sequential consistency for race-free programs

[Alexander Terekhov]

On 7/15/05, Doug Lea <dl at cs.oswego.edu> wrote:
[...]
> It seems that in principle "no speculative stores"  could  someday 
> be formalizable if someone  wants to put a lot  of effort into it.

Informally, it simply means that loads have implicit ddhsb+cchsb.

It would make

     #include <stdio.h>
     #include <pthread.h>

     pthread_rwlock_t rwlock;

     int var;

     void * thread(void *) {
       pthread_rwlock_rdlock(&rwlock);
       if (var) var = 0;
       //pthread_rwlock_unlock(&rwlock);
       return 0;
     }

     int main() {
       pthread_t tid;
       pthread_rwlock_init(&rwlock, 0);
       pthread_rwlock_wrlock(&rwlock);
       pthread_create(&tid, 0, thread, 0);
       var = 1;
       pthread_rwlock_unlock(&rwlock);
       pthread_join(tid, 0);
       printf("%d\n", var);
     }

data-race-free vs data-race-UNfree

     #include <stdio.h>
     #include <pthread.h>

     pthread_rwlock_t rwlock;

     int var;

     void * thread(void *) {
       pthread_rwlock_rdlock(&rwlock);
       /*if (var) */ var = 0;
       //pthread_rwlock_unlock(&rwlock);
       return 0;
     }

     int main() {
       pthread_t tid;
       pthread_rwlock_init(&rwlock, 0);
       pthread_rwlock_wrlock(&rwlock);
       pthread_create(&tid, 0, thread, 0);
       var = 1;
       pthread_rwlock_unlock(&rwlock);
       pthread_join(tid, 0);
       printf("%d\n", var);
     }

Oder?

regards,
alexander.