-
Notifications
You must be signed in to change notification settings - Fork 0
/
table_unmap.v
128 lines (122 loc) · 6.22 KB
/
table_unmap.v
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
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import TableWalk.Spec.
Require Import AbsAccessor.Spec.
Require Import TableAux.Spec.
Local Open Scope Z_scope.
Section Spec.
Definition unmap_table (llt_gidx: Z) (idx: Z) (level: Z) (map_addr: Z) (adt: RData) :=
let gn_llt := (gs (share adt)) @ llt_gidx in
rely (g_tag (ginfo gn_llt) =? GRANULE_STATE_TABLE);
rely (gtype gn_llt =? GRANULE_STATE_TABLE);
let llt_pte := (g_data (gnorm gn_llt)) @ idx in
rely is_int64 llt_pte;
if (level <? RTT_PAGE_LEVEL) && (__entry_is_table llt_pte) then
Some (adt {log: EVT CPU_ID (REL llt_gidx gn_llt {glock: Some CPU_ID}) :: log adt}, VZ64 1)
else
let data_addr := PTE_TO_PA llt_pte in
let ipa_state := PTE_TO_IPA_STATE llt_pte in
let ipa_gidx := __addr_to_gidx map_addr in
if ipa_state =? IPA_STATE_PRESENT then
let new_pgte := Z.lor (IPA_STATE_TO_PTE IPA_STATE_ABSENT) data_addr in
let llt' := (g_data (gnorm gn_llt)) # idx == new_pgte in
let gllt' := gn_llt {gnorm: (gnorm gn_llt) {g_data: llt'}} in
let tlbs' := (fun cpu gidx => if gidx =? ipa_gidx then -1 else tlbs (share adt) cpu gidx) in
Some (adt {log: EVT CPU_ID (REL llt_gidx gllt' {glock: Some CPU_ID}) :: log adt}
{share : (share adt) {gs : (gs (share adt)) # llt_gidx == gllt'} {tlbs: tlbs'}}, VZ64 0)
else
Some (adt {log: EVT CPU_ID (REL llt_gidx gn_llt {glock: Some CPU_ID}) :: log adt}, VZ64 1).
Definition table_unmap_spec (g_rd: Pointer) (map_addr: Z64) (level: Z64) (adt: RData) : option (RData * Z64) :=
match map_addr, level with
| VZ64 map_addr, VZ64 level =>
rely is_int64 map_addr; rely (level >=? 3); rely GRANULE_ALIGNED map_addr;
let idx0 := __addr_to_idx map_addr 0 in
let idx1 := __addr_to_idx map_addr 1 in
let idx2 := __addr_to_idx map_addr 2 in
let idx3 := __addr_to_idx map_addr 3 in
let ret_idx := (if level =? 1 then idx0 else if level =? 2 then idx1 else if level =? 3 then idx2 else idx3) in
rely (peq (base g_rd) ginfo_loc);
rely prop_dec ((buffer (priv adt)) @ SLOT_RD = None);
rely prop_dec ((buffer (priv adt)) @ SLOT_TABLE = None);
let rd_gidx := (offset g_rd) in
let grd := (gs (share adt)) @ rd_gidx in
rely (g_tag (ginfo grd) =? GRANULE_STATE_RD);
rely prop_dec (glock grd = Some CPU_ID);
let root_gidx := (g_rtt (gnorm grd)) in
rely is_gidx rd_gidx; rely is_gidx root_gidx;
when adt == query_oracle adt;
(* hold root lock *)
let adt := adt {log: EVT CPU_ID (ACQ root_gidx) :: log adt} in
let groot := (gs (share adt)) @ root_gidx in
rely (tbl_level (gaux groot) =? 0);
rely prop_dec (glock groot = None);
rely (g_tag (ginfo groot) =? GRANULE_STATE_TABLE);
rely (gtype groot =? GRANULE_STATE_TABLE);
(* walk deeper root *)
let entry0 := (g_data (gnorm groot)) @ idx0 in
rely is_int64 entry0;
let phys0 := __entry_to_phys entry0 3 in
let lv1_gidx := __addr_to_gidx phys0 in
if (__entry_is_table entry0) && (GRANULE_ALIGNED phys0) && (is_gidx lv1_gidx) then
(* level 1 valid, hold level 1 lock *)
let adt := adt {log: EVT CPU_ID (REL root_gidx groot {glock: Some CPU_ID}) :: EVT CPU_ID (ACQ lv1_gidx) :: log adt} in
let glv1 := (gs (share adt)) @ lv1_gidx in
rely prop_dec (glock glv1 = None);
rely (tbl_level (gaux glv1) =? 1);
(* walk deeper level 1 *)
rely (g_tag (ginfo glv1) =? GRANULE_STATE_TABLE);
rely (gtype glv1 =? GRANULE_STATE_TABLE);
let entry1 := (g_data (gnorm glv1)) @ idx1 in
rely is_int64 entry1;
let phys1 := __entry_to_phys entry1 3 in
let lv2_gidx := __addr_to_gidx phys1 in
if (__entry_is_table entry1) && (GRANULE_ALIGNED phys1) && (is_gidx lv2_gidx) then
(* level 2 valid, hold level 2 lock *)
when adt == query_oracle adt;
let adt := adt {log: EVT CPU_ID (REL lv1_gidx glv1 {glock: Some CPU_ID}) :: EVT CPU_ID (ACQ lv2_gidx) :: log adt} in
let glv2 := (gs (share adt)) @ lv2_gidx in
rely (tbl_level (gaux glv2) =? 2);
rely prop_dec (glock glv2 = None);
if level =? 3 then
(* walk until level 2 *)
let adt := adt {priv: (priv adt) {wi_llt: lv2_gidx} {wi_index: idx2}} in
unmap_table lv2_gidx idx2 level map_addr adt
else
(* walk deeper level 2 *)
rely (g_tag (ginfo glv2) =? GRANULE_STATE_TABLE);
rely (gtype glv2 =? GRANULE_STATE_TABLE);
let entry2 := (g_data (gnorm glv2)) @ idx2 in
rely is_int64 entry2;
let phys2 := __entry_to_phys entry2 3 in
let lv3_gidx := __addr_to_gidx phys2 in
if (__entry_is_table entry2) && (GRANULE_ALIGNED phys2) && (is_gidx lv3_gidx) then
(* level 2 valid, hold level 2 lock *)
when adt == query_oracle adt;
let adt := adt {log: EVT CPU_ID (REL lv2_gidx glv2 {glock: Some CPU_ID}) :: EVT CPU_ID (ACQ lv3_gidx) :: log adt} in
let glv3 := (gs (share adt)) @ lv3_gidx in
rely prop_dec (glock glv3 = None);
rely (tbl_level (gaux glv3) =? 3);
if level =? 4 then
(* walk until level 3 *)
let adt := adt {priv: (priv adt) {wi_llt: lv3_gidx} {wi_index: idx3}} in
unmap_table lv3_gidx idx3 level map_addr adt
else (* can't be other level *)
None
else
(* level 3 invalid *)
Some (adt {log: EVT CPU_ID (REL lv2_gidx glv2 {glock: Some CPU_ID}) :: log adt}
{priv: (priv adt) {wi_llt: 0} {wi_index: ret_idx}}, VZ64 1)
else
(* level 2 invalid *)
Some (adt {log: EVT CPU_ID (REL lv1_gidx glv1 {glock: Some CPU_ID}) :: log adt}
{priv: (priv adt) {wi_llt: 0} {wi_index: ret_idx}}, VZ64 1)
else
(* level 1 invalid *)
Some (adt {log: EVT CPU_ID (REL root_gidx groot {glock: Some CPU_ID}) :: log adt}
{priv: (priv adt) {wi_llt: 0} {wi_index: ret_idx}}, VZ64 1)
end.
End Spec.