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
|
# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
! ignore .*LD_PRELOAD.*
# This test raises a deadlock, thus the return code of 2
! expect return 2
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-mutex-simpledeadlock
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
> All threads are started.
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
> All threads are started.
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [ker_engine/INFO] 3 actors are still active, awaiting something. Here is their status:
> [0.000000] [ker_engine/INFO] - pid 1 (main thread@Lilibeth) simcall ActorJoin(pid:2)
> [0.000000] [ker_engine/INFO] - pid 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3)
> [0.000000] [ker_engine/INFO] - pid 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
> [0.000000] [mc_global/INFO] Counter-example execution trace:
> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorCreate(child 2)
> [0.000000] [mc_global/INFO] Actor 1 in simcall ActorCreate(child 3)
> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;1;2;2;3;2;3;3'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 25 unique states visited; 1 explored traces (4 transition replays, 27 states visited overall)
> [0.000000] [mc_ct/INFO] Start the critical transition detection phase.
> All threads are started.
> All threads are started.
> All threads are started.
> [0.000000] [mc_ct/INFO] *********************************
> [0.000000] [mc_ct/INFO] *** CRITICAL TRANSITION FOUND ***
> [0.000000] [mc_ct/INFO] *********************************
> [0.000000] [mc_ct/INFO] Current knowledge of explored stack:
> [0.000000] [mc_ct/INFO] ( CORRECT) Actor 1 in ==> simcall: ActorCreate(child 2)
> [0.000000] [mc_ct/INFO] ( CORRECT) Actor 1 in ==> simcall: ActorCreate(child 3)
> [0.000000] [mc_ct/INFO] ( CORRECT) Actor 2 in ==> simcall: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_ct/INFO] ( CORRECT) Actor 2 in ==> simcall: MUTEX_WAIT(mutex: 0, owner: 2)
> [0.000000] [mc_ct/INFO] ( CORRECT) Actor 3 in ==> simcall: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
> [0.000000] [mc_ct/INFO] (INCORRECT) Actor 2 in ==> simcall: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
> [0.000000] [mc_ct/INFO] (INCORRECT) Actor 3 in ==> simcall: MUTEX_WAIT(mutex: 1, owner: 3)
> [0.000000] [mc_ct/INFO] (INCORRECT) Actor 3 in ==> simcall: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_ct/INFO] Found the critical transition: Actor 3 ==> simcall: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
# The return code of a replay is not modified
! expect return 0
! timeout 500
! setenv LD_PRELOAD=${libdir:=.}/libsthread.so
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/pthread-mutex-simpledeadlock --cfg=model-check/replay:'1;1;2;2;3;2;3;3' --log=no_loc
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/replay' to '1;1;2;2;3;2;3;3'
> [0.000000] [mc_record/INFO] path=1;1;2;2;3;2;3;3
> [0.000000] [mc_record/INFO] The backtrace of each transition will not be shown because of --log=no_loc
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #1 '1/0' Actor main thread(pid:1): ActorCreate(-1)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #2 '1/0' Actor main thread(pid:1): ActorCreate(-1)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> All threads are started.
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #3 '2/0' Actor thread 1(pid:2): MUTEX_ASYNC_LOCK(mutex_id:0 owner:none)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #4 '2/0' Actor thread 1(pid:2): MUTEX_WAIT(mutex_id:0 owner:2)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #5 '3/0' Actor thread 2(pid:3): MUTEX_ASYNC_LOCK(mutex_id:1 owner:none)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #6 '2/0' Actor thread 1(pid:2): MUTEX_ASYNC_LOCK(mutex_id:1 owner:3)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #7 '3/0' Actor thread 2(pid:3): MUTEX_WAIT(mutex_id:1 owner:3)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] * Path chunk #8 '3/0' Actor thread 2(pid:3): MUTEX_ASYNC_LOCK(mutex_id:0 owner:2)
> [0.000000] [mc_record/INFO] ***********************************************************************************
> [0.000000] [mc_record/INFO] The replay of the trace is complete. DEADLOCK detected.
> [0.000000] [ker_engine/INFO] 3 actors are still active, awaiting something. Here is their status:
> [0.000000] [ker_engine/INFO] - pid 1 (main thread@Lilibeth) simcall ActorJoin(pid:2)
> [0.000000] [ker_engine/INFO] - pid 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3)
> [0.000000] [ker_engine/INFO] - pid 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
> [0.000000] [sthread/INFO] All threads exited. Terminating the simulation.
> Process called exit when leaving - Skipping cleanups
> Process called exit when leaving - Skipping cleanups
|
