622extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
623extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
624extern int pthread_setspecific (pthread_key_t __key,
625 __const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ;
626extern int pthread_getcpuclockid (pthread_t __thread_id,
627 __clockid_t *__clock_id)
628 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
629extern int pthread_atfork (void (*__prepare) (void),
630 void (*__parent) (void),
631 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
632
633int w=0, r=0, x, y;
634void __VERIFIER_atomic_take_write_lock() {
635 __VERIFIER_assume(w==0 && r==0);
636 w = 1;
637}
638void __VERIFIER_atomic_take_read_lock() {
639 __VERIFIER_assume(w==0);
640 r = r+1;
641}
642void *writer() {
643 __VERIFIER_atomic_take_write_lock();
644 x = 3;
645 w = 0;
646}
647void *reader() {
648 int l;
649 __VERIFIER_atomic_take_read_lock();
650 l = x;
651 y = l;
652 if (!(y == x)) ERROR: goto ERROR;;
653 l = r-1;
654 r = l;
655}
656int main() {
657 pthread_t t1, t2, t3, t4;
658 pthread_create(&t1, 0, writer, 0);
659 pthread_create(&t2, 0, reader, 0);
660 pthread_create(&t3, 0, writer, 0);
661 pthread_create(&t4, 0, reader, 0);
662 pthread_join(t1, 0);