From: Martin Quinson Date: Sun, 16 Oct 2022 10:42:24 +0000 (+0200) Subject: Rename the transitions so that asynchronous ones clearly appear so X-Git-Tag: v3.34~774 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/87ab6a5d123f0032675234e655f79dac2bc78beb Rename the transitions so that asynchronous ones clearly appear so --- diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh index 2e610e7410..0ce52a1c98 100644 --- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh +++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh @@ -2,7 +2,7 @@ $ ${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] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execution came to an end at 1;1;0 (state: 3, depth: 3) > [Checker] Backtracking from 1;1;0 @@ -10,8 +10,8 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt $ ${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] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) -> [Checker] Execute 2: BARRIER_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) +> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) > [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5) @@ -20,19 +20,19 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] BARRIER_WAIT(barrier: 0) (state=3) > [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [Checker] Dependent Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] BARRIER_WAIT(barrier: 0) (state=3) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] Backtracking from 1;2 > [Checker] DFS exploration ended. 5 unique states visited; 2 backtracks (7 transition replays, 1 states visited overall) $ ${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] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) -> [Checker] Execute 2: BARRIER_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) -> [Checker] Execute 3: BARRIER_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) +> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves) +> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves) > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves) > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves) @@ -48,19 +48,19 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [Checker] BARRIER_WAIT(barrier: 0) (state=5) > [Checker] Dependent Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] BARRIER_WAIT(barrier: 0) (state=5) > [Checker] Dependent Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] BARRIER_WAIT(barrier: 0) (state=4) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=2) -> [Checker] BARRIER_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_LOCK(barrier: 0) (state=3) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3) > [Checker] Backtracking from 1;2;3 > [Checker] INDEPENDENT Transitions: -> [Checker] BARRIER_LOCK(barrier: 0) (state=1) -> [Checker] BARRIER_LOCK(barrier: 0) (state=2) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1) +> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2) > [Checker] DFS exploration ended. 7 unique states visited; 2 backtracks (10 transition replays, 2 states visited overall) diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh index 5bec63ffe3..2469cc31a9 100644 --- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh +++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh @@ -5,25 +5,25 @@ p This file tests the dependencies between MUTEX transitions $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" > [App ] Configuration change: Set 'actors' to '1' > [Checker] Start a DFS exploration. Reduction is: dpor. -> [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves) -> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 4, state: 4, 0 interleaves) +> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 4, state: 4, 0 interleaves) > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 6, 0 interleaves) > [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7) > [Checker] Backtracking from 1;1;1;2;2;2;0 > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=2) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:1) (state=1) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) -> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves) -> [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 2, state: 8, 0 interleaves) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 2, state: 8, 0 interleaves) > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 3, state: 9, 0 interleaves) > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:1) (stack depth: 4, state: 10, 0 interleaves) > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 5, state: 11, 0 interleaves) @@ -35,59 +35,59 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=11) > [Checker] Backtracking from 2;1;2;2 > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=8) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=8) > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=9) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=1) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=8) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=8) > [Checker] DFS exploration ended. 13 unique states visited; 3 backtracks (18 transition replays, 3 states visited overall) $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" > [App ] Configuration change: Set 'actors' to '2' > [Checker] Start a DFS exploration. Reduction is: dpor. -> [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves) -> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 4, state: 4, 0 interleaves) +> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 4, state: 4, 0 interleaves) > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 6, 0 interleaves) -> [Checker] Execute 3: MUTEX_LOCK(mutex: 1, owner:3) (stack depth: 7, state: 7, 0 interleaves) +> [Checker] Execute 3: MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (stack depth: 7, state: 7, 0 interleaves) > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 8, state: 8, 0 interleaves) > [Checker] Execute 3: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 9, state: 9, 0 interleaves) -> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 10, 0 interleaves) +> [Checker] Execute 4: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 10, 0 interleaves) > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 11, 0 interleaves) > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 12, 0 interleaves) > [Checker] Execution came to an end at 1;1;1;2;2;2;3;3;3;4;4;4;0 (state: 13, depth: 13) > [Checker] Backtracking from 1;1;1;2;2;2;3;3;3;4;4;4;0 > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 1, owner:-1) (state=9) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=10) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=10) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 1, owner:3) (state=8) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=10) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=10) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=10) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=10) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=6) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=5) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=2) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:1) (state=1) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=7) -> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 7, 0 interleaves) -> [Checker] Execute 3: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 8, state: 14, 0 interleaves) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=7) +> [Checker] Execute 4: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 7, 0 interleaves) +> [Checker] Execute 3: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 8, state: 14, 0 interleaves) > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 9, state: 15, 0 interleaves) > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:3) (stack depth: 10, state: 16, 0 interleaves) > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 11, state: 17, 0 interleaves) @@ -99,81 +99,81 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] MUTEX_WAIT(mutex: 1, owner:3) (state=17) > [Checker] Backtracking from 1;1;1;2;2;2;4;3;4;4 > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=14) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=14) > [Checker] MUTEX_WAIT(mutex: 1, owner:4) (state=15) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=14) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=14) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=6) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=5) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=2) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:1) (state=1) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=7) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=7) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=3) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=2) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:1) (state=1) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=4) -> [Checker] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves) -> [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 2, state: 20, 0 interleaves) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:1) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=4) +> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (stack depth: 2, state: 20, 0 interleaves) > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner:2) (stack depth: 3, state: 21, 0 interleaves) > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner:1) (stack depth: 4, state: 22, 0 interleaves) > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 5, state: 23, 0 interleaves) > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 6, state: 24, 0 interleaves) -> [Checker] Execute 3: MUTEX_LOCK(mutex: 1, owner:3) (stack depth: 7, state: 25, 0 interleaves) +> [Checker] Execute 3: MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (stack depth: 7, state: 25, 0 interleaves) > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 8, state: 26, 0 interleaves) > [Checker] Execute 3: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 9, state: 27, 0 interleaves) -> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 28, 0 interleaves) +> [Checker] Execute 4: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 10, state: 28, 0 interleaves) > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 11, state: 29, 0 interleaves) > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:-1) (stack depth: 12, state: 30, 0 interleaves) > [Checker] Execution came to an end at 2;1;2;2;1;1;3;3;3;4;4;4;0 (state: 31, depth: 13) > [Checker] Backtracking from 2;1;2;2;1;1;3;3;3;4;4;4;0 > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 1, owner:-1) (state=27) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=28) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=28) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 1, owner:3) (state=26) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=28) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=28) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=28) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=28) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=24) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=23) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:1) (state=22) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=21) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=20) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=20) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=1) -> [Checker] MUTEX_LOCK(mutex: 1, owner:3) (state=25) -> [Checker] Execute 4: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 25, 0 interleaves) -> [Checker] Execute 3: MUTEX_LOCK(mutex: 1, owner:4) (stack depth: 8, state: 32, 0 interleaves) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:3) (state=25) +> [Checker] Execute 4: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 7, state: 25, 0 interleaves) +> [Checker] Execute 3: MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (stack depth: 8, state: 32, 0 interleaves) > [Checker] Execute 4: MUTEX_WAIT(mutex: 1, owner:4) (stack depth: 9, state: 33, 0 interleaves) > [Checker] Execute 4: MUTEX_UNLOCK(mutex: 1, owner:3) (stack depth: 10, state: 34, 0 interleaves) > [Checker] Execute 3: MUTEX_WAIT(mutex: 1, owner:3) (stack depth: 11, state: 35, 0 interleaves) @@ -185,39 +185,39 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt > [Checker] MUTEX_WAIT(mutex: 1, owner:3) (state=35) > [Checker] Backtracking from 2;1;2;2;1;1;4;3;4;4 > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=32) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=32) > [Checker] MUTEX_WAIT(mutex: 1, owner:4) (state=33) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=32) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=32) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:-1) (state=24) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=23) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:1) (state=22) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] INDEPENDENT Transitions: > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=21) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=20) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=20) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=1) -> [Checker] MUTEX_LOCK(mutex: 1, owner:4) (state=25) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 1, owner:4) (state=25) > [Checker] Dependent Transitions: > [Checker] MUTEX_UNLOCK(mutex: 0, owner:1) (state=22) > [Checker] MUTEX_WAIT(mutex: 0, owner:1) (state=23) > [Checker] Backtracking from 2;1;2;2 > [Checker] INDEPENDENT Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=20) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=20) > [Checker] MUTEX_WAIT(mutex: 0, owner:2) (state=21) > [Checker] Dependent Transitions: -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=1) -> [Checker] MUTEX_LOCK(mutex: 0, owner:2) (state=20) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=1) +> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner:2) (state=20) > [Checker] DFS exploration ended. 37 unique states visited; 7 backtracks (76 transition replays, 33 states visited overall) $ ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical diff --git a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh index d63b175385..1fe9bddd3f 100644 --- a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh +++ b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh @@ -2,78 +2,78 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n" > [Checker] Start a DFS exploration. Reduction is: dpor. -> [Checker] Execute 1: SEM_LOCK(semaphore: 0) (stack depth: 1, state: 1, 0 interleaves) +> [Checker] Execute 1: SEM_ASYNC_LOCK(semaphore: 0) (stack depth: 1, state: 1, 0 interleaves) > [Checker] Execute 1: SEM_WAIT(semaphore: 0, granted: yes) (stack depth: 2, state: 2, 0 interleaves) > [Checker] Execute 1: SEM_UNLOCK(semaphore: 1) (stack depth: 3, state: 3, 0 interleaves) -> [Checker] Execute 1: SEM_LOCK(semaphore: 0) (stack depth: 4, state: 4, 0 interleaves) -> [Checker] Execute 2: SEM_LOCK(semaphore: 1) (stack depth: 5, state: 5, 0 interleaves) +> [Checker] Execute 1: SEM_ASYNC_LOCK(semaphore: 0) (stack depth: 4, state: 4, 0 interleaves) +> [Checker] Execute 2: SEM_ASYNC_LOCK(semaphore: 1) (stack depth: 5, state: 5, 0 interleaves) > [Checker] Execute 2: SEM_WAIT(semaphore: 1, granted: yes) (stack depth: 6, state: 6, 0 interleaves) > [Checker] Execute 2: SEM_UNLOCK(semaphore: 0) (stack depth: 7, state: 7, 0 interleaves) > [Checker] Execute 1: SEM_WAIT(semaphore: 0, granted: yes) (stack depth: 8, state: 8, 0 interleaves) > [Checker] Execute 1: SEM_UNLOCK(semaphore: 1) (stack depth: 9, state: 9, 0 interleaves) -> [Checker] Execute 1: SEM_LOCK(semaphore: 0) (stack depth: 10, state: 10, 0 interleaves) -> [Checker] Execute 2: SEM_LOCK(semaphore: 1) (stack depth: 11, state: 11, 0 interleaves) +> [Checker] Execute 1: SEM_ASYNC_LOCK(semaphore: 0) (stack depth: 10, state: 10, 0 interleaves) +> [Checker] Execute 2: SEM_ASYNC_LOCK(semaphore: 1) (stack depth: 11, state: 11, 0 interleaves) > [Checker] Execute 2: SEM_WAIT(semaphore: 1, granted: yes) (stack depth: 12, state: 12, 0 interleaves) > [Checker] Execute 2: SEM_UNLOCK(semaphore: 0) (stack depth: 13, state: 13, 0 interleaves) > [Checker] Execute 1: SEM_WAIT(semaphore: 0, granted: yes) (stack depth: 14, state: 14, 0 interleaves) > [Checker] Execute 1: SEM_UNLOCK(semaphore: 1) (stack depth: 15, state: 15, 0 interleaves) -> [Checker] Execute 1: SEM_LOCK(semaphore: 0) (stack depth: 16, state: 16, 0 interleaves) -> [Checker] Execute 2: SEM_LOCK(semaphore: 1) (stack depth: 17, state: 17, 0 interleaves) +> [Checker] Execute 1: SEM_ASYNC_LOCK(semaphore: 0) (stack depth: 16, state: 16, 0 interleaves) +> [Checker] Execute 2: SEM_ASYNC_LOCK(semaphore: 1) (stack depth: 17, state: 17, 0 interleaves) > [Checker] Execute 2: SEM_WAIT(semaphore: 1, granted: yes) (stack depth: 18, state: 18, 0 interleaves) > [Checker] Execute 2: SEM_UNLOCK(semaphore: 0) (stack depth: 19, state: 19, 0 interleaves) > [Checker] Execute 1: SEM_WAIT(semaphore: 0, granted: yes) (stack depth: 20, state: 20, 0 interleaves) > [Checker] Execute 1: SEM_UNLOCK(semaphore: 1) (stack depth: 21, state: 21, 0 interleaves) -> [Checker] Execute 2: SEM_LOCK(semaphore: 1) (stack depth: 22, state: 22, 0 interleaves) +> [Checker] Execute 2: SEM_ASYNC_LOCK(semaphore: 1) (stack depth: 22, state: 22, 0 interleaves) > [Checker] Execute 2: SEM_WAIT(semaphore: 1, granted: yes) (stack depth: 23, state: 23, 0 interleaves) > [Checker] Execute 2: SEM_UNLOCK(semaphore: 0) (stack depth: 24, state: 24, 0 interleaves) > [Checker] Execution came to an end at 1;1;1;1;2;2;2;1;1;1;2;2;2;1;1;1;2;2;2;1;1;2;2;2;0 (state: 25, depth: 25) > [Checker] Backtracking from 1;1;1;1;2;2;2;1;1;1;2;2;2;1;1;1;2;2;2;1;1;2;2;2;0 > [Checker] INDEPENDENT Transitions: > [Checker] SEM_UNLOCK(semaphore: 1) (state=21) -> [Checker] SEM_LOCK(semaphore: 1) (state=22) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=22) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=20) -> [Checker] SEM_LOCK(semaphore: 1) (state=22) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=22) > [Checker] Dependent Transitions: > [Checker] SEM_UNLOCK(semaphore: 0) (state=19) > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=20) > [Checker] Backtracking from 1;1;1;1;2;2;2;1;1;1;2;2;2;1;1;1;2;2;2 > [Checker] INDEPENDENT Transitions: -> [Checker] SEM_LOCK(semaphore: 0) (state=16) -> [Checker] SEM_LOCK(semaphore: 1) (state=17) +> [Checker] SEM_ASYNC_LOCK(semaphore: 0) (state=16) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=17) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_UNLOCK(semaphore: 1) (state=15) -> [Checker] SEM_LOCK(semaphore: 1) (state=17) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=17) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=14) -> [Checker] SEM_LOCK(semaphore: 1) (state=17) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=17) > [Checker] Dependent Transitions: > [Checker] SEM_UNLOCK(semaphore: 0) (state=13) > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=14) > [Checker] Backtracking from 1;1;1;1;2;2;2;1;1;1;2;2;2 > [Checker] INDEPENDENT Transitions: -> [Checker] SEM_LOCK(semaphore: 0) (state=10) -> [Checker] SEM_LOCK(semaphore: 1) (state=11) +> [Checker] SEM_ASYNC_LOCK(semaphore: 0) (state=10) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=11) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_UNLOCK(semaphore: 1) (state=9) -> [Checker] SEM_LOCK(semaphore: 1) (state=11) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=11) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=8) -> [Checker] SEM_LOCK(semaphore: 1) (state=11) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=11) > [Checker] Dependent Transitions: > [Checker] SEM_UNLOCK(semaphore: 0) (state=7) > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=8) > [Checker] Backtracking from 1;1;1;1;2;2;2 > [Checker] INDEPENDENT Transitions: -> [Checker] SEM_LOCK(semaphore: 0) (state=4) -> [Checker] SEM_LOCK(semaphore: 1) (state=5) +> [Checker] SEM_ASYNC_LOCK(semaphore: 0) (state=4) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=5) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_UNLOCK(semaphore: 1) (state=3) -> [Checker] SEM_LOCK(semaphore: 1) (state=5) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=5) > [Checker] INDEPENDENT Transitions: > [Checker] SEM_WAIT(semaphore: 0, granted: yes) (state=2) -> [Checker] SEM_LOCK(semaphore: 1) (state=5) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=5) > [Checker] INDEPENDENT Transitions: -> [Checker] SEM_LOCK(semaphore: 0) (state=1) -> [Checker] SEM_LOCK(semaphore: 1) (state=5) +> [Checker] SEM_ASYNC_LOCK(semaphore: 0) (state=1) +> [Checker] SEM_ASYNC_LOCK(semaphore: 1) (state=5) > [Checker] DFS exploration ended. 25 unique states visited; 4 backtracks (64 transition replays, 36 states visited overall) diff --git a/src/kernel/actor/CommObserver.cpp b/src/kernel/actor/CommObserver.cpp index e15d6aa877..8f86d94cb9 100644 --- a/src/kernel/actor/CommObserver.cpp +++ b/src/kernel/actor/CommObserver.cpp @@ -143,7 +143,7 @@ void ActivityWaitanySimcall::prepare(int times_considered) void CommIsendSimcall::serialize(std::stringstream& stream) const { - stream << (short)mc::Transition::Type::COMM_SEND << ' '; + stream << (short)mc::Transition::Type::COMM_ASYNC_SEND << ' '; stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' ' << src_buff_size_ << ' ' << tag_; XBT_DEBUG("SendObserver comm:%p mbox:%u buff:%p size:%zu tag:%d", comm_, mbox_->get_id(), src_buff_, src_buff_size_, @@ -152,7 +152,7 @@ void CommIsendSimcall::serialize(std::stringstream& stream) const void CommIrecvSimcall::serialize(std::stringstream& stream) const { - stream << (short)mc::Transition::Type::COMM_RECV << ' '; + stream << (short)mc::Transition::Type::COMM_ASYNC_RECV << ' '; stream << (uintptr_t)comm_ << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_; XBT_DEBUG("RecvObserver comm:%p mbox:%u buff:%p tag:%d", comm_, mbox_->get_id(), dst_buff_, tag_); } diff --git a/src/kernel/actor/SynchroObserver.cpp b/src/kernel/actor/SynchroObserver.cpp index 5e5ca9d6b6..96d75c7c63 100644 --- a/src/kernel/actor/SynchroObserver.cpp +++ b/src/kernel/actor/SynchroObserver.cpp @@ -63,7 +63,7 @@ void SemaphoreAcquisitionObserver::serialize(std::stringstream& stream) const BarrierObserver::BarrierObserver(ActorImpl* actor, mc::Transition::Type type, activity::BarrierImpl* bar) : ResultingSimcall(actor, false), type_(type), barrier_(bar), timeout_(-1) { - xbt_assert(type_ == mc::Transition::Type::BARRIER_LOCK); + xbt_assert(type_ == mc::Transition::Type::BARRIER_ASYNC_LOCK); } BarrierObserver::BarrierObserver(ActorImpl* actor, mc::Transition::Type type, activity::BarrierAcquisitionImpl* acqui, double timeout) @@ -78,7 +78,7 @@ void BarrierObserver::serialize(std::stringstream& stream) const } bool BarrierObserver::is_enabled() { - return type_ == mc::Transition::Type::BARRIER_LOCK || + return type_ == mc::Transition::Type::BARRIER_ASYNC_LOCK || (type_ == mc::Transition::Type::BARRIER_WAIT && acquisition_ != nullptr && acquisition_->granted_); } diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index bb9a5b2f94..031416a2ad 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -233,7 +233,7 @@ void CommDetExtension::get_comm_pattern(const Transition* transition) auto pattern = std::make_unique(); pattern->index = initial_pattern.index_comm + incomplete_pattern.size(); - if (transition->type_ == Transition::Type::COMM_SEND) { + if (transition->type_ == Transition::Type::COMM_ASYNC_SEND) { auto* send = static_cast(transition); pattern->type = PatternCommunicationType::send; @@ -242,7 +242,7 @@ void CommDetExtension::get_comm_pattern(const Transition* transition) // FIXME: Detached sends should be enforced when the receive is waited - } else if (transition->type_ == Transition::Type::COMM_RECV) { + } else if (transition->type_ == Transition::Type::COMM_ASYNC_RECV) { auto* recv = static_cast(transition); pattern->type = PatternCommunicationType::receive; @@ -290,8 +290,8 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) return; switch (transition->type_) { - case Transition::Type::COMM_SEND: - case Transition::Type::COMM_RECV: + case Transition::Type::COMM_ASYNC_SEND: + case Transition::Type::COMM_ASYNC_RECV: get_comm_pattern(transition); break; case Transition::Type::COMM_WAIT: diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 520992744c..b10abd263d 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -59,13 +59,13 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri xbt_assert(stream >> type); switch (auto simcall = static_cast(type)) { - case Transition::Type::BARRIER_LOCK: + case Transition::Type::BARRIER_ASYNC_LOCK: case Transition::Type::BARRIER_WAIT: return new BarrierTransition(issuer, times_considered, simcall, stream); - case Transition::Type::COMM_RECV: + case Transition::Type::COMM_ASYNC_RECV: return new CommRecvTransition(issuer, times_considered, stream); - case Transition::Type::COMM_SEND: + case Transition::Type::COMM_ASYNC_SEND: return new CommSendTransition(issuer, times_considered, stream); case Transition::Type::COMM_TEST: return new CommTestTransition(issuer, times_considered, stream); @@ -81,13 +81,13 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri return new RandomTransition(issuer, times_considered, stream); case Transition::Type::MUTEX_TRYLOCK: - case Transition::Type::MUTEX_LOCK: + case Transition::Type::MUTEX_ASYNC_LOCK: case Transition::Type::MUTEX_TEST: case Transition::Type::MUTEX_WAIT: case Transition::Type::MUTEX_UNLOCK: return new MutexTransition(issuer, times_considered, simcall, stream); - case Transition::Type::SEM_LOCK: + case Transition::Type::SEM_ASYNC_LOCK: case Transition::Type::SEM_UNLOCK: case Transition::Type::SEM_WAIT: return new SemaphoreTransition(issuer, times_considered, simcall, stream); diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp index 91f02b9b0f..47a4b08a42 100644 --- a/src/mc/transition/Transition.hpp +++ b/src/mc/transition/Transition.hpp @@ -31,13 +31,12 @@ class Transition { public: /* Ordering is important here. depends() implementations only consider subsequent types in this ordering */ - XBT_DECLARE_ENUM_CLASS(Type, RANDOM, /* First because indep with anybody */ - TESTANY, WAITANY, /* high priority because they can rewrite themselves to *_WAIT */ - BARRIER_LOCK, BARRIER_WAIT, /* BARRIER transitions sorted alphabetically */ - COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */ - MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */ - SEM_LOCK, SEM_UNLOCK, SEM_WAIT, /* alphabetical ordering of SEM transitions */ - ACTOR_JOIN, + XBT_DECLARE_ENUM_CLASS(Type, RANDOM, ACTOR_JOIN, /* First because indep with anybody */ + TESTANY, WAITANY, /* high priority because they can rewrite themselves to *_WAIT */ + BARRIER_ASYNC_LOCK, BARRIER_WAIT, /* BARRIER transitions sorted alphabetically */ + COMM_ASYNC_RECV, COMM_ASYNC_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */ + MUTEX_ASYNC_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */ + SEM_ASYNC_LOCK, SEM_UNLOCK, SEM_WAIT, /* alphabetical ordering of SEM transitions */ /* UNKNOWN must be last */ UNKNOWN); Type type_ = Type::UNKNOWN; diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index 0d48bcf7db..a25b10aa68 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -102,7 +102,7 @@ bool CommTestTransition::depends(const Transition* other) const } CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream) - : Transition(Type::COMM_RECV, issuer, times_considered) + : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered) { xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_); } @@ -155,7 +155,7 @@ bool CommRecvTransition::depends(const Transition* other) const } CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream) - : Transition(Type::COMM_SEND, issuer, times_considered) + : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered) { xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_); XBT_DEBUG("SendTransition comm:%" PRIxPTR " mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_); diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index 99aa4c2028..09de8eeece 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -34,7 +34,7 @@ bool BarrierTransition::depends(const Transition* o) const return false; // LOCK indep LOCK: requests are not ordered in a barrier - if (type_ == Type::BARRIER_LOCK && other->type_ == Type::BARRIER_LOCK) + if (type_ == Type::BARRIER_ASYNC_LOCK && other->type_ == Type::BARRIER_ASYNC_LOCK) return false; // WAIT indep WAIT: requests are not ordered @@ -72,12 +72,12 @@ bool MutexTransition::depends(const Transition* o) const // Theorem 4.4.11: LOCK indep TEST/WAIT. // If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it. - if (type_ == Type::MUTEX_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT)) + if (type_ == Type::MUTEX_ASYNC_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT)) return false; // Theorem 4.4.8: LOCK indep UNLOCK. // pop_front and push_back are independent. - if (type_ == Type::MUTEX_LOCK && other->type_ == Type::MUTEX_UNLOCK) + if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK) return false; // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a @@ -100,7 +100,7 @@ bool MutexTransition::depends(const Transition* o) const std::string SemaphoreTransition::to_string(bool verbose) const { - if (type_ == Type::SEM_LOCK || type_ == Type::SEM_UNLOCK) + if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK) return xbt::string_printf("%s(semaphore: %" PRIxPTR ")", Transition::to_c_str(type_), sem_); if (type_ == Type::SEM_WAIT) return xbt::string_printf("%s(semaphore: %" PRIxPTR ", granted: %s)", Transition::to_c_str(type_), sem_, @@ -122,12 +122,12 @@ bool SemaphoreTransition::depends(const Transition* o) const return false; // LOCK indep UNLOCK: pop_front and push_back are independent. - if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_UNLOCK) + if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_UNLOCK) return false; // LOCK indep WAIT: If both enabled, ordering has no impact on the result. If WAIT is not enabled, LOCK won't enable // it. - if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_WAIT) + if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_WAIT) return false; // UNLOCK indep UNLOCK: ordering of two pop_front has no impact diff --git a/src/s4u/s4u_Barrier.cpp b/src/s4u/s4u_Barrier.cpp index b7f0c99ef8..f7104fb009 100644 --- a/src/s4u/s4u_Barrier.cpp +++ b/src/s4u/s4u_Barrier.cpp @@ -36,7 +36,7 @@ int Barrier::wait() kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self(); if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency - kernel::actor::BarrierObserver lock_observer{issuer, mc::Transition::Type::BARRIER_LOCK, pimpl_}; + kernel::actor::BarrierObserver lock_observer{issuer, mc::Transition::Type::BARRIER_ASYNC_LOCK, pimpl_}; auto acquisition = kernel::actor::simcall_answered([issuer, this] { return pimpl_->acquire_async(issuer); }, &lock_observer); diff --git a/src/s4u/s4u_Mutex.cpp b/src/s4u/s4u_Mutex.cpp index 0adc7f026c..6eb656704e 100644 --- a/src/s4u/s4u_Mutex.cpp +++ b/src/s4u/s4u_Mutex.cpp @@ -19,7 +19,7 @@ void Mutex::lock() kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self(); if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency - kernel::actor::MutexObserver lock_observer{issuer, mc::Transition::Type::MUTEX_LOCK, pimpl_}; + kernel::actor::MutexObserver lock_observer{issuer, mc::Transition::Type::MUTEX_ASYNC_LOCK, pimpl_}; auto acquisition = kernel::actor::simcall_answered([issuer, this] { return pimpl_->lock_async(issuer); }, &lock_observer); diff --git a/src/s4u/s4u_Semaphore.cpp b/src/s4u/s4u_Semaphore.cpp index c2021e5626..d8f64714f3 100644 --- a/src/s4u/s4u_Semaphore.cpp +++ b/src/s4u/s4u_Semaphore.cpp @@ -29,7 +29,7 @@ bool Semaphore::acquire_timeout(double timeout) kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self(); if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency - kernel::actor::SemaphoreObserver lock_observer{issuer, mc::Transition::Type::SEM_LOCK, pimpl_}; + kernel::actor::SemaphoreObserver lock_observer{issuer, mc::Transition::Type::SEM_ASYNC_LOCK, pimpl_}; auto acquisition = kernel::actor::simcall_answered([issuer, this] { return pimpl_->acquire_async(issuer); }, &lock_observer);