1 # This program is free software; you can redistribute it and/or modify
2 # it under the terms of the GNU General Public License as published by
3 # the Free Software Foundation; either version 2 of the License, or
4 # (at your option) any later version.
6 # This program is distributed in the hope that it will be useful,
7 # but WITHOUT ANY WARRANTY; without even the implied warranty of
8 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
9 # GNU General Public License for more details.
11 # You should have received a copy of the GNU General Public License
12 # along with this program; if not, write to the Free Software
13 # Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
15 # Copyright (C) Mathieu Desnoyers, 2009
17 # Authors: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
20 #for multi-core verif, 15.5GB shared mem, use files if full
21 #CFLAGS=-DHASH64 -DMEMLIM=15500 -DNCORE=2
22 #CFLAGS=-DHASH64 -DCOLLAPSE -DMA=88 -DMEMLIM=15500 -DNCORE=8
25 #CFLAGS=-DHASH64 -DCOLLAPSE -DMA=88
26 CFLAGS
=-DHASH64
-DCOLLAPSE
32 #make urcu_free | tee urcu_free.log
33 #make urcu_free_no_mb | tee urcu_free_no_mb.log
34 #make urcu_free_no_rmb | tee urcu_free_no_rmb.log
35 #make urcu_free_no_wmb | tee urcu_free_no_wmb.log
36 #make urcu_free_single_flip | tee urcu_free_single_flip.log
37 make urcu_progress_writer | tee urcu_progress_writer.log
38 make urcu_progress_reader | tee urcu_progress_reader.log
39 make urcu_progress_writer_error | tee urcu_progress_writer_error.log
40 #make asserts | tee asserts.log
43 #show trail : spin -v -t -N pan.ltl input.spin
44 # after each individual make.
48 @echo
"Verification summary"
52 cat DEFINES
> .input.spin
53 cat
${SPINFILE} >> .input.spin
54 rm -f .input.spin.trail
55 spin
-a
-X .input.spin
56 gcc
-O2
-w
${CFLAGS} -DSAFETY
-o pan pan.c
57 .
/pan
-v
-c1
-X
-m10000000
-w20
58 cp .input.spin
$@.spin.input
59 -cp .input.spin.trail
$@.spin.input.trail
61 urcu_free
: clean urcu_free_ltl run
62 cp .input.spin
$@.spin.input
63 -cp .input.spin.trail
$@.spin.input.trail
65 urcu_free_nested
: clean urcu_free_ltl urcu_free_nested_define run
66 cp .input.spin
$@.spin.input
67 -cp .input.spin.trail
$@.spin.input.trail
69 urcu_free_nested_define
:
70 cp urcu_free_nested.
define .input.
define
72 urcu_free_no_rmb
: clean urcu_free_ltl urcu_free_no_rmb_define run
73 cp .input.spin
$@.spin.input
74 -cp .input.spin.trail
$@.spin.input.trail
76 urcu_free_no_rmb_define
:
77 cp urcu_free_no_rmb.
define .input.
define
79 urcu_free_no_wmb
: clean urcu_free_ltl urcu_free_no_wmb_define run
80 cp .input.spin
$@.spin.input
81 -cp .input.spin.trail
$@.spin.input.trail
83 urcu_free_no_wmb_define
:
84 cp urcu_free_no_wmb.
define .input.
define
86 urcu_free_no_mb
: clean urcu_free_ltl urcu_free_no_mb_define run
87 cp .input.spin
$@.spin.input
88 -cp .input.spin.trail
$@.spin.input.trail
90 urcu_free_no_mb_define
:
91 cp urcu_free_no_mb.
define .input.
define
93 urcu_free_single_flip
: clean urcu_free_ltl urcu_free_single_flip_define run
94 cp .input.spin
$@.spin.input
95 -cp .input.spin.trail
$@.spin.input.trail
97 urcu_free_single_flip_define
:
98 cp urcu_free_single_flip.
define .input.
define
102 cat .input.
define >> pan.ltl
103 cat DEFINES
>> pan.ltl
104 spin
-f
"!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
108 urcu_progress_writer
: clean urcu_progress_writer_ltl \
109 urcu_progress_writer_define run_weak_fair
110 cp .input.spin
$@.spin.input
111 -cp .input.spin.trail
$@.spin.input.trail
113 urcu_progress_writer_define
:
114 cp urcu_progress_writer.
define .input.
define
116 urcu_progress_writer_ltl
:
118 cat .input.
define > pan.ltl
119 cat DEFINES
>> pan.ltl
120 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
122 urcu_progress_reader
: clean urcu_progress_reader_ltl \
123 urcu_progress_reader_define run_weak_fair
124 cp .input.spin
$@.spin.input
125 -cp .input.spin.trail
$@.spin.input.trail
127 urcu_progress_reader_define
:
128 cp urcu_progress_reader.
define .input.
define
130 urcu_progress_reader_ltl
:
132 cat .input.
define > pan.ltl
133 cat DEFINES
>> pan.ltl
134 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
136 urcu_progress_writer_error
: clean urcu_progress_writer_error_ltl \
137 urcu_progress_writer_error_define run_weak_fair
138 cp .input.spin
$@.spin.input
139 -cp .input.spin.trail
$@.spin.input.trail
141 urcu_progress_writer_error_define
:
142 cp urcu_progress_writer_error.
define .input.
define
144 urcu_progress_writer_error_ltl
:
146 cat .input.
define > pan.ltl
147 cat DEFINES
>> pan.ltl
148 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
152 .
/pan
-a
-f
-v
-c1
-X
-m10000000
-w20
155 .
/pan
-a
-v
-c1
-X
-m10000000
-w20
158 gcc
-O2
-w
${CFLAGS} -o pan pan.c
160 pan.c
: pan.ltl
${SPINFILE}
161 cat .input.
define > .input.spin
162 cat DEFINES
>> .input.spin
163 cat
${SPINFILE} >> .input.spin
164 rm -f .input.spin.trail
165 spin
-a
-X
-N pan.ltl .input.spin
167 .PHONY
: clean default
distclean summary
169 rm -f pan
* trail.out .input.spin
* *.spin.trail .input.
define
171 rm -f
*.trail
*.input
*.log