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 __VERIFIER_atomic_release_read_lock() {
643 r = r-1;
644}
645void *writer() {
646 __VERIFIER_atomic_take_write_lock();
647 x = 3;
648 w = 0;
649}
650void *reader() {
651 int l;
652 __VERIFIER_atomic_take_read_lock();
653 l = x;
654 y = l;
655 if (!(y == x)) ERROR: goto ERROR;;
656 __VERIFIER_atomic_release_read_lock();
657}
658int main() {
659 pthread_t t1, t2, t3, t4;
660 pthread_create(&t1, 0, writer, 0);
661 pthread_create(&t2, 0, reader, 0);
662 pthread_create(&t3, 0, writer, 0);
663 pthread_create(&t4, 0, reader, 0);
664 pthread_join(t1, 0);
665 pthread_join(t2, 0);