@@ -162,11 +162,12 @@ labelledThreads threadMap =
162
162
--
163
163
data TimerVars s = TimerVars ! (TVar s TimeoutState ) ! (TVar s Bool )
164
164
165
+ type RunQueue = OrdPSQ (Down ThreadId ) (Down ThreadId ) ()
165
166
166
167
-- | Internal state.
167
168
--
168
169
data SimState s a = SimState {
169
- runqueue :: ! [ ThreadId ] ,
170
+ runqueue :: ! RunQueue ,
170
171
-- | All threads other than the currently running thread: both running
171
172
-- and blocked threads.
172
173
threads :: ! (Map ThreadId (Thread s a )),
@@ -193,7 +194,7 @@ data SimState s a = SimState {
193
194
initialState :: SimState s a
194
195
initialState =
195
196
SimState {
196
- runqueue = [] ,
197
+ runqueue = PSQ. empty ,
197
198
threads = Map. empty,
198
199
curTime = Time 0 ,
199
200
timers = PSQ. empty,
@@ -213,15 +214,17 @@ invariant :: Maybe (Thread s a) -> SimState s a -> x -> x
213
214
invariant (Just running) simstate@ SimState {runqueue,threads,clocks} =
214
215
assert (not (threadBlocked running))
215
216
. assert (threadId running `Map.notMember` threads)
216
- . assert (threadId running `List.notElem ` runqueue)
217
+ . assert (not ( Down ( threadId running) `PSQ.member ` runqueue) )
217
218
. assert (threadClockId running `Map.member` clocks)
218
219
. invariant Nothing simstate
219
220
220
221
invariant Nothing SimState {runqueue,threads,clocks} =
221
- assert (all ( `Map.member` threads) runqueue)
222
- . assert (and [ (threadBlocked t || threadDone t) == ( threadId t `notElem ` runqueue)
222
+ assert (PSQ. fold' ( \ ( Down tid) _ _ a -> tid `Map.member` threads && a) True runqueue)
223
+ . assert (and [ (threadBlocked t || threadDone t) == not ( Down ( threadId t) `PSQ.member ` runqueue)
223
224
| t <- Map. elems threads ])
224
- . assert (and (zipWith (>) runqueue (drop 1 runqueue)))
225
+ . assert (and (zipWith (\ (Down tid, _, _) (Down tid', _, _) -> tid > tid')
226
+ (PSQ. toList runqueue)
227
+ (drop 1 (PSQ. toList runqueue))))
225
228
. assert (and [ threadClockId t `Map.member` clocks
226
229
| t <- Map. elems threads ])
227
230
@@ -233,8 +236,8 @@ timeSinceEpoch (Time t) = fromRational (toRational t)
233
236
234
237
-- | Insert thread into `runqueue`.
235
238
--
236
- insertThread :: Thread s a -> [ ThreadId ] -> [ ThreadId ]
237
- insertThread t = List. insertBy (comparing Down ) (threadId t )
239
+ insertThread :: Thread s a -> RunQueue -> RunQueue
240
+ insertThread Thread { threadId } = PSQ. insert ( Down threadId ) (Down threadId) ( )
238
241
239
242
240
243
-- | Schedule / run a thread.
@@ -818,7 +821,7 @@ reschedule simstate@SimState{ runqueue, threads,
818
821
curTime= time
819
822
} =
820
823
fmap (SimPORTrace time tid tstep Nothing (EventReschedule control)) $
821
- assert (tid `elem ` runqueue) $
824
+ assert (Down tid `PSQ.member ` runqueue) $
822
825
assert (tid `Map.member` threads) $
823
826
invariant Nothing simstate $
824
827
let thread = threads Map. ! tid in
@@ -831,12 +834,13 @@ reschedule simstate@SimState{ runqueue, threads,
831
834
++ " actual step: " ++ show (threadStep thread)++ " \n "
832
835
++ " Thread:\n " ++ show thread ++ " \n "
833
836
else
834
- schedule thread simstate { runqueue = List . delete tid runqueue
837
+ schedule thread simstate { runqueue = PSQ . delete ( Down tid) runqueue
835
838
, threads = Map. delete tid threads }
836
839
837
840
-- When there is no current running thread but the runqueue is non-empty then
838
841
-- schedule the next one to run.
839
- reschedule simstate@ SimState { runqueue = tid: runqueue', threads } =
842
+ reschedule simstate@ SimState { runqueue, threads }
843
+ | Just (Down tid, _, _, runqueue') <- PSQ. minView runqueue =
840
844
invariant Nothing simstate $
841
845
842
846
let thread = threads Map. ! tid in
@@ -845,7 +849,7 @@ reschedule simstate@SimState{ runqueue = tid:runqueue', threads } =
845
849
846
850
-- But when there are no runnable threads, we advance the time to the next
847
851
-- timer event, or stop.
848
- reschedule simstate@ SimState { runqueue = [] , threads, timers, curTime = time, races } =
852
+ reschedule simstate@ SimState { threads, timers, curTime = time, races } =
849
853
invariant Nothing simstate $
850
854
851
855
-- time is moving on
0 commit comments