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 2e610e7..0ce52a1 100644 (file)
--- 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 5bec63f..2469cc3 100644 (file)
--- 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 d63b175..1fe9bdd 100644 (file)
--- 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 e15d6aa..8f86d94 100644 (file)
--- 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 5e5ca9d..96d75c7 100644 (file)
--- 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 bb9a5b2..031416a 100644 (file)
--- 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<PatternCommunication>();
   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<const CommSendTransition*>(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<const CommRecvTransition*>(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 5209927..b10abd2 100644 (file)
--- 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<Transition::Type>(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 91f02b9..47a4b08 100644 (file)
--- 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 0d48bcf..a25b10a 100644 (file)
--- 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 99aa4c2..09de8ee 100644 (file)
--- 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 b7f0c99..f7104fb 100644 (file)
--- 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 0adc7f0..6eb6567 100644 (file)
--- 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 c2021e5..d8f6471 100644 (file)
--- 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);