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
|
#!/usr/bin/env tesh
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Execution came to an end at 1;1
> [Checker] (state: 3, depth: 3, 1 explored traces)
> [Checker] DFS exploration ended. 3 unique states visited; 1 explored traces (0 transition replays, 3 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Executed 1: ActorCreate(child 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] Executed 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] Execution came to an end at 1;1;2;1;2
> [Checker] (state: 6, depth: 6, 1 explored traces)
> [Checker] Sleep set actually containing:
> [Checker] <1,BARRIER_ASYNC_LOCK(barrier: 0)>
> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] DFS exploration ended. 7 unique states visited; 1 explored traces (1 transition replays, 8 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Executed 1: ActorCreate(child 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Executed 1: ActorCreate(child 3) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
> [Checker] Executed 2: BARRIER_WAIT(barrier: 0) (stack depth: 7, state: 7, 0 interleaves)
> [Checker] Executed 3: BARRIER_WAIT(barrier: 0) (stack depth: 8, state: 8, 0 interleaves)
> [Checker] Execution came to an end at 1;1;1;2;3;1;2;3
> [Checker] (state: 9, depth: 9, 1 explored traces)
> [Checker] Sleep set actually containing:
> [Checker] <2,BARRIER_ASYNC_LOCK(barrier: 0)>
> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] DFS exploration ended. 10 unique states visited; 1 explored traces (3 transition replays, 13 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/exploration-algo:BeFS --log=mc_befs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Configuration change: Set 'model-check/exploration-algo' to 'BeFS'
> [Checker] Start a BeFS exploration. Reduction is: dpor.
> [Checker] Executed 1: ActorCreate(child 2) (stack depth: 1, state: 1, 0 interleaves, 1 opened states)
> [Checker] Executed 1: ActorCreate(child 3) (stack depth: 2, state: 2, 0 interleaves, 1 opened states)
> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves, 1 opened states)
> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 4, state: 4, 0 interleaves, 1 opened states)
> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 5, state: 5, 0 interleaves, 1 opened states)
> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves, 1 opened states)
> [Checker] Executed 2: BARRIER_WAIT(barrier: 0) (stack depth: 7, state: 7, 0 interleaves, 1 opened states)
> [Checker] Executed 3: BARRIER_WAIT(barrier: 0) (stack depth: 8, state: 8, 0 interleaves, 1 opened states)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 10).
> [Checker] Execution came to an end at 1;1;1;2;3;1;2;3
> [Checker] (state: 9, depth: 9, 1 explored traces)
> [Checker] Backtracking from 1;1;1;2;3;1;2;3
> [Checker] Sleep set actually containing:
> [Checker] <2,BARRIER_ASYNC_LOCK(barrier: 0)>
> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 4, state: 4, 0 interleaves, 0 opened states)
> [Checker] 3 actors remain, but none of them need to be interleaved (depth 6).
> [Checker] Backtracking from 1;1;1;3
> [Checker] BeFS exploration ended. 10 unique states visited; 1 explored traces (3 transition replays, 13 states visited overall)
|
