1
1
{-# LANGUAGE BangPatterns #-}
2
2
{-# LANGUAGE CPP #-}
3
- {-# LANGUAGE DeriveGeneric #-}
4
- {-# LANGUAGE DerivingStrategies #-}
5
3
{-# LANGUAGE DerivingVia #-}
6
4
{-# LANGUAGE ExistentialQuantification #-}
7
5
{-# LANGUAGE FlexibleInstances #-}
8
6
{-# LANGUAGE GADTSyntax #-}
9
- {-# LANGUAGE GeneralizedNewtypeDeriving #-}
10
- {-# LANGUAGE LambdaCase #-}
11
7
{-# LANGUAGE MultiParamTypeClasses #-}
12
8
{-# LANGUAGE NamedFieldPuns #-}
13
- {-# LANGUAGE PatternSynonyms #-}
14
9
{-# LANGUAGE RankNTypes #-}
15
10
{-# LANGUAGE ScopedTypeVariables #-}
16
11
{-# LANGUAGE TypeFamilies #-}
@@ -161,22 +156,22 @@ initialState =
161
156
where
162
157
epoch1970 = UTCTime (fromGregorian 1970 1 1 ) 0
163
158
164
- invariant :: Maybe (Thread s a ) -> SimState s a -> Bool
159
+ invariant :: Maybe (Thread s a ) -> SimState s a -> x -> x
165
160
166
161
invariant (Just running) simstate@ SimState {runqueue,threads,clocks} =
167
- not (threadBlocked running)
168
- && threadId running `Map.notMember` threads
169
- && threadId running `List.notElem` toList runqueue
170
- && threadClockId running `Map.member` clocks
171
- && invariant Nothing simstate
162
+ assert ( not (threadBlocked running) )
163
+ . assert ( threadId running `Map.notMember` threads)
164
+ . assert ( threadId running `List.notElem` runqueue)
165
+ . assert ( threadClockId running `Map.member` clocks)
166
+ . invariant Nothing simstate
172
167
173
168
invariant Nothing SimState {runqueue,threads,clocks} =
174
- all (`Map.member` threads) runqueue
175
- && and [ threadBlocked t == (threadId t `notElem` runqueue)
176
- | t <- Map. elems threads ]
177
- && toList runqueue == List. nub (toList runqueue)
178
- && and [ threadClockId t `Map.member` clocks
179
- | t <- Map. elems threads ]
169
+ assert ( all (`Map.member` threads) runqueue)
170
+ . assert ( and [ threadBlocked t == (threadId t `notElem` runqueue)
171
+ | t <- Map. elems threads ])
172
+ . assert ( toList runqueue == List. nub (toList runqueue) )
173
+ . assert ( and [ threadClockId t `Map.member` clocks
174
+ | t <- Map. elems threads ])
180
175
181
176
-- | Interpret the simulation monotonic time as a 'NominalDiffTime' since
182
177
-- the start.
@@ -202,7 +197,7 @@ schedule !thread@Thread{
202
197
nextVid, nextTmid,
203
198
curTime = time
204
199
} =
205
- assert ( invariant (Just thread) simstate) $
200
+ invariant (Just thread) simstate $
206
201
case action of
207
202
208
203
Return x -> {-# SCC "schedule.Return" #-}
@@ -423,7 +418,7 @@ schedule !thread@Thread{
423
418
return (SimTrace time tid tlbl (EventTimeoutCreated nextTmid tid expiry) trace)
424
419
425
420
RegisterDelay d k | d < 0 ->
426
- {-# SCC "schedule.NewRegisterDelay" #-} do
421
+ {-# SCC "schedule.NewRegisterDelay.1 " #-} do
427
422
! tvar <- execNewTVar nextVid
428
423
(Just $ " <<timeout " ++ show (unTimeoutId nextTmid) ++ " >>" )
429
424
True
@@ -435,7 +430,7 @@ schedule !thread@Thread{
435
430
trace)
436
431
437
432
RegisterDelay d k ->
438
- {-# SCC "schedule.NewRegisterDelay" #-} do
433
+ {-# SCC "schedule.NewRegisterDelay.2 " #-} do
439
434
! tvar <- execNewTVar nextVid
440
435
(Just $ " <<timeout " ++ show (unTimeoutId nextTmid) ++ " >>" )
441
436
False
@@ -809,7 +804,7 @@ reschedule :: SimState s a -> ST s (SimTrace a)
809
804
reschedule ! simstate@ SimState { runqueue, threads }
810
805
| Just (! tid, runqueue') <- Deque. uncons runqueue =
811
806
{-# SCC "reschedule.Just" #-}
812
- assert ( invariant Nothing simstate) $
807
+ invariant Nothing simstate $
813
808
814
809
let thread = threads Map. ! tid in
815
810
schedule thread simstate { runqueue = runqueue'
@@ -819,7 +814,7 @@ reschedule !simstate@SimState{ runqueue, threads }
819
814
-- timer event, or stop.
820
815
reschedule ! simstate@ SimState { threads, timers, curTime = time } =
821
816
{-# SCC "reschedule.Nothing" #-}
822
- assert ( invariant Nothing simstate) $
817
+ invariant Nothing simstate $
823
818
824
819
-- important to get all events that expire at this time
825
820
case removeMinimums timers of
0 commit comments