@@ -19,13 +19,14 @@ void ShieldInit(Shield shield)
1919{
2020 shield -> inside = FALSE;
2121 shield -> suspended = FALSE;
22- shield -> queuePending = FALSE;
2322 shield -> queue = NULL ;
2423 shield -> length = 0 ;
2524 shield -> next = 0 ;
2625 shield -> limit = 0 ;
2726 shield -> depth = 0 ;
2827 shield -> unsynced = 0 ;
28+ shield -> unqueued = 0 ;
29+ shield -> synced = 0 ;
2930 shield -> holds = 0 ;
3031 shield -> sig = ShieldSig ;
3132}
@@ -55,6 +56,8 @@ void ShieldFinish(Shield shield)
5556
5657 AVER (shield -> depth == 0 );
5758 AVER (shield -> unsynced == 0 );
59+ AVER (shield -> unqueued == 0 );
60+ AVER (shield -> synced == 0 );
5861 AVER (shield -> holds == 0 );
5962 shield -> sig = SigInvalid ;
6063}
@@ -69,6 +72,8 @@ Bool ShieldCheck(Shield shield)
6972 CHECKL (shield -> queue == NULL || shield -> length > 0 );
7073 CHECKL (shield -> limit <= shield -> length );
7174 CHECKL (shield -> next <= shield -> limit );
75+ CHECKL (shield -> unqueued <= shield -> unsynced );
76+ CHECKL (shield -> synced <= shield -> limit );
7277
7378 /* The mutator is not suspended while outside the shield
7479 <design/shield#.inv.outside.running>. */
@@ -85,11 +90,11 @@ Bool ShieldCheck(Shield shield)
8590 /* There are no unsynced segments when we're outside the shield. */
8691 CHECKL (shield -> inside || shield -> unsynced == 0 );
8792
88- /* Every unsynced segment should be on the queue, because we have to
89- remember to sync it before we return to the mutator . */
90- CHECKL (shield -> limit + shield -> queuePending >= shield -> unsynced );
93+ /* The queue contains exactly all the unsynced segments that aren't
94+ unqueued, and the queued synced segments . */
95+ CHECKL (shield -> limit == shield -> unsynced - shield -> unqueued + shield -> synced );
9196
92- /* The mutator is suspeneded if there are any holds. */
97+ /* The mutator is suspended if there are any holds. */
9398 CHECKL (shield -> holds == 0 || shield -> suspended );
9499
95100 /* This is too expensive to check all the time since we have an
@@ -105,7 +110,8 @@ Bool ShieldCheck(Shield shield)
105110 if (!SegIsSynced (seg ))
106111 ++ unsynced ;
107112 }
108- CHECKL (unsynced + shield -> queuePending == shield -> unsynced );
113+ CHECKL (unsynced == shield -> limit - shield -> synced );
114+ CHECKL (unsynced + shield -> unqueued == shield -> unsynced );
109115 }
110116#endif
111117
@@ -125,6 +131,8 @@ Res ShieldDescribe(Shield shield, mps_lib_FILE *stream, Count depth)
125131 " next $U\n" , (WriteFU )shield -> next ,
126132 " length $U\n" , (WriteFU )shield -> length ,
127133 " unsynced $U\n" , (WriteFU )shield -> unsynced ,
134+ " unqueued $U\n" , (WriteFU )shield -> unqueued ,
135+ " synced $U\n" , (WriteFU )shield -> synced ,
128136 " holds $U\n" , (WriteFU )shield -> holds ,
129137 "} Shield $P\n" , (WriteFP )shield ,
130138 NULL );
@@ -168,11 +176,22 @@ static void shieldSetSM(Shield shield, Seg seg, AccessSet mode)
168176 if (SegIsSynced (seg )) {
169177 SegSetSM (seg , mode );
170178 ++ shield -> unsynced ;
179+ if (seg -> queued ) {
180+ AVER (shield -> synced > 0 );
181+ -- shield -> synced ;
182+ } else
183+ ++ shield -> unqueued ;
171184 } else {
172185 SegSetSM (seg , mode );
173186 if (SegIsSynced (seg )) {
174187 AVER (shield -> unsynced > 0 );
175188 -- shield -> unsynced ;
189+ if (seg -> queued )
190+ ++ shield -> synced ;
191+ else {
192+ AVER (shield -> unqueued > 0 );
193+ -- shield -> unqueued ;
194+ }
176195 }
177196 }
178197 }
@@ -187,11 +206,22 @@ static void shieldSetPM(Shield shield, Seg seg, AccessSet mode)
187206 if (SegIsSynced (seg )) {
188207 SegSetPM (seg , mode );
189208 ++ shield -> unsynced ;
209+ if (seg -> queued ) {
210+ AVER (shield -> synced > 0 );
211+ -- shield -> synced ;
212+ } else
213+ ++ shield -> unqueued ;
190214 } else {
191215 SegSetPM (seg , mode );
192216 if (SegIsSynced (seg )) {
193217 AVER (shield -> unsynced > 0 );
194218 -- shield -> unsynced ;
219+ if (seg -> queued )
220+ ++ shield -> synced ;
221+ else {
222+ AVER (shield -> unqueued > 0 );
223+ -- shield -> unqueued ;
224+ }
195225 }
196226 }
197227 }
@@ -220,9 +250,11 @@ static void shieldSync(Shield shield, Seg seg)
220250 SHIELD_AVERT_CRITICAL (Seg , seg );
221251
222252 if (!SegIsSynced (seg )) {
253+ /* TODO: Could assert something about the unsync count going down. */
223254 shieldSetPM (shield , seg , SegSM (seg ));
224255 ProtSet (SegBase (seg ), SegLimit (seg ), SegPM (seg ));
225256 }
257+ AVER_CRITICAL (SegIsSynced (seg ));
226258}
227259
228260
@@ -239,6 +271,7 @@ static void shieldSuspend(Arena arena)
239271
240272 AVERT (Arena , arena );
241273 shield = ArenaShield (arena );
274+ AVERT (Shield , shield );
242275 AVER (shield -> inside );
243276
244277 if (!shield -> suspended ) {
@@ -275,6 +308,7 @@ void (ShieldRelease)(Arena arena)
275308
276309 AVERT (Arena , arena );
277310 shield = ArenaShield (arena );
311+ AVERT (Shield , shield );
278312 AVER (shield -> inside );
279313 AVER (shield -> suspended );
280314
@@ -318,6 +352,11 @@ static Seg shieldDequeue(Shield shield, Index i)
318352 AVER (seg -> queued );
319353 shield -> queue [i ] = NULL ; /* to ensure it can't get re-used */
320354 seg -> queued = FALSE;
355+ if (SegIsSynced (seg )) {
356+ AVER (shield -> synced > 0 );
357+ -- shield -> synced ;
358+ } else
359+ ++ shield -> unqueued ;
321360 return seg ;
322361}
323362
@@ -444,11 +483,15 @@ static void shieldQueue(Arena arena, Seg seg)
444483 /* <design/trace#.fix.noaver> */
445484 AVERT_CRITICAL (Arena , arena );
446485 shield = ArenaShield (arena );
486+ AVERT_CRITICAL (Shield , shield );
447487 SHIELD_AVERT_CRITICAL (Seg , seg );
448488
449489 if (SegIsSynced (seg ) || seg -> queued )
450490 return ;
451491
492+ /* This segment is unsynced and not queued. */
493+ AVER (shield -> unqueued > 0 );
494+
452495 if (SegIsExposed (seg )) {
453496 /* This can occur if the mutator isn't suspended, we expose a
454497 segment, then raise the shield on it. In this case, the
@@ -519,6 +562,7 @@ static void shieldQueue(Arena arena, Seg seg)
519562 shield -> queue [shield -> next ] = seg ;
520563 ++ shield -> next ;
521564 seg -> queued = TRUE;
565+ -- shield -> unqueued ;
522566
523567 if (shield -> next >= shield -> limit )
524568 shield -> limit = shield -> next ;
@@ -539,16 +583,14 @@ void (ShieldRaise)(Arena arena, Seg seg, AccessSet mode)
539583 SHIELD_AVERT (Seg , seg );
540584 AVERT (AccessSet , mode );
541585 shield = ArenaShield (arena );
542- AVER (!shield -> queuePending );
543- shield -> queuePending = TRUE;
586+ AVERT (Shield , shield );
544587
545588 /* <design/shield#.inv.prot.shield> preserved */
546589 shieldSetSM (ArenaShield (arena ), seg , BS_UNION (SegSM (seg ), mode ));
547590
548591 /* Ensure <design/shield#.inv.unsynced.suspended> and
549592 <design/shield#.inv.unsynced.depth> */
550593 shieldQueue (arena , seg );
551- shield -> queuePending = FALSE;
552594
553595 /* Check queue and segment consistency. */
554596 AVERT (Arena , arena );
@@ -591,6 +633,7 @@ void (ShieldEnter)(Arena arena)
591633
592634 AVERT (Arena , arena );
593635 shield = ArenaShield (arena );
636+ AVERT (Shield , shield );
594637 AVER (!shield -> inside );
595638 AVER (shield -> depth == 0 );
596639 AVER (!shield -> suspended );
@@ -620,28 +663,40 @@ static void shieldDebugCheck(Arena arena)
620663 Seg seg ;
621664 Count queued = 0 ;
622665 Count depth = 0 ;
666+ Count unqueued = 0 ;
667+ Count unsynced = 0 ;
668+ Count synced = 0 ;
623669
624670 AVERT (Arena , arena );
625671 shield = ArenaShield (arena );
672+ AVERT (Shield , shield );
626673 AVER (shield -> inside || shield -> limit == 0 );
627674
628675 if (SegFirst (& seg , arena ))
629676 do {
630677 depth += SegDepth (seg );
631678 if (shield -> limit == 0 ) {
632679 AVER (!seg -> queued );
633- AVER (SegIsSynced (seg ));
680+ AVER (shield -> unsynced > 0 || SegIsSynced (seg ));
634681 /* You can directly set protections here to see if it makes a
635682 difference. */
636683 /* ProtSet(SegBase(seg), SegLimit(seg), SegPM(seg)); */
637- } else {
638- if (seg -> queued )
639- ++ queued ;
640684 }
685+ if (seg -> queued )
686+ ++ queued ;
687+ if (!SegIsSynced (seg ))
688+ ++ unsynced ;
689+ if (seg -> queued && SegIsSynced (seg ))
690+ ++ synced ;
691+ if (!seg -> queued && !SegIsSynced (seg ))
692+ ++ unqueued ;
641693 } while (SegNext (& seg , arena , seg ));
642694
643695 AVER (depth == shield -> depth );
644696 AVER (queued == shield -> limit );
697+ AVER (unsynced == shield -> unsynced );
698+ AVER (unqueued == shield -> unqueued );
699+ AVER (synced == shield -> synced );
645700}
646701#endif
647702
@@ -668,6 +723,7 @@ void (ShieldFlush)(Arena arena)
668723
669724 AVERT (Arena , arena );
670725 shield = ArenaShield (arena );
726+ AVERT (Shield , shield );
671727#ifdef SHIELD_DEBUG
672728 shieldDebugCheck (arena );
673729#endif
@@ -687,6 +743,7 @@ void (ShieldLeave)(Arena arena)
687743
688744 AVERT (Arena , arena );
689745 shield = ArenaShield (arena );
746+ AVERT (Shield , shield );
690747 AVER (shield -> inside );
691748 AVER (shield -> depth == 0 ); /* no pending covers */
692749 AVER (shield -> holds == 0 );
@@ -721,6 +778,7 @@ void (ShieldExpose)(Arena arena, Seg seg)
721778 /* <design/trace#.fix.noaver> */
722779 AVERT_CRITICAL (Arena , arena );
723780 shield = ArenaShield (arena );
781+ AVERT (Shield , shield );
724782 AVER_CRITICAL (shield -> inside );
725783
726784 SegSetDepth (seg , SegDepth (seg ) + 1 );
@@ -747,6 +805,7 @@ void (ShieldCover)(Arena arena, Seg seg)
747805 /* <design/trace#.fix.noaver> */
748806 AVERT_CRITICAL (Arena , arena );
749807 shield = ArenaShield (arena );
808+ AVERT_CRITICAL (Shield , shield );
750809 AVERT_CRITICAL (Seg , seg );
751810 AVER_CRITICAL (SegPM (seg ) == AccessSetEMPTY );
752811
0 commit comments