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>
25 make urcu_free | tee urcu_free.log
26 make urcu_free_nested | tee urcu_free_nested.log
27 make urcu_free_no_rmb | tee urcu_free_no_rmb.log
28 make urcu_free_no_wmb | tee urcu_free_no_wmb.log
29 make urcu_free_no_mb | tee urcu_free_no_mb.log
30 make urcu_free_single_flip | tee urcu_free_single_flip.log
31 make urcu_progress_writer | tee urcu_progress_writer.log
32 make urcu_progress_reader | tee urcu_progress_reader.log
33 make urcu_progress_writer_error | tee urcu_progress_writer_error.log
34 make asserts | tee asserts.log
37 #show trail : spin -v -t -N pan.ltl input.spin
38 # after each individual make.
42 @echo
"Verification summary"
46 cat DEFINES
> .input.spin
47 cat
${SPINFILE} >> .input.spin
48 rm -f .input.spin.trail
49 spin
-a
-X .input.spin
50 gcc
-w
${CFLAGS} -DSAFETY
-o pan pan.c
51 .
/pan
-v
-c1
-X
-m10000
-w20
52 cp .input.spin
$@.spin.input
53 -cp .input.spin.trail
$@.spin.input.trail
55 urcu_free
: clean urcu_free_ltl run
56 cp .input.spin
$@.spin.input
57 -cp .input.spin.trail
$@.spin.input.trail
59 urcu_free_nested
: clean urcu_free_ltl urcu_free_nested_define run
60 cp .input.spin
$@.spin.input
61 -cp .input.spin.trail
$@.spin.input.trail
63 urcu_free_nested_define
:
64 cp urcu_free_nested.
define .input.
define
66 urcu_free_no_rmb
: clean urcu_free_ltl urcu_free_no_rmb_define run
67 cp .input.spin
$@.spin.input
68 -cp .input.spin.trail
$@.spin.input.trail
70 urcu_free_no_rmb_define
:
71 cp urcu_free_no_rmb.
define .input.
define
73 urcu_free_no_wmb
: clean urcu_free_ltl urcu_free_no_wmb_define run
74 cp .input.spin
$@.spin.input
75 -cp .input.spin.trail
$@.spin.input.trail
77 urcu_free_no_wmb_define
:
78 cp urcu_free_no_wmb.
define .input.
define
80 urcu_free_no_mb
: clean urcu_free_ltl urcu_free_no_mb_define run
81 cp .input.spin
$@.spin.input
82 -cp .input.spin.trail
$@.spin.input.trail
84 urcu_free_no_mb_define
:
85 cp urcu_free_no_mb.
define .input.
define
87 urcu_free_single_flip
: clean urcu_free_ltl urcu_free_single_flip_define run
88 cp .input.spin
$@.spin.input
89 -cp .input.spin.trail
$@.spin.input.trail
91 urcu_free_single_flip_define
:
92 cp urcu_free_single_flip.
define .input.
define
96 cat .input.
define >> pan.ltl
97 cat DEFINES
>> pan.ltl
98 spin
-f
"!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
102 urcu_progress_writer
: clean urcu_progress_writer_ltl \
103 urcu_progress_writer_define run_weak_fair
104 cp .input.spin
$@.spin.input
105 -cp .input.spin.trail
$@.spin.input.trail
107 urcu_progress_writer_define
:
108 cp urcu_progress_writer.
define .input.
define
110 urcu_progress_writer_ltl
:
112 cat .input.
define > pan.ltl
113 cat DEFINES
>> pan.ltl
114 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
116 urcu_progress_reader
: clean urcu_progress_reader_ltl \
117 urcu_progress_reader_define run_weak_fair
118 cp .input.spin
$@.spin.input
119 -cp .input.spin.trail
$@.spin.input.trail
121 urcu_progress_reader_define
:
122 cp urcu_progress_reader.
define .input.
define
124 urcu_progress_reader_ltl
:
126 cat .input.
define > pan.ltl
127 cat DEFINES
>> pan.ltl
128 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
130 urcu_progress_writer_error
: clean urcu_progress_writer_error_ltl \
131 urcu_progress_writer_error_define run_weak_fair
132 cp .input.spin
$@.spin.input
133 -cp .input.spin.trail
$@.spin.input.trail
135 urcu_progress_writer_error_define
:
136 cp urcu_progress_writer_error.
define .input.
define
138 urcu_progress_writer_error_ltl
:
140 cat .input.
define > pan.ltl
141 cat DEFINES
>> pan.ltl
142 spin
-f
"!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
146 .
/pan
-a
-f
-v
-c1
-X
-m10000
-w20
149 .
/pan
-a
-v
-c1
-X
-m10000
-w20
152 gcc
-w
${CFLAGS} -o pan pan.c
154 pan.c
: pan.ltl
${SPINFILE}
155 cat .input.
define > .input.spin
156 cat DEFINES
>> .input.spin
157 cat
${SPINFILE} >> .input.spin
158 rm -f .input.spin.trail
159 spin
-a
-X
-N pan.ltl .input.spin
161 .PHONY
: clean default
distclean summary
163 rm -f pan
* trail.out .input.spin
* *.spin.trail .input.
define
165 rm -f
*.trail
*.input
*.log