@@ -1057,7 +1057,9 @@ execAtomically time tid tlbl nextVid0 action0 k0 =
1057
1057
-> ST s (SimTrace c )
1058
1058
go ctl ! read ! written writtenSeq createdSeq ! nextVid action = assert localInvariant $
1059
1059
case action of
1060
- ReturnStm x -> case ctl of
1060
+ ReturnStm x ->
1061
+ {-# SCC "execAtomically.go.ReturnStm" #-}
1062
+ case ctl of
1061
1063
AtomicallyFrame -> do
1062
1064
-- Trace each created TVar
1063
1065
ds <- traverse (\ (SomeTVar tvar) -> traceTVarST tvar True
@@ -1112,78 +1114,91 @@ execAtomically time tid tlbl nextVid0 action0 k0 =
1112
1114
-- Continue with the k continuation
1113
1115
go ctl' read written' writtenSeq' createdSeq' nextVid (k x)
1114
1116
1115
- ThrowStm e -> do
1117
+ ThrowStm e ->
1118
+ {-# SCC "execAtomically.go.ThrowStm" #-} do
1116
1119
-- Revert all the TVar writes
1117
1120
traverse_ (\ (SomeTVar tvar) -> revertTVar tvar) written
1118
1121
k0 $ StmTxAborted (Map. elems read ) (toException e)
1119
1122
1120
- Retry -> case ctl of
1123
+ Retry ->
1124
+ {-# SCC "execAtomically.go.Retry" #-}
1125
+ case ctl of
1121
1126
AtomicallyFrame -> do
1122
1127
-- Revert all the TVar writes
1123
1128
traverse_ (\ (SomeTVar tvar) -> revertTVar tvar) written
1124
1129
-- Return vars read, so the thread can block on them
1125
1130
k0 $ StmTxBlocked (Map. elems read )
1126
1131
1127
- OrElseLeftFrame b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
1132
+ OrElseLeftFrame b k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
1133
+ {-# SCC "execAtomically.go.OrElseLeftFrame" #-} do
1128
1134
-- Revert all the TVar writes within this orElse
1129
1135
traverse_ (\ (SomeTVar tvar) -> revertTVar tvar) written
1130
1136
-- Execute the orElse right hand with an empty written set
1131
1137
let ctl'' = OrElseRightFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl'
1132
1138
go ctl'' read Map. empty [] [] nextVid b
1133
1139
1134
- OrElseRightFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
1140
+ OrElseRightFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
1141
+ {-# SCC "execAtomically.go.OrElseRightFrame" #-} do
1135
1142
-- Revert all the TVar writes within this orElse branch
1136
1143
traverse_ (\ (SomeTVar tvar) -> revertTVar tvar) written
1137
1144
-- Skip the continuation and propagate the retry into the outer frame
1138
1145
-- using the written set for the outer frame
1139
1146
go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry
1140
1147
1141
- OrElse a b k -> do
1148
+ OrElse a b k ->
1149
+ {-# SCC "execAtomically.go.OrElse" #-} do
1142
1150
-- Execute the left side in a new frame with an empty written set
1143
1151
let ctl' = OrElseLeftFrame b k written writtenSeq createdSeq ctl
1144
1152
go ctl' read Map. empty [] [] nextVid a
1145
1153
1146
- NewTVar ! mbLabel x k -> do
1154
+ NewTVar ! mbLabel x k ->
1155
+ {-# SCC "execAtomically.go.NewTVar" #-} do
1147
1156
v <- execNewTVar nextVid mbLabel x
1148
1157
-- record a write to the TVar so we know to update its VClock
1149
1158
let written' = Map. insert (tvarId v) (SomeTVar v) written
1150
1159
-- save the value: it will be committed or reverted
1151
1160
saveTVar v
1152
1161
go ctl read written' writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k v)
1153
1162
1154
- LabelTVar ! label tvar k -> do
1163
+ LabelTVar ! label tvar k ->
1164
+ {-# SCC "execAtomically.go.LabelTVar" #-} do
1155
1165
writeSTRef (tvarLabel tvar) $! (Just label)
1156
1166
go ctl read written writtenSeq createdSeq nextVid k
1157
1167
1158
- TraceTVar tvar f k -> do
1168
+ TraceTVar tvar f k ->
1169
+ {-# SCC "execAtomically.go.TraceTVar" #-} do
1159
1170
writeSTRef (tvarTrace tvar) (Just f)
1160
1171
go ctl read written writtenSeq createdSeq nextVid k
1161
1172
1162
1173
ReadTVar v k
1163
- | tvarId v `Map.member` read || tvarId v `Map.member` written -> do
1174
+ | tvarId v `Map.member` read || tvarId v `Map.member` written ->
1175
+ {-# SCC "execAtomically.go.ReadTVar" #-} do
1164
1176
x <- execReadTVar v
1165
1177
go ctl read written writtenSeq createdSeq nextVid (k x)
1166
- | otherwise -> do
1178
+ | otherwise ->
1179
+ {-# SCC "execAtomically.go.ReadTVar" #-} do
1167
1180
x <- execReadTVar v
1168
1181
let read' = Map. insert (tvarId v) (SomeTVar v) read
1169
1182
go ctl read' written writtenSeq createdSeq nextVid (k x)
1170
1183
1171
1184
WriteTVar v x k
1172
- | tvarId v `Map.member` written -> do
1173
- execWriteTVar v x
1185
+ | tvarId v `Map.member` written ->
1186
+ {-# SCC "execAtomically.go.WriteTVar" #-} do
1174
1187
go ctl read written writtenSeq createdSeq nextVid k
1175
- | otherwise -> do
1176
- saveTVar v
1188
+ | otherwise ->
1189
+ {-# SCC "execAtomically.go.WriteTVar" #-} do
1177
1190
execWriteTVar v x
1178
1191
let written' = Map. insert (tvarId v) (SomeTVar v) written
1179
1192
go ctl read written' (SomeTVar v : writtenSeq) createdSeq nextVid k
1180
1193
1181
- SayStm msg k -> do
1194
+ SayStm msg k ->
1195
+ {-# SCC "execAtomically.go.SayStm" #-} do
1182
1196
trace <- go ctl read written writtenSeq createdSeq nextVid k
1183
1197
-- TODO: step
1184
1198
return $ SimPORTrace time tid (- 1 ) tlbl (EventSay msg) trace
1185
1199
1186
- OutputStm x k -> do
1200
+ OutputStm x k ->
1201
+ {-# SCC "execAtomically.go.OutputStm" #-} do
1187
1202
trace <- go ctl read written writtenSeq createdSeq nextVid k
1188
1203
-- TODO: step
1189
1204
return $ SimPORTrace time tid (- 1 ) tlbl (EventLog x) trace
0 commit comments