source: CIVL/examples/pthread/cprover/25_stack_true.c@ bb03188

//original file: EBStack.java
//amino-cbbs\trunk\amino\java\src\main\java\org\amino\ds\lockfree
//push only

#include <pthread.h>

#define assume(e) __VERIFIER_assume(e)
#define assert(e) { if(!(e)) { ERROR: goto ERROR; (void)0; } }

void __VERIFIER_atomic_acquire(int * m)
{
        assume(*m==0);
        *m = 1;
}

void __VERIFIER_atomic_release(int * m)
{
        assume(*m==1);
        *m = 0;
}

#define MEMSIZE (2*32+1) //0 for "NULL"
int memory[MEMSIZE];
#define INDIR(cell,idx) memory[cell+idx]

int next_alloc_idx = 1;
int m = 0;
int top;

inline int index_malloc(){
        int curr_alloc_idx = -1;

        __VERIFIER_atomic_acquire(&m);
        if(next_alloc_idx+2-1 > MEMSIZE){
                __VERIFIER_atomic_release(&m);
                curr_alloc_idx = 0;
        }else{
                curr_alloc_idx = next_alloc_idx;
                next_alloc_idx += 2;
                __VERIFIER_atomic_release(&m);
        }

        return curr_alloc_idx;
}

inline void EBStack_init(){
        top = 0;
}

inline int isEmpty() {
        if(top == 0)
                return 1;
        else
                return 0;
}

inline int push(int d) {
        int oldTop = -1, newTop = -1;

        newTop = index_malloc();
        if(newTop == 0){
                return 0;
        }else{
                INDIR(newTop,0) = d;

                __VERIFIER_atomic_acquire(&m);
                oldTop = top;
                INDIR(newTop,1) = oldTop;
                top = newTop; 
                __VERIFIER_atomic_release(&m);
                return 1;
        }
}

inline void init(){
        EBStack_init();
}

void __VERIFIER_atomic_assert(int r)
{
                assert(!r || !isEmpty());
}

inline void push_loop(){
        int r = -1;
        int arg = __VERIFIER_nondet_int();
        while(1){
                r = push(arg);
    __VERIFIER_atomic_assert(r);
        }
}

int m2 = 0;
int state = 0;
void* thr1(void* arg)
{
        __VERIFIER_atomic_acquire(&m2);
        switch(state)
        {
        case 0: 
                EBStack_init();
                state = 1;
                //fall-through
        case 1: 
                __VERIFIER_atomic_release(&m2);
                
                push_loop();
                break;
        }

  return 0;
}

int main()
{
  pthread_t t;

        while(1) { pthread_create(&t, 0, thr1, 0); }
}