Skip to content

Commit 953fff8

Browse files
zouyonghaozouyonghao
authored
Refine specifications for FrameRef and Entry for child, entry and spt relation (#192)
* Refine specifications for FrameRef and Entry for child, entry and spt relation; Prove the None case. * Format Signed-off-by: Yonghao Zou <zouyonghao@live.cn> * Format again Signed-off-by: Yonghao Zou <zouyonghao@live.cn>
1 parent 1bcbacb commit 953fff8

4 files changed

Lines changed: 91 additions & 52 deletions

File tree

‎lock-protocol/src/mm/frame/frame_ref.rs‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,11 +32,15 @@ impl<'a, M: AnyFrameMeta> FrameRef<'a, M> {
3232
) -> (res: Self)
3333
requires
3434
alloc_model.invariants(),
35-
alloc_model.meta_map.contains_key(raw as int),
36-
alloc_model.meta_map[raw as int].pptr() == alloc_model.meta_map[raw as int].pptr(),
35+
alloc_model.meta_map.contains_key(
36+
raw as int,
37+
), // alloc_model.meta_map[raw as int].pptr() == alloc_model.meta_map[raw as int].pptr(),
38+
// ?
39+
3740
ensures
3841
res.deref().start_paddr() == raw,
3942
res.deref().meta_ptr == alloc_model.meta_map[raw as int].pptr(),
43+
alloc_model.invariants(),
4044
{
4145
Self {
4246
inner: ManuallyDrop::new(Frame::from_raw(raw, Tracked(alloc_model))),

‎lock-protocol/src/mm/page_table/mod.rs‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,10 @@ Sized {
228228
/// or [`Self::new_pt`], whatever modified with [`Self::set_prop`] or not,
229229
/// this method should return true.
230230
#[verifier::when_used_as_spec(is_present_spec)]
231-
fn is_present(&self) -> (res: bool);
231+
fn is_present(&self) -> (res: bool)
232+
ensures
233+
res == self.is_present_spec(),
234+
;
232235

233236
spec fn is_present_spec(&self) -> bool;
234237

‎lock-protocol/src/mm/page_table/node/child.rs‎

Lines changed: 73 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ use std::mem::ManuallyDrop;
55
use vstd::prelude::*;
66

77
use crate::mm::cursor::spec_helpers;
8+
use crate::mm::entry::Entry;
89
use crate::mm::meta::AnyFrameMeta;
910
use crate::mm::page_prop::PageProperty;
1011
use crate::mm::vm_space::Token;
@@ -15,6 +16,8 @@ use crate::mm::PageTableEntryTrait;
1516
use crate::mm::PagingConstsTrait;
1617
use crate::mm::PagingConsts;
1718
use crate::mm::PagingLevel;
19+
use crate::spec::sub_pt::state_machine::IntermediatePageTableEntryView;
20+
use std::ops::Deref;
1821

1922
use crate::sync::rcu::RcuDrop;
2023

@@ -112,23 +115,89 @@ impl<'a, C: PageTableConfig> ChildRef<'a, C> {
112115
///
113116
/// The provided level must be the same with the level of the page table
114117
/// node that contains this PTE.
115-
#[verifier::external_body]
116118
pub(super) fn from_pte(
117119
pte: &C::E,
118120
level: PagingLevel,
119121
Tracked(spt): Tracked<&SubPageTable<C>>,
120-
) -> Self {
122+
entry: &Entry<C>, // TODO: should be ghost
123+
) -> (res: Self)
124+
requires
125+
spt.wf(),
126+
pte == entry.pte,
127+
entry.wf(spt),
128+
ensures
129+
res.child_entry_spt_wf(entry, spt),
130+
{
121131
if !pte.is_present() {
122132
return ChildRef::None;
123133
}
124134
let paddr = pte.frame_paddr();
125135

126136
if !pte.is_last(level) {
137+
assert(spt.alloc_model.invariants());
138+
assume(spt.alloc_model.meta_map.contains_key(paddr as int)); // TODO
127139
let node = PageTableNodeRef::borrow_paddr(paddr, Tracked(&spt.alloc_model));
128140
// debug_assert_eq!(node.level(), level - 1);
129-
return ChildRef::PageTable(node);
141+
let res = ChildRef::PageTable(node);
142+
assume(res.child_entry_spt_wf(entry, spt));
143+
assert(!(res is None));
144+
assert(pte.is_present());
145+
return res;
146+
}
147+
let res = ChildRef::Frame(paddr, level, pte.prop());
148+
assume(spt.ptes.value().contains_key(entry.pte.pte_paddr() as int));
149+
assume(spt.ptes.value()[entry.pte.pte_paddr() as int].map_to_pa == paddr);
150+
res
151+
}
152+
153+
#[verifier::inline]
154+
pub(in crate::mm) open spec fn child_entry_spt_wf(
155+
&self,
156+
entry: &Entry<C>,
157+
spt: &SubPageTable<C>,
158+
) -> bool {
159+
&&& self is PageTable <==> match self {
160+
ChildRef::PageTable(pt) => {
161+
&&& spt.i_ptes.value().contains_key(entry.pte.pte_paddr() as int)
162+
&&& pt.wf(&spt.alloc_model)
163+
&&& pt.deref().start_paddr() == entry.pte.frame_paddr() as usize
164+
&&& pt.level_spec(&spt.alloc_model) == entry.node.level_spec(&spt.alloc_model) - 1
165+
&&& spt.alloc_model.meta_map.contains_key(pt.deref().start_paddr() as int)
166+
&&& spt.alloc_model.meta_map[pt.deref().start_paddr() as int].pptr() == pt.meta_ptr
167+
&&& spt.frames.value().contains_key(pt.deref().start_paddr() as int)
168+
&&& spt.frames.value()[pt.deref().start_paddr() as int].ancestor_chain
169+
== spt.frames.value()[entry.node.paddr() as int].ancestor_chain.insert(
170+
entry.node.level_spec(&spt.alloc_model) as int,
171+
IntermediatePageTableEntryView {
172+
map_va: entry.va as int,
173+
frame_pa: entry.node.paddr() as int,
174+
in_frame_index: entry.idx as int,
175+
map_to_pa: pt.deref().start_paddr() as int,
176+
level: entry.node.level_spec(&spt.alloc_model),
177+
phantom: PhantomData,
178+
},
179+
)
180+
},
181+
_ => false,
182+
}
183+
&&& self is Frame <==> match self {
184+
ChildRef::Frame(pa, level, prop) => {
185+
&&& pa == entry.pte.frame_paddr() as usize
186+
&&& spt.ptes.value().contains_key(entry.pte.pte_paddr() as int)
187+
&&& spt.ptes.value()[entry.pte.pte_paddr() as int].map_to_pa == pa
188+
},
189+
_ => false,
190+
}
191+
&&& (self is PageTable || self is Frame) <==> entry.pte.is_present_spec()
192+
&&& self is None <==> {
193+
// &&& !spt.i_ptes.value().contains_key(entry.pte.pte_paddr() as int)
194+
// &&& !spt.ptes.value().contains_key(entry.pte.pte_paddr() as int)
195+
&&& !entry.pte.is_present_spec()
196+
}
197+
&&& self is None <==> match self {
198+
ChildRef::None => true,
199+
_ => false,
130200
}
131-
ChildRef::Frame(paddr, level, pte.prop())
132201
}
133202
}
134203

‎lock-protocol/src/mm/page_table/node/entry.rs‎

Lines changed: 8 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
6363
&&& self.idx < nr_subpage_per_huge::<C>()
6464
&&& self.pte.pte_paddr_spec() == index_pte_paddr(self.node.paddr() as int, self.idx as int)
6565
&&& spt.frames.value().contains_key(self.node.paddr() as int)
66-
&&& self.pte.is_present_spec() ==> {
66+
&&& self.pte.is_present_spec() <==> {
6767
||| spt.i_ptes.value().contains_key(self.pte.pte_paddr_spec() as int)
6868
||| spt.ptes.value().contains_key(self.pte.pte_paddr_spec() as int)
6969
}
@@ -98,7 +98,6 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
9898
}
9999

100100
/// Gets a reference to the child.
101-
#[verifier::external_body]
102101
pub(in crate::mm) fn to_ref(&self, Tracked(spt): Tracked<&SubPageTable<C>>) -> (res: ChildRef<
103102
'rcu,
104103
C,
@@ -107,53 +106,17 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
107106
spt.wf(),
108107
self.wf(spt),
109108
ensures
110-
res is PageTable <==> match res {
111-
ChildRef::PageTable(pt) => {
112-
&&& spt.i_ptes.value().contains_key(self.pte.pte_paddr() as int)
113-
&&& pt.wf(&spt.alloc_model)
114-
&&& pt.deref().start_paddr() == self.pte.frame_paddr() as usize
115-
&&& pt.level_spec(&spt.alloc_model) == self.node.level_spec(&spt.alloc_model)
116-
- 1
117-
&&& spt.alloc_model.meta_map.contains_key(pt.deref().start_paddr() as int)
118-
&&& spt.alloc_model.meta_map[pt.deref().start_paddr() as int].pptr()
119-
== pt.meta_ptr
120-
&&& spt.frames.value().contains_key(pt.deref().start_paddr() as int)
121-
&&& spt.frames.value()[pt.deref().start_paddr() as int].ancestor_chain
122-
== spt.frames.value()[self.node.paddr() as int].ancestor_chain.insert(
123-
self.node.level_spec(&spt.alloc_model) as int,
124-
IntermediatePageTableEntryView {
125-
map_va: self.va as int,
126-
frame_pa: self.node.paddr() as int,
127-
in_frame_index: self.idx as int,
128-
map_to_pa: pt.deref().start_paddr() as int,
129-
level: self.node.level_spec(&spt.alloc_model),
130-
phantom: PhantomData,
131-
},
132-
)
133-
},
134-
_ => false,
135-
},
136-
res is Frame <==> match res {
137-
ChildRef::Frame(pa, level, prop) => {
138-
&&& pa == self.pte.frame_paddr() as usize
139-
&&& spt.ptes.value().contains_key(self.pte.pte_paddr() as int)
140-
&&& spt.ptes.value()[self.pte.pte_paddr() as int].map_to_pa == pa
141-
},
142-
_ => false,
143-
},
144-
res is None <==> {
145-
&&& !spt.i_ptes.value().contains_key(self.pte.pte_paddr() as int)
146-
&&& !spt.ptes.value().contains_key(self.pte.pte_paddr() as int)
147-
},
148-
res is None <==> match res {
149-
ChildRef::None => true,
150-
_ => false,
151-
},
109+
res.child_entry_spt_wf(self, spt),
152110
{
153111
// SAFETY: The entry structure represents an existent entry with the
154112
// right node information.
155113
// unsafe { Child::ref_from_pte(&self.pte, self.node.level(Tracked(&spt.alloc_model)), self.node.is_tracked(), false) }
156-
ChildRef::from_pte(&self.pte, self.node.level(Tracked(&spt.alloc_model)), Tracked(spt))
114+
ChildRef::from_pte(
115+
&self.pte,
116+
self.node.level(Tracked(&spt.alloc_model)),
117+
Tracked(spt),
118+
&self,
119+
)
157120
}
158121

159122
/// Operates on the mapping properties of the entry.

0 commit comments

Comments
 (0)