-
Notifications
You must be signed in to change notification settings - Fork 105
/
DetSchedSchedule_AI.thy
3644 lines (3144 loc) · 161 KB
/
DetSchedSchedule_AI.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory DetSchedSchedule_AI
imports ArchDetSchedDomainTime_AI
begin
crunch do_machine_op
for ct_not_in_q[wp]: "ct_not_in_q"
lemma set_tcb_queue_wp[wp]: "\<lbrace>\<lambda>s. P (ready_queues_update (\<lambda>_ t' p. if t' = t \<and> p = prio then queue else ready_queues s t' p) s)\<rbrace> set_tcb_queue t prio queue \<lbrace>\<lambda>_. P\<rbrace>"
apply (simp add: set_tcb_queue_def)
apply wp
done
lemma get_tcb_queue_wp[wp]: "\<lbrace>\<lambda>s. P (ready_queues s t p) s\<rbrace> get_tcb_queue t p \<lbrace>P\<rbrace>"
apply (simp add: get_tcb_queue_def)
apply wp
done
crunch tcb_sched_action
for valid_etcbs[wp]: "valid_etcbs"
lemma enqueue_distinct[intro!]: "distinct queue \<Longrightarrow> distinct (tcb_sched_enqueue thread queue)"
apply (simp add: tcb_sched_enqueue_def)
done
lemma is_activatable_trivs[iff]:
"is_activatable_2 ct (switch_thread t) kh"
"is_activatable_2 ct choose_new_thread kh"
by (simp_all add: is_activatable_def)
lemma weak_valid_sched_action_trivs[iff]:
"weak_valid_sched_action_2 resume_cur_thread ekh kh"
"weak_valid_sched_action_2 choose_new_thread ekh kh"
by (simp_all add: weak_valid_sched_action_def)
lemma switch_in_cur_domain_trivs[iff]:
"switch_in_cur_domain_2 resume_cur_thread ekh cdom"
"switch_in_cur_domain_2 choose_new_thread ekh cdom"
by (simp_all add: switch_in_cur_domain_def)
lemma ct_in_cur_domain_2_trivs[iff]:
"ct_in_cur_domain_2 thread thread' (switch_thread t) cdom ekh"
"ct_in_cur_domain_2 thread thread' choose_new_thread cdom ekh"
by (simp_all add: ct_in_cur_domain_2_def)
lemma valid_sched_action_triv[iff]:
"valid_sched_action_2 choose_new_thread ekh kh ct cdom"
by (simp add: valid_sched_action_def)
lemma simple_sched_action_trivs[iff]:
"simple_sched_action_2 resume_cur_thread"
"simple_sched_action_2 choose_new_thread"
by (simp_all add: simple_sched_action_def)
lemma scheduler_act_not_trivs[iff]:
"scheduler_act_not_2 resume_cur_thread t"
"scheduler_act_not_2 choose_new_thread t"
by (simp_all add: scheduler_act_not_def)
lemma tcb_sched_action_enqueue_valid_queues[wp]:
"\<lbrace>valid_queues and st_tcb_at runnable thread\<rbrace>
tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply simp
apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_enqueue_def is_etcb_at_def
split: option.split)
done
lemma tcb_sched_action_append_valid_queues[wp]:
"\<lbrace>valid_queues and st_tcb_at runnable thread\<rbrace>
tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_append_def is_etcb_at_def
split: option.split)
done
lemma tcb_sched_action_dequeue_valid_queues[wp]:
"\<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_dequeue_def
split: option.splits)
apply blast
done
lemma tcb_sched_action_enqueue_ct_not_in_q[wp]:
"\<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace>
tcb_sched_action tcb_sched_enqueue thread
\<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: ct_not_in_q_def not_cur_thread_def etcb_at_def
tcb_sched_enqueue_def not_queued_def
split: option.splits)
done
lemma tcb_sched_action_append_ct_not_in_q[wp]:
"\<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: ct_not_in_q_def not_cur_thread_def etcb_at_def
tcb_sched_append_def not_queued_def
split: option.splits)
done
lemma tcb_sched_action_dequeue_ct_not_in_q[wp]:
"\<lbrace>ct_not_in_q\<rbrace> tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (fastforce simp: ct_not_in_q_def etcb_at_def tcb_sched_dequeue_def
not_queued_def
split: option.splits)
done
crunch tcb_sched_action
for is_activatable[wp]: "is_activatable t"
crunch tcb_sched_action
for weak_valid_sched_action[wp]: "weak_valid_sched_action"
crunch tcb_sched_action
for valid_sched_action[wp]: valid_sched_action
crunch tcb_sched_action
for ct_in_cur_domain[wp]: ct_in_cur_domain
lemma tcb_sched_action_enqueue_valid_blocked:
"\<lbrace>valid_blocked_except thread\<rbrace>
tcb_sched_action tcb_sched_enqueue thread
\<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def tcb_sched_enqueue_def not_queued_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply (rule conjI)
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
done
lemma tcb_sched_action_append_valid_blocked:
"\<lbrace>valid_blocked_except thread\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def tcb_sched_append_def not_queued_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply (rule conjI)
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
done
lemma tcb_sched_action_dequeue_valid_blocked:
"\<lbrace>valid_blocked and st_tcb_at (\<lambda>st. \<not> active st) thread\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def tcb_sched_dequeue_def not_queued_def valid_blocked_def split: option.splits)
apply (case_tac "t=thread")
apply simp
apply (force simp: st_tcb_at_def obj_at_def)
apply (erule_tac x=t in allE)
apply force
done
lemma tcb_sched_action_dequeue_valid_blocked_except:
"\<lbrace>valid_blocked\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. valid_blocked_except thread\<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def tcb_sched_dequeue_def not_queued_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply (case_tac "t=thread")
apply simp
apply (erule_tac x=t in allE)
apply force
done
abbreviation valid_sched_except_blocked_2 where
"valid_sched_except_blocked_2 queues ekh sa cdom kh ct it \<equiv>
valid_etcbs_2 ekh kh \<and> valid_queues_2 queues ekh kh \<and> ct_not_in_q_2 queues sa ct \<and> valid_sched_action_2 sa ekh kh ct cdom \<and> ct_in_cur_domain_2 ct it sa cdom ekh \<and> valid_idle_etcb_2 ekh"
abbreviation valid_sched_except_blocked :: "det_ext state \<Rightarrow> bool" where
"valid_sched_except_blocked s \<equiv> valid_sched_except_blocked_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)"
declare valid_idle_etcb_lift[wp]
lemma tcb_sched_action_enqueue_valid_sched[wp]:
"\<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace>
tcb_sched_action tcb_sched_enqueue thread
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (simp add: valid_sched_def | wp tcb_sched_action_enqueue_valid_blocked)+
lemma tcb_sched_action_append_valid_sched[wp]:
"\<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (simp add: valid_sched_def | wp tcb_sched_action_append_valid_blocked)+
lemma tcb_sched_action_dequeue_valid_sched_not_runnable:
"\<lbrace>valid_sched and st_tcb_at (\<lambda>st. \<not> active st) thread\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (simp add: valid_sched_def | wp tcb_sched_action_dequeue_valid_blocked)+
lemma tcb_sched_action_dequeue_valid_sched_except_blocked:
"\<lbrace>valid_sched\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace>"
by (simp add: valid_sched_def | wp tcb_sched_action_dequeue_valid_blocked_except)+
crunch set_scheduler_action
for valid_etcbs[wp]: "valid_etcbs"
crunch set_scheduler_action
for valid_queues[wp]: "valid_queues"
lemma set_scheduler_action_rct_ct_not_in_q[wp]:
"\<lbrace>ct_not_queued\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (fastforce simp: ct_not_in_q_def not_queued_def)
done
lemma set_scheduler_action_rct_is_activatable[wp]:
"\<lbrace>st_tcb_at activatable t\<rbrace>
set_scheduler_action resume_cur_thread
\<lbrace>\<lambda>_. is_activatable t\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: is_activatable_def)
done
lemma set_scheduler_action_rct_weak_valid_sched_action[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: weak_valid_sched_action_def)
done
lemma set_scheduler_action_wp:
"\<lbrace>\<lambda>s. Q (scheduler_action_update (\<lambda>_. a) s)\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_.Q\<rbrace>"
apply (simp add: set_scheduler_action_def)
apply wp
done
lemma set_scheduler_action_rct_valid_sched_action[wp]:
"\<lbrace>\<lambda>s. st_tcb_at activatable (cur_thread s) s\<rbrace>
set_scheduler_action resume_cur_thread
\<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: valid_sched_action_def | wp set_scheduler_action_wp)+
apply (simp add: is_activatable_def)
done
lemma set_scheduler_action_rct_ct_in_cur_domain[wp]:
"\<lbrace>\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
apply (simp add: valid_sched_action_def | wp set_scheduler_action_wp)+
apply (clarsimp simp: in_cur_domain_def ct_in_cur_domain_2_def)
done
lemma set_scheduler_action_rct_valid_blocked:
"\<lbrace>valid_blocked and simple_sched_action\<rbrace>
set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: valid_blocked_def simple_sched_action_def split: scheduler_action.splits | wp set_scheduler_action_wp)+
done
crunch set_scheduler_action
for etcb_at[wp]: "etcb_at P t"
lemma set_scheduler_action_rct_valid_sched:
"\<lbrace>valid_sched and ct_not_queued
and (\<lambda>s. st_tcb_at activatable (cur_thread s) s)
and (\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s)
and simple_sched_action\<rbrace>
set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_.valid_sched\<rbrace>"
by (simp add: valid_sched_def | wp set_scheduler_action_rct_valid_blocked)+
lemma set_scheduler_action_cnt_ct_not_in_q[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: ct_not_in_q_def)
done
lemma set_scheduler_action_cnt_is_activatable[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. is_activatable t\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: is_activatable_def)
done
lemma set_scheduler_action_cnt_ct_in_cur_domain[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: ct_in_cur_domain_def)
done
lemma set_scheduler_action_cnt_weak_valid_sched_action[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
apply (simp add: set_scheduler_action_def, wp)
apply (simp add: weak_valid_sched_action_def)
done
lemma set_scheduler_action_cnt_valid_sched_action[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: valid_sched_action_def, wp set_scheduler_action_wp)
apply (simp add: is_activatable_def)
done
lemma set_scheduler_action_cnt_valid_blocked_weak:
"\<lbrace>valid_blocked and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: valid_blocked_def, wp set_scheduler_action_wp)
apply (simp add: simple_sched_action_def split: scheduler_action.splits)
done
lemma set_scheduler_action_cnt_valid_blocked:
"\<lbrace>valid_blocked and (\<lambda>s. \<forall>t. scheduler_action s = switch_thread t \<longrightarrow>
(\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: valid_blocked_def, wp set_scheduler_action_wp)
apply clarsimp
apply (erule_tac x=t in allE)
apply (erule impCE)
apply force
apply (erule_tac x=st in allE)
apply (force simp: not_queued_def)
done
lemma set_scheduler_action_cnt_valid_blocked_except:
"\<lbrace>valid_blocked_except target and (\<lambda>s. \<forall>t. scheduler_action s = switch_thread t \<longrightarrow>
(\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked_except target\<rbrace>"
apply (simp add: valid_blocked_except_def, wp set_scheduler_action_wp)
apply clarsimp
apply (erule_tac x=t in allE)
apply (erule impCE)
apply force
apply (force simp: not_queued_def)
done
lemma set_scheduler_action_cnt_weak_valid_sched:
"\<lbrace>valid_sched and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (simp add: valid_sched_def simple_sched_action_def split: scheduler_action.splits | wp set_scheduler_action_cnt_valid_blocked)+
crunch reschedule_required
for valid_etcbs[wp]: "valid_etcbs"
lemma reschedule_required_valid_queues[wp]:
"\<lbrace>valid_queues and weak_valid_sched_action\<rbrace>
reschedule_required
\<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: reschedule_required_def | wp | wpc)+
apply (simp add: weak_valid_sched_action_def)
done
lemma reschedule_required_ct_not_in_q[wp]:
"\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
by (simp add: reschedule_required_def, wp)
lemma reschedule_required_is_activatable[wp]:
"\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. is_activatable t\<rbrace>"
by (simp add: reschedule_required_def, wp)
lemma reschedule_required_weak_valid_sched_action[wp]:
"\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
by (simp add: reschedule_required_def, wp)
lemma tcb_sched_action_enqueue_valid_blocked_except:
"\<lbrace>valid_blocked_except thread\<rbrace>
tcb_sched_action tcb_sched_enqueue thread'
\<lbrace>\<lambda>_. valid_blocked_except thread \<rbrace>"
apply (simp add: tcb_sched_action_def, wp)
apply (clarsimp simp: etcb_at_def tcb_sched_enqueue_def not_queued_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply (rule conjI)
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
apply clarsimp
apply (case_tac "t=thread")
apply force
apply (erule_tac x=t in allE)
apply clarsimp
apply force
done
lemma reschedule_required_valid_sched_action[wp]:
"\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: valid_sched_action_def reschedule_required_def)
apply (wp set_scheduler_action_wp | simp)+
done
lemma reschedule_required_ct_in_cur_domain[wp]:
"\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
by (simp add: reschedule_required_def, wp)
lemma reschedule_required_valid_blocked:
"\<lbrace>valid_blocked\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: reschedule_required_def | wp set_scheduler_action_cnt_valid_blocked tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift | wpc)+
apply (simp add: tcb_sched_action_def)
apply wp+
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule conjI)
apply (force simp: etcb_at_def tcb_sched_enqueue_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply clarsimp
done
lemma reschedule_required_valid_blocked_except:
"\<lbrace>valid_blocked_except target\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_blocked_except target\<rbrace>"
apply (simp add: reschedule_required_def | wp set_scheduler_action_cnt_valid_blocked_except tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_all_lift | wpc)+
apply (simp add: tcb_sched_action_def)
apply wp+
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule conjI)
apply (force simp: etcb_at_def tcb_sched_enqueue_def valid_blocked_except_def split: option.splits)
apply clarsimp
done
crunch reschedule_required
for etcb_at[wp]: "etcb_at P t"
lemma reschedule_required_valid_sched:
"\<lbrace>valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked and valid_idle_etcb\<rbrace>
reschedule_required
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (simp add: valid_sched_def | wp reschedule_required_valid_blocked)+
lemma reschedule_required_valid_sched_cur_thread:
"\<lbrace>(\<lambda>s. target = cur_thread s) and valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked_except target and valid_idle_etcb\<rbrace>
reschedule_required
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (simp add: valid_sched_def | wp reschedule_required_valid_blocked)+
apply (clarsimp simp: valid_blocked_except_def valid_blocked_def)
done
lemma get_tcb_st_tcb_at:
"get_tcb t s = Some y \<Longrightarrow> st_tcb_at \<top> t s"
apply (simp add: get_tcb_def pred_tcb_at_def obj_at_def
split: option.splits kernel_object.splits)
done
lemma st_tcb_at_kh_if_split:
"st_tcb_at_kh P ptr (\<lambda>t. if t = ref then x else kh t)
= (if ptr = ref then (\<exists>tcb. x = Some (TCB tcb) \<and> P (tcb_state tcb))
else st_tcb_at_kh P ptr kh)"
by (fastforce simp: st_tcb_at_kh_def obj_at_kh_def obj_at_def)
lemma set_thread_state_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp | wpc | simp add: set_thread_state_ext_def set_object_def get_object_def)+
apply (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split
dest: get_tcb_st_tcb_at)
done
lemma set_bound_notification_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wp | wpc | simp add: set_object_def get_object_def)+
apply (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split
dest: get_tcb_st_tcb_at)
done
lemma set_thread_state_runnable_valid_queues:
"\<lbrace>valid_queues and K (runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp | wpc | simp add: set_thread_state_ext_def set_object_def get_object_def)+
apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split)
done
lemma set_bound_notification_valid_queues:
"\<lbrace>valid_queues\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
apply clarsimp
apply (drule (1) bspec, clarsimp simp: st_tcb_def2)
done
lemma set_thread_state_ct_not_in_q[wp]:
"\<lbrace>ct_not_in_q\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp gts_wp)+
done
lemma set_bound_notification_ct_not_in_q[wp]:
"\<lbrace>ct_not_in_q\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def | wp)+
done
lemma set_thread_state_cur_is_activatable[wp]:
"\<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_ (s::det_state). is_activatable (cur_thread s) s\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def |
wp set_scheduler_action_wp gts_wp)+
apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split
pred_tcb_at_def obj_at_def)
done
lemma set_bound_notification_cur_is_activatable[wp]:
"\<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace>
set_bound_notification ref ntfn
\<lbrace>\<lambda>_ (s::det_state). is_activatable (cur_thread s) s\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def | wp set_scheduler_action_wp)+
apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split pred_tcb_at_def
obj_at_def get_tcb_def)
done
lemma set_thread_state_runnable_weak_valid_sched_action:
"\<lbrace>weak_valid_sched_action and (\<lambda>s. runnable ts)\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp gts_wp)+
apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split)
done
lemma set_thread_state_switch_in_cur_domain[wp]:
"\<lbrace>switch_in_cur_domain\<rbrace>
set_thread_state ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def
| wp set_scheduler_action_wp gts_wp)+
done
lemma set_bound_notification_switch_in_cur_domain[wp]:
"\<lbrace>switch_in_cur_domain\<rbrace>
set_bound_notification ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def | wp set_scheduler_action_wp gbn_wp)+
done
lemma set_bound_notification_weak_valid_sched_action:
"\<lbrace>weak_valid_sched_action\<rbrace>
set_bound_notification ref ntfnptr
\<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def | wp)+
apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split
st_tcb_def2)
done
lemma set_thread_state_runnable_valid_sched_action:
"\<lbrace>valid_sched_action and (\<lambda>s. runnable ts)\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: valid_sched_action_def
| wp set_thread_state_runnable_weak_valid_sched_action)+
done
lemma set_thread_state_cur_ct_in_cur_domain[wp]:
"\<lbrace>ct_in_cur_domain\<rbrace>
set_thread_state ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def |
wp set_scheduler_action_wp gts_wp)+
done
lemma set_thread_state_schact_is_rct:
"\<lbrace>schact_is_rct and (\<lambda>s. ref = cur_thread s \<longrightarrow> runnable ts )\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_. schact_is_rct\<rbrace>"
unfolding set_thread_state_def set_thread_state_ext_extended.dxo_eq
apply (clarsimp simp: set_thread_state_ext_def)
apply (wpsimp wp: set_object_wp gts_wp simp: set_scheduler_action_def)
apply (clarsimp simp: schact_is_rct_def st_tcb_at_def obj_at_def)
done
lemma set_bound_notification_cur_ct_in_cur_domain[wp]:
"\<lbrace>ct_in_cur_domain\<rbrace>
set_bound_notification ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def |
wp set_scheduler_action_wp gbn_wp)+
done
crunch set_thread_state, set_bound_notification, get_bound_notification
for etcb_at[wp]: "etcb_at P t"
lemma set_thread_state_runnable_valid_sched_except_blocked:
"\<lbrace>valid_sched and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace>"
apply (simp add: valid_sched_def | wp set_thread_state_runnable_valid_queues
set_thread_state_runnable_valid_sched_action)+
done
lemma set_bound_notification_valid_sched_action:
"\<lbrace>valid_sched_action\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: valid_sched_action_def |
wp set_bound_notification_weak_valid_sched_action)+
done
lemma set_bound_notification_valid_blocked[wp]:
"\<lbrace>valid_blocked\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: set_bound_notification_def)
apply (simp add: set_object_def get_object_def | wp)+
apply (clarsimp simp: valid_blocked_def)
apply (drule_tac x=ta in spec, clarsimp)
apply (drule_tac x=st in spec)
apply (simp only: st_tcb_at_kh_if_split)
apply (simp add: st_tcb_def2 split: if_split_asm)
done
lemma set_bound_notification_valid_sched:
"\<lbrace>valid_sched\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (simp add: valid_sched_def | wp set_bound_notification_valid_queues
set_bound_notification_valid_sched_action)+
done
lemma valid_blocked_valid_blocked_except[simp]:
"valid_blocked s \<Longrightarrow> valid_blocked_except t s"
by (simp add: valid_blocked_def valid_blocked_except_def)
lemma set_thread_state_valid_blocked_except:
"\<lbrace>valid_blocked\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_blocked_except ref\<rbrace>"
apply (simp add: set_thread_state_def)
apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp)+
apply (rule hoare_strengthen_post)
apply (rule set_scheduler_action_cnt_valid_blocked_weak)
apply simp
apply (wp gts_wp)+
apply (clarsimp simp: valid_blocked_def valid_blocked_except_def st_tcb_at_def obj_at_def)
done
(* as user schedule invariants *)
lemma as_user_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
by (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split dest: get_tcb_st_tcb_at)
lemma as_user_valid_queues[wp]: "\<lbrace>valid_queues\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_queues\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
apply clarsimp
apply (drule (1) bspec, clarsimp simp: st_tcb_def2)
apply (drule get_tcb_SomeD, auto)
done
lemma as_user_weak_valid_sched_action[wp]: "\<lbrace>weak_valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def)
by (drule get_tcb_SomeD, auto)
lemma as_user_is_activatable[wp]: "\<lbrace>is_activatable t\<rbrace> as_user ptr s \<lbrace>\<lambda>_. is_activatable t\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def)
by (drule get_tcb_SomeD, auto)
lemma as_user_valid_sched_action[wp]: "\<lbrace>valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
apply (clarsimp simp: valid_sched_action_def st_tcb_at_def obj_at_def)
apply (rule conjI)
apply (clarsimp simp: is_activatable_def st_tcb_at_def obj_at_def st_tcb_at_kh_if_split)
apply (drule get_tcb_SomeD, clarsimp)
apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_def obj_at_def st_tcb_at_kh_if_split)
apply (drule get_tcb_SomeD, clarsimp)
done
crunch as_user
for ct_in_cur_domain[wp]: ct_in_cur_domain
(wp: ct_in_cur_domain_lift)
lemma as_user_valid_idle_etcb[wp]: "\<lbrace>valid_idle_etcb\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>"
by (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
lemma as_user_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+
apply (clarsimp simp: valid_blocked_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def)
apply (drule_tac x=ptr in spec)
by (drule get_tcb_SomeD, auto)
definition ct_in_q where
"ct_in_q s \<equiv> st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p))"
locale DetSchedSchedule_AI =
assumes arch_switch_to_idle_thread_valid_etcbs'[wp]:
"\<lbrace>valid_etcbs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
assumes arch_switch_to_thread_valid_etcbs'[wp]:
"\<And>t. \<lbrace>valid_etcbs\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
assumes arch_switch_to_idle_thread_valid_queues'[wp]:
"\<lbrace>valid_queues\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. valid_queues\<rbrace>"
assumes arch_switch_to_thread_valid_queues'[wp]:
"\<And>t. \<lbrace>valid_queues\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_queues\<rbrace>"
assumes arch_switch_to_idle_thread_weak_valid_sched_action'[wp]:
"\<lbrace>weak_valid_sched_action\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
assumes arch_switch_to_thread_weak_valid_sched_action'[wp]:
"\<And>t. \<lbrace>weak_valid_sched_action\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
assumes switch_to_idle_thread_ct_not_in_q[wp]:
"\<lbrace>valid_queues and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
assumes switch_to_idle_thread_valid_sched_action[wp]:
"\<lbrace>valid_sched_action and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
assumes switch_to_idle_thread_ct_in_cur_domain[wp]:
"\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
assumes arch_switch_to_thread_ct_not_in_q'[wp]:
"\<And>t. \<lbrace>ct_not_in_q\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
assumes arch_switch_to_thread_is_activatable'[wp]:
"\<And>t t'. \<lbrace>is_activatable t'\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. is_activatable t'\<rbrace>"
assumes arch_switch_to_thread_valid_sched_action'[wp]:
"\<And>t. \<lbrace>valid_sched_action\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
assumes arch_switch_to_thread_valid_sched'[wp]:
"\<And>t. \<lbrace>valid_sched\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes arch_switch_to_thread_ct_in_cur_domain_2[wp]:
"\<And>t' t.
\<lbrace>\<lambda>s. ct_in_cur_domain_2 t' (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>
arch_switch_to_thread t
\<lbrace>\<lambda>_ s. ct_in_cur_domain_2 t' (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>"
assumes arch_switch_to_thread_valid_blocked[wp]:
"\<And>t. \<lbrace>valid_blocked and ct_in_q\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>"
assumes arch_switch_to_thread_etcb_at'[wp]:
"\<And>P t' t. \<lbrace>etcb_at P t'\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. etcb_at P t'\<rbrace>"
assumes arch_switch_to_idle_thread_valid_idle[wp]:
"\<lbrace>valid_idle :: det_ext state \<Rightarrow> bool\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. valid_idle\<rbrace>"
assumes switch_to_idle_thread_ct_not_queued[wp]:
"\<lbrace>valid_queues and valid_etcbs and valid_idle\<rbrace>
switch_to_idle_thread
\<lbrace>\<lambda>rv s. not_queued (cur_thread s) s\<rbrace>"
assumes switch_to_idle_thread_valid_blocked[wp]:
"\<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace>"
assumes arch_switch_to_thread_exst'[wp]:
"\<And>P t. \<lbrace>\<lambda>s. P (exst s :: det_ext)\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>rv s. P (exst s)\<rbrace>"
assumes arch_switch_to_thread_scheduler_action'[wp]:
"\<And>P t.
\<lbrace>\<lambda>s. P (scheduler_action (s :: det_ext state))\<rbrace>
arch_switch_to_thread t
\<lbrace>\<lambda>rv s. P (scheduler_action (s :: det_ext state))\<rbrace>"
assumes stit_activatable':
"\<lbrace>valid_idle :: det_ext state \<Rightarrow> bool\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
assumes arch_switch_to_idle_thread_etcb_at'[wp]:
"\<And>P t. \<lbrace>etcb_at P t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. etcb_at P t\<rbrace>"
assumes switch_to_idle_thread_cur_thread_idle_thread [wp]:
"\<lbrace>\<top> :: det_ext state \<Rightarrow> bool\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. cur_thread s = idle_thread s\<rbrace>"
assumes arch_switch_to_idle_thread_scheduler_action'[wp]:
"\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>"
assumes arch_finalise_cap_ct_not_in_q'[wp]:
"\<And>acap final. \<lbrace>ct_not_in_q\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
assumes arch_finalise_cap_valid_etcbs'[wp]:
"\<And>acap final. \<lbrace>valid_etcbs\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
assumes arch_finalise_cap_simple_sched_action'[wp]:
"\<And>acap final. \<lbrace>simple_sched_action\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>_. simple_sched_action\<rbrace>"
assumes arch_finalise_cap_valid_sched'[wp]:
"\<And>acap final. \<lbrace>valid_sched\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes arch_post_cap_deletion_valid_idle[wp]:
"\<And>target. \<lbrace>valid_idle :: det_ext state \<Rightarrow> bool\<rbrace>
arch_post_cap_deletion target
\<lbrace>\<lambda>_. valid_idle\<rbrace>"
assumes handle_arch_fault_reply_valid_sched'[wp]:
"\<And>f t x y. \<lbrace>valid_sched\<rbrace> handle_arch_fault_reply f t x y \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes activate_thread_valid_sched:
"\<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes arch_perform_invocation_valid_sched[wp]:
"\<And>i.
\<lbrace>invs and valid_sched and ct_active and valid_arch_inv i\<rbrace>
arch_perform_invocation i
\<lbrace>\<lambda>_.valid_sched\<rbrace>"
assumes arch_invoke_irq_control_valid_sched'[wp]:
"\<And>i. \<lbrace>valid_sched\<rbrace> arch_invoke_irq_control i \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes handle_vm_fault_valid_sched'[wp]:
"\<And>t f. \<lbrace>valid_sched\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes handle_vm_fault_not_queued'[wp]:
"\<And>t' t f. \<lbrace>not_queued t'\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. not_queued t'\<rbrace>"
assumes handle_vm_fault_scheduler_act_not'[wp]:
"\<And>t' t f. \<lbrace>scheduler_act_not t'\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. scheduler_act_not t'\<rbrace>"
assumes handle_arch_fault_reply_not_queued'[wp]:
"\<And>t' f t x y. \<lbrace>not_queued t'\<rbrace> handle_arch_fault_reply f t x y \<lbrace>\<lambda>_. not_queued t'\<rbrace>"
assumes handle_arch_fault_reply_scheduler_act_not'[wp]:
"\<And>t' f t x y. \<lbrace>scheduler_act_not t'\<rbrace> handle_arch_fault_reply f t x y \<lbrace>\<lambda>_. scheduler_act_not t'\<rbrace>"
assumes handle_arch_fault_reply_cur'[wp]:
"\<And>f t x y. \<lbrace>cur_tcb :: det_ext state \<Rightarrow> bool\<rbrace> handle_arch_fault_reply f t x y \<lbrace>\<lambda>_. cur_tcb\<rbrace>"
assumes hvmf_st_tcb_at[wp]:
"\<And>P t' t w.
\<lbrace>st_tcb_at P t' :: det_ext state \<Rightarrow> bool \<rbrace>
handle_vm_fault t w
\<lbrace>\<lambda>rv. st_tcb_at P t' \<rbrace>"
assumes handle_vm_fault_st_tcb_cur_thread[wp]:
"\<And>P t f.
\<lbrace> \<lambda>s :: det_ext state. st_tcb_at P (cur_thread s) s \<rbrace>
handle_vm_fault t f
\<lbrace>\<lambda>_ s. st_tcb_at P (cur_thread s) s \<rbrace>"
assumes arch_activate_idle_thread_valid_list'[wp]:
"\<And>t. \<lbrace>valid_list\<rbrace> arch_activate_idle_thread t \<lbrace>\<lambda>_. valid_list\<rbrace>"
assumes arch_switch_to_thread_valid_list'[wp]:
"\<And>t. \<lbrace>valid_list\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. valid_list\<rbrace>"
assumes arch_switch_to_idle_thread_valid_list'[wp]:
"\<lbrace>valid_list\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. valid_list\<rbrace>"
assumes prepare_thread_delete_idel_thread[wp] :
"\<And>t. prepare_thread_delete t \<lbrace>\<lambda>(s:: det_ext state). P (idle_thread s)\<rbrace>"
assumes prepare_thread_delete_ct_not_in_q'[wp]:
"\<And>t. \<lbrace>ct_not_in_q\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
assumes prepare_thread_delete_valid_etcbs'[wp]:
"\<And>t. \<lbrace>valid_etcbs\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
assumes prepare_thread_delete_simple_sched_action'[wp]:
"\<And>t. \<lbrace>simple_sched_action\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>_. simple_sched_action\<rbrace>"
assumes prepare_thread_delete_valid_sched'[wp]:
"\<And>t. \<lbrace>valid_sched\<rbrace> prepare_thread_delete t \<lbrace>\<lambda>_. valid_sched\<rbrace>"
assumes make_fault_arch_msg_not_cur_thread[wp] :
"\<And>ft t t'. make_arch_fault_msg ft t \<lbrace>not_cur_thread t'\<rbrace>"
assumes make_fault_arch_msg_valid_sched[wp] :
"\<And>ft t. make_arch_fault_msg ft t \<lbrace>valid_sched\<rbrace>"
assumes make_fault_arch_msg_scheduler_action[wp] :
"\<And>P ft t. make_arch_fault_msg ft t \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>"
assumes make_fault_arch_msg_ready_queues[wp] :
"\<And>P ft t. make_arch_fault_msg ft t \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
assumes make_fault_arch_msg_valid_etcbs[wp] :
"\<And>ft t. make_arch_fault_msg ft t \<lbrace>valid_etcbs\<rbrace>"
assumes arch_get_sanitise_register_info_not_cur_thread[wp] :
"\<And>ft t'. arch_get_sanitise_register_info ft \<lbrace>not_cur_thread t'\<rbrace>"
assumes arch_get_sanitise_register_info_valid_sched[wp] :
"\<And>ft. arch_get_sanitise_register_info ft \<lbrace>valid_sched\<rbrace>"
assumes arch_get_sanitise_register_info_scheduler_action[wp] :
"\<And>P ft. arch_get_sanitise_register_info ft \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>"
assumes arch_get_sanitise_register_info_ready_queues[wp] :
"\<And>P ft. arch_get_sanitise_register_info ft \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
assumes arch_get_sanitise_register_info_valid_etcbs[wp] :
"\<And>ft. arch_get_sanitise_register_info ft \<lbrace>valid_etcbs\<rbrace>"
assumes arch_get_sanitise_register_info_cur'[wp]:
"\<And>f. \<lbrace>cur_tcb :: det_ext state \<Rightarrow> bool\<rbrace> arch_get_sanitise_register_info f \<lbrace>\<lambda>_. cur_tcb\<rbrace>"
assumes arch_post_modify_registers_not_cur_thread[wp] :
"\<And>c ft t'. arch_post_modify_registers c ft \<lbrace>not_cur_thread t'\<rbrace>"
assumes arch_post_modify_registers_valid_sched[wp] :
"\<And>c ft. arch_post_modify_registers c ft \<lbrace>valid_sched\<rbrace>"
assumes arch_post_modify_registers_scheduler_action[wp] :
"\<And>P c ft. arch_post_modify_registers c ft \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>"
assumes arch_post_modify_registers_ready_queues[wp] :
"\<And>P c ft. arch_post_modify_registers c ft \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
assumes arch_post_modify_registers_valid_etcbs[wp] :
"\<And>c ft. arch_post_modify_registers c ft \<lbrace>valid_etcbs\<rbrace>"
assumes arch_post_modify_registers_cur'[wp]:
"\<And>c f. \<lbrace>cur_tcb :: det_ext state \<Rightarrow> bool\<rbrace> arch_post_modify_registers c f \<lbrace>\<lambda>_. cur_tcb\<rbrace>"
assumes arch_post_modify_registers_not_idle_thread[wp]:
"\<And>c t. \<lbrace>\<lambda>s::det_ext state. t \<noteq> idle_thread s\<rbrace> arch_post_modify_registers c t \<lbrace>\<lambda>_ s. t \<noteq> idle_thread s\<rbrace>"
assumes arch_post_cap_deletion_valid_etcbs[wp] :
"\<And>c. arch_post_cap_deletion c \<lbrace>valid_etcbs\<rbrace>"
assumes arch_post_cap_deletion_valid_sched[wp] :
"\<And>c. arch_post_cap_deletion c \<lbrace>valid_sched\<rbrace>"
assumes arch_post_cap_deletion_ct_not_in_q[wp] :
"\<And>c. arch_post_cap_deletion c \<lbrace>ct_not_in_q\<rbrace>"
assumes arch_post_cap_deletion_simple_sched_action[wp] :
"\<And>c. arch_post_cap_deletion c \<lbrace>simple_sched_action\<rbrace>"
assumes arch_post_cap_deletion_not_cur_thread[wp] :
"\<And>c t. arch_post_cap_deletion c \<lbrace>not_cur_thread t\<rbrace>"
assumes arch_post_cap_deletion_sched_act_not[wp] :
"\<And>c t. arch_post_cap_deletion c \<lbrace>scheduler_act_not t\<rbrace>"
assumes arch_post_cap_deletion_not_queued[wp] :
"\<And>c t. arch_post_cap_deletion c \<lbrace>not_queued t\<rbrace>"
assumes arch_post_cap_deletion_is_etcb_at[wp] :
"\<And>c t. arch_post_cap_deletion c \<lbrace>is_etcb_at t\<rbrace>"
assumes arch_post_cap_deletion_weak_valid_sched_action[wp] :
"\<And>c. arch_post_cap_deletion c \<lbrace>weak_valid_sched_action\<rbrace>"
assumes arch_finalise_cap_idle_thread[wp] :
"\<And>P b t. arch_finalise_cap t b \<lbrace>\<lambda> (s:: det_ext state). P (idle_thread s)\<rbrace>"
assumes arch_invoke_irq_handler_valid_sched[wp]:
"\<And>i. arch_invoke_irq_handler i \<lbrace>valid_sched\<rbrace>"
assumes arch_mask_irq_signal_valid_sched[wp]:
"\<And>irq. arch_mask_irq_signal irq \<lbrace>valid_sched\<rbrace>"
context DetSchedSchedule_AI begin
crunch switch_to_idle_thread, switch_to_thread
for valid_etcbs[wp]: valid_etcbs
(simp: whenE_def)
crunch switch_to_idle_thread, switch_to_thread
for valid_queues[wp]: valid_queues
(simp: whenE_def ignore: set_tcb_queue tcb_sched_action)
crunch
switch_to_idle_thread, switch_to_thread
for weak_valid_sched_action[wp]: "weak_valid_sched_action"
(simp: whenE_def)
end
lemma tcb_sched_action_dequeue_ct_not_in_q_2_ct_upd:
"\<lbrace>valid_queues\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>r s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) thread\<rbrace>"
apply (simp add: tcb_sched_action_def unless_def set_tcb_queue_def)
apply wp
apply (fastforce simp: etcb_at_def ct_not_in_q_def valid_queues_def
tcb_sched_dequeue_def not_queued_def
split: option.split)
done
lemma tcb_sched_action_dequeue_valid_sched_action_2_ct_upd:
"\<lbrace>valid_sched_action and
(\<lambda>s. is_activatable_2 thread (scheduler_action s) (kheap s))\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>r s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) thread (cur_domain s)\<rbrace>"
apply (simp add: tcb_sched_action_def unless_def set_tcb_queue_def)
apply wp
apply (clarsimp simp: etcb_at_def valid_sched_action_def split: option.split)
done
context DetSchedSchedule_AI begin
lemma as_user_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> as_user tptr f \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: as_user_def set_object_def get_object_def)
apply (wp | wpc)+
apply clarsimp
apply (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def
valid_sched_action_def is_activatable_def
weak_valid_sched_action_def st_tcb_at_kh_if_split
st_tcb_def2 valid_blocked_def)
done
lemma tcb_sched_action_dequeue_not_queued[wp]:
"\<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>_. not_queued t\<rbrace>"
unfolding tcb_sched_action_def tcb_sched_dequeue_def
apply wpsimp
apply (clarsimp simp add: valid_queues_def etcb_at_def not_queued_def
split: option.splits)
done
lemma switch_to_thread_ct_not_queued[wp]:
"\<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv s. not_queued (cur_thread s) s\<rbrace>"
unfolding switch_to_thread_def
by wpsimp
end
lemma ct_not_in_q_def2:
"ct_not_in_q_2 queues sa ct = (sa = resume_cur_thread \<longrightarrow> (\<forall>d p. ct \<notin> set (queues d p)))"
by (fastforce simp add: ct_not_in_q_def not_queued_def)
context DetSchedSchedule_AI begin
lemma switch_to_thread_ct_not_in_q[wp]:
"\<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: ct_not_in_q_def2 not_queued_def[symmetric])
apply (wp hoare_drop_imps | simp)+
done
lemma switch_to_thread_valid_sched_action[wp]:
"\<lbrace>valid_sched_action and is_activatable t\<rbrace>
switch_to_thread t
\<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
by (wpsimp wp: tcb_sched_action_dequeue_valid_sched_action_2_ct_upd simp: switch_to_thread_def)
end
lemma tcb_sched_action_dequeue_ct_in_cur_domain':
"\<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_ s. ct_in_cur_domain (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (simp add: etcb_at_def split: option.split)
done
context DetSchedSchedule_AI begin
crunch as_user
for ct_in_cur_domain_2[wp]: "\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)"
(simp: whenE_def get_object_def)
lemma switch_to_thread_ct_in_cur_domain[wp]:
"\<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>
switch_to_thread thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
apply (simp add: switch_to_thread_def)
apply (wpsimp wp: tcb_sched_action_dequeue_ct_in_cur_domain')
done
end
lemma ct_in_q_valid_blocked_ct_upd:
"\<lbrakk>ct_in_q s; valid_blocked s\<rbrakk> \<Longrightarrow> valid_blocked (s\<lparr>cur_thread := thread\<rparr>)"
apply (clarsimp simp: valid_blocked_def ct_in_q_def)
apply (erule_tac x=t in allE)
apply clarsimp
apply (case_tac "t=cur_thread s")