PREP       = rm -f pan* *trail mpi-spin-init.c
MS         = $(PREP) ; ms -nocancel -noprobe -symmax=5 -symhash=5
MSCC       = mscc -DCOLLAPSE
EXECUTE    = time ./pan -m10000000 -n

PARAMS0 = -np=3 -buf=0  -req=4 -DNPRODUCERS=2
PARAMS1 = -np=4 -buf=0  -req=6 -DNPRODUCERS=3
PARAMS2 = -np=4 -buf=1  -req=6 -DNPRODUCERS=3
PARAMS3 = -np=4 -buf=4  -req=6 -DNPRODUCERS=3
PARAMS4 = -np=5 -buf=0  -req=8 -DNPRODUCERS=4
PARAMS5 = -np=5 -buf=1  -req=8 -DNPRODUCERS=4
PARAMS6 = -np=6 -buf=0 -req=10 -DNPRODUCERS=5
PARAMS7 = -np=7 -buf=0 -req=12 -DNPRODUCERS=6
PARAMS8 = -np=8 -buf=0 -req=14 -DNPRODUCERS=7

# Property 0: Freedom from deadlock, assertions
PREREQ_p0  = mpsc_p0.prom
MS_p0      = $(MS) -dl
MSCC_p0    = $(MSCC) -DSAFETY
EXECUTE_p0 = ($(EXECUTE))

# Property 1: Every message produced is consumed
PREREQ_p1  = mpsc_p1.prom
MS_p1      = $(MS) -DMAXSIZE=1 -DSPROD=1
MSCC_p1    = $(MSCC)
EXECUTE_p1 = ($(EXECUTE) -a)

# Property 2: No producer becomes permanently blocked
PREREQ_p2  = mpsc_p2.prom
MS_p2      = $(MS) -DSPROD=1 -dl
MSCC_p2    = $(MSCC) -DNFAIR=3
EXECUTE_p2 = ($(EXECUTE) -a -f)

# Property 3: For fixed producer, messages are consumed in order produced
PREREQ_p3  = mpsc_p3.prom
MS_p3      = $(MS) -DMAXSIZE=1 -DSPROD=1
MSCC_p3    = $(MSCC)
EXECUTE_p3 = ($(EXECUTE) -a)

small: mpsc_org_p0_0 \
       mpsc_p0_0 mpsc_p0_1 mpsc_p0_2 mpsc_p1_0 mpsc_p1_1 mpsc_p1_2 \
       mpsc_p2_0 mpsc_p2_1 mpsc_p2_2 mpsc_p3_0 mpsc_p3_1 mpsc_p3_2

all: mpsc

# Note: mpsc_p0_8 can be done, but it takes about 35 million states
# and 2+ gigs of RAM

mpsc: mpsc_p0 mpsc_p1 mpsc_p2 mpsc_p3
mpsc_p0: mpsc_org_p0_0 mpsc_p0_0 mpsc_p0_1 mpsc_p0_2 mpsc_p0_3 mpsc_p0_4 \
         mpsc_p0_5 mpsc_p0_6 mpsc_p0_7 mpsc_p0_8
mpsc_p1: mpsc_p1_0 mpsc_p1_1 mpsc_p1_2 mpsc_p1_3  mpsc_p1_4  \
         mpsc_p1_5 mpsc_p1_6
mpsc_p2: mpsc_p2_0 mpsc_p2_1 mpsc_p2_2 mpsc_p2_3 mpsc_p2_4 \
         mpsc_p2_5 # mpsc_p2_6 mpsc_p2_7
mpsc_p3: mpsc_p3_0 mpsc_p3_1 mpsc_p3_2 mpsc_p3_3 mpsc_p3_4 \
         mpsc_p3_5 # mpsc_p3_6 mpsc_p3_7

# The original version of the code in the text contains an error.
# The busy wait loop is not constructed correctly.  This reveals
# the error.  In this trace, requests are repeatedly posted
# to proc 0 until the request bound is exceeded.  

mpsc_org_p0_0: mpsc_org_p0.prom
	$(MS_p0) $(PARAMS0) mpsc_org_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_org_p0_0.out 2>mpsc_org_p0_0.err
	./pan -r > trail.txt

mpsc_p0_0: $(PREREQ_p0)
	$(MS_p0) $(PARAMS0) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_0.out 2>mpsc_p0_0.err

mpsc_p0_1: $(PREREQ_p0)
	$(MS_p0) $(PARAMS1) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_1.out 2>mpsc_p0_1.err

mpsc_p0_2: $(PREREQ_p0)
	$(MS_p0) $(PARAMS2) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_2.out 2>mpsc_p0_2.err

mpsc_p0_3: $(PREREQ_p0)
	$(MS_p0) $(PARAMS3) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_3.out 2>mpsc_p0_3.err

mpsc_p0_4: $(PREREQ_p0)
	$(MS_p0) $(PARAMS4) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_4.out 2>mpsc_p0_4.err

mpsc_p0_5: $(PREREQ_p0)
	$(MS_p0) $(PARAMS5) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_5.out 2>mpsc_p0_5.err

mpsc_p0_6: $(PREREQ_p0)
	$(MS_p0) $(PARAMS6) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_6.out 2>mpsc_p0_6.err

mpsc_p0_7: $(PREREQ_p0)
	$(MS_p0) $(PARAMS7) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_7.out 2>mpsc_p0_7.err

mpsc_p0_8: $(PREREQ_p0)
	$(MS_p0) $(PARAMS8) mpsc_p0.prom
	$(MSCC_p0)
	$(EXECUTE_p0) > mpsc_p0_8.out 2>mpsc_p0_8.err


mpsc_p1_0: $(PREREQ_p1)
	$(MS_p1) $(PARAMS0) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_0.out 2>mpsc_p1_0.err

mpsc_p1_1: $(PREREQ_p1)
	$(MS_p1) $(PARAMS1) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_1.out 2>mpsc_p1_1.err

mpsc_p1_2: $(PREREQ_p1)
	$(MS_p1) $(PARAMS2) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_2.out 2>mpsc_p1_2.err

mpsc_p1_3: $(PREREQ_p1)
	$(MS_p1) $(PARAMS3) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_3.out 2>mpsc_p1_3.err

mpsc_p1_4: $(PREREQ_p1)
	$(MS_p1) $(PARAMS4) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_4.out 2>mpsc_p1_4.err

mpsc_p1_5: $(PREREQ_p1)
	$(MS_p1) $(PARAMS5) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_5.out 2>mpsc_p1_5.err

mpsc_p1_6: $(PREREQ_p1)
	$(MS_p1) $(PARAMS6) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_6.out 2>mpsc_p1_6.err

mpsc_p1_7: $(PREREQ_p1)
	$(MS_p1) $(PARAMS7) mpsc_p1.prom
	$(MSCC_p1)
	$(EXECUTE_p1) > mpsc_p1_7.out 2>mpsc_p1_7.err



mpsc_p2_0: $(PREREQ_p2)
	$(MS_p2) $(PARAMS0) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_0.out 2>mpsc_p2_0.err

mpsc_p2_1: $(PREREQ_p2)
	$(MS_p2) $(PARAMS1) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_1.out 2>mpsc_p2_1.err

mpsc_p2_2: $(PREREQ_p2)
	$(MS_p2) $(PARAMS2) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_2.out 2>mpsc_p2_2.err

mpsc_p2_3: $(PREREQ_p2)
	$(MS_p2) $(PARAMS3) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_3.out 2>mpsc_p2_3.err

mpsc_p2_4: $(PREREQ_p2)
	$(MS_p2) $(PARAMS4) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_4.out 2>mpsc_p2_4.err

mpsc_p2_5: $(PREREQ_p2)
	$(MS_p2) $(PARAMS5) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_5.out 2>mpsc_p2_5.err

mpsc_p2_6: $(PREREQ_p2)
	$(MS_p2) $(PARAMS6) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_6.out 2>mpsc_p2_6.err

mpsc_p2_7: $(PREREQ_p2)
	$(MS_p2) $(PARAMS7) mpsc_p2.prom
	$(MSCC_p2)
	$(EXECUTE_p2) > mpsc_p2_7.out 2>mpsc_p2_7.err



mpsc_p3_0: $(PREREQ_p3)
	$(MS_p3) $(PARAMS0) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_0.out 2>mpsc_p3_0.err

mpsc_p3_1: $(PREREQ_p3)
	$(MS_p3) $(PARAMS1) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_1.out 2>mpsc_p3_1.err

mpsc_p3_2: $(PREREQ_p3)
	$(MS_p3) $(PARAMS2) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_2.out 2>mpsc_p3_2.err

mpsc_p3_3: $(PREREQ_p3)
	$(MS_p3) $(PARAMS3) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_3.out 2>mpsc_p3_3.err

mpsc_p3_4: $(PREREQ_p3)
	$(MS_p3) $(PARAMS4) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_4.out 2>mpsc_p3_4.err

mpsc_p3_5: $(PREREQ_p3)
	$(MS_p3) $(PARAMS5) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_5.out 2>mpsc_p3_5.err

mpsc_p3_6: $(PREREQ_p3)
	$(MS_p3) $(PARAMS6) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_6.out 2>mpsc_p3_6.err

mpsc_p3_7: $(PREREQ_p3)
	$(MS_p3) $(PARAMS7) mpsc_p3.prom
	$(MSCC_p3)
	$(EXECUTE_p3) > mpsc_p3_7.out 2>mpsc_p3_7.err

mpisrc:
	cd ../src ; make

clean:
	-rm -f pan* *.trail *.out mpi-spin-init.c trail.txt *.err *~
