1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
#!/usr/bin/env tesh
! expect return 1
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
> [ 0.000000] (0:maestro@) Behavior: assert
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
! expect return 4
# because simgrid::mc::ExitStatus::PROGRAM_CRASH = 4
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
> [ 0.000000] (0:maestro@) Behavior: abort
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Aborted
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (1:app@Fafard) Error reached
> [ 0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 36 explored traces (30 transition replays, 73 states visited overall)
! expect return 4
# because simgrid::mc::ExitStatus::PROGRAM_CRASH = 4
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
> [ 0.000000] (0:maestro@) Behavior: segv
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> Segmentation fault.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Segmentation fault
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
#!/usr/bin/env tesh
! expect return 1
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check/reduction:odpor
> [ 0.000000] (0:maestro@) Behavior: assert
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: odpor.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
! expect return 4
# because simgrid::mc::ExitStatus::PROGRAM_CRASH = 4
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc --cfg=model-check/reduction:odpor
> [ 0.000000] (0:maestro@) Behavior: abort
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: odpor.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Aborted
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check/reduction:odpor
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: odpor.
> [ 0.000000] (1:app@Fafard) Error reached
> [ 0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 36 explored traces (30 transition replays, 73 states visited overall)
! expect return 4
# because simgrid::mc::ExitStatus::PROGRAM_CRASH = 4
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc --cfg=model-check/reduction:odpor
> [ 0.000000] (0:maestro@) Behavior: segv
> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: odpor.
> Segmentation fault.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Segmentation fault
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 explored traces (19 transition replays, 46 states visited overall)
> [ 0.000000] (0:maestro@) Start the critical transition detection phase.
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) *** CRITICAL TRANSITION FOUND ***
> [ 0.000000] (0:maestro@) *********************************
> [ 0.000000] (0:maestro@) Current knowledge of explored stack:
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) ( CORRECT) Actor 1 in ==> simcall: Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Found the critical transition: Actor 1 ==> simcall: Random([0;5] ~> 4)
|
