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 #CFLAGS=-DHASH64 -DREACH
23 #try pan -i to get the smallest trace.
26 SPINFILE_FAIR
=futex.spin
29 make futex_progress | tee futex_progress.log
30 make futex_progress_no_wake | tee futex_progress_no_wake.log
31 make futex_progress_late_dec | tee futex_progress_late_dec.log
32 make futex_progress_inverted_waiting_vs_gp_futex | tee futex_progress_inverted_waiting_vs_gp_futex.
define.log
33 make asserts | tee asserts.log
36 #show trail : spin -v -t -N pan.ltl input.spin
37 # after each individual make.
41 @echo
"Verification summary"
45 cat DEFINES
> .input.spin
46 cat
${SPINFILE} >> .input.spin
47 rm -f .input.spin.trail
48 spin
-a
-X .input.spin
49 gcc
-w
${CFLAGS} -DSAFETY
-o pan pan.c
50 .
/pan
-v
-c1
-X
-m10000000
-w19
51 cp .input.spin
$@.spin.input
52 -cp .input.spin.trail
$@.spin.input.trail
54 futex_progress
: clean futex_ltl run_weak_fair
55 cp .input.spin
$@.spin.input
56 -cp .input.spin.trail
$@.spin.input.trail
58 futex_progress_no_wake
: clean futex_ltl futex_progress_no_wake_define run_weak_fair
59 cp .input.spin
$@.spin.input
60 -cp .input.spin.trail
$@.spin.input.trail
62 futex_progress_no_wake_define
:
63 cp futex_progress_no_wake.
define .input.
define
65 futex_progress_late_dec
: clean futex_ltl futex_progress_late_dec_define run_weak_fair
66 cp .input.spin
$@.spin.input
67 -cp .input.spin.trail
$@.spin.input.trail
69 futex_progress_late_dec_define
:
70 cp futex_progress_late_dec.
define .input.
define
72 futex_progress_inverted_waiting_vs_gp_futex
: clean futex_ltl futex_progress_inverted_waiting_vs_gp_futex_define run_weak_fair
73 cp .input.spin
$@.spin.input
74 -cp .input.spin.trail
$@.spin.input.trail
76 futex_progress_inverted_waiting_vs_gp_futex_define
:
77 cp futex_progress_inverted_waiting_vs_gp_futex.
define .input.
define
82 cat .input.
define >> pan.ltl
83 spin
-f
"!(`cat futex.ltl | grep -v ^//`)" >> pan.ltl
86 .
/pan
-a
-v
-c1
-X
-m10000000
-w19
89 gcc
-w
${CFLAGS} -o pan pan.c
91 pan.c
: pan.ltl
${SPINFILE}
92 cat DEFINES
> .input.spin
93 cat .input.
define >> .input.spin
94 cat
${SPINFILE} >> .input.spin
95 rm -f .input.spin.trail
96 spin
-a
-X
-N pan.ltl .input.spin
98 run_weak_fair
: pan_fair
99 .
/pan_fair
-a
-f
-v
-c1
-X
-m10000000
-w20
102 gcc
-w
${CFLAGS} -o pan_fair pan_fair.c
104 pan_fair.c
: pan.ltl
${SPINFILE_FAIR}
105 cat DEFINES
> .input.spin
106 cat .input.
define >> .input.spin
107 cat
${SPINFILE_FAIR} >> .input.spin
108 rm -f .input.spin.trail
109 spin
-a
-X
-N pan.ltl .input.spin
112 .PHONY
: clean default
distclean summary
114 rm -f pan
* trail.out .input.spin
* *.spin.trail .input.
define
116 rm -f
*.trail
*.input
*.log