Skip to content

Commit c2525e3

Browse files
Xungan2Xungan2
committed
Temp progress
1 parent e884efd commit c2525e3

5 files changed

Lines changed: 116 additions & 24 deletions

File tree

‎lock-protocol/src/exec/rcu/cursor/locking.rs‎

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -216,9 +216,10 @@ pub(super) fn lock_range<'rcu>(
216216
)
217217
}
218218

219-
pub fn unlock_range(cursor: &mut Cursor<'_>, m: Tracked<LockProtocolModel>) -> (res: Tracked<
220-
LockProtocolModel,
221-
>)
219+
pub fn unlock_range(
220+
cursor: &mut Cursor<'_>,
221+
m: Tracked<LockProtocolModel>
222+
) -> (res: Tracked<LockProtocolModel>)
222223
requires
223224
old(cursor).wf(),
224225
m@.inv(),
@@ -487,7 +488,8 @@ fn dfs_acquire_lock(
487488
// cur_node_va: Vaddr,
488489
// va_range: Range<Vaddr>,
489490
m: Tracked<LockProtocolModel>,
490-
) -> (res: Tracked<LockProtocolModel>)
491+
forgot_guards: Tracked<SubTreeForgotGuard>,
492+
) -> (res: (Tracked<LockProtocolModel>, Tracked<SubTreeForgotGuard>))
491493
requires
492494
cur_node.wf(),
493495
cur_node.guard->Some_0.stray_perm().value() == false,
@@ -498,15 +500,17 @@ fn dfs_acquire_lock(
498500
m@.cur_node() == cur_node.nid() + 1,
499501
m@.node_is_locked(cur_node.nid()),
500502
ensures
501-
res@.inv(),
502-
res@.inst_id() == cur_node.inst_id(),
503-
res@.state() is Locking,
504-
res@.sub_tree_rt() == m@.sub_tree_rt(),
505-
res@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
503+
res.0@.inv(),
504+
res.0@.inst_id() == cur_node.inst_id(),
505+
res.0@.state() is Locking,
506+
res.0@.sub_tree_rt() == m@.sub_tree_rt(),
507+
res.0@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
506508
decreases cur_node.deref().deref().level_spec(),
507509
{
508510
broadcast use crate::spec::utils::group_node_helper_lemmas;
509511

512+
let tracked mut forgot_guards = forgot_guards.get();
513+
510514
let cur_level = cur_node.deref().deref().level();
511515
if cur_level == 1 {
512516
assert(m@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid())) by {
@@ -579,8 +583,14 @@ fn dfs_acquire_lock(
579583
proof {
580584
m = res.get();
581585
}
586+
// Forget the page table guard.
587+
assert(pt_guard.guard is Some);
588+
let tracked guard = pt_guard.guard.tracked_unwrap()
589+
let tracked forgot_guard = guard.inner.get();
590+
proof {
591+
forgot_guards.tracked_put(, forgot_guard);
592+
}
582593
let _ = ManuallyDrop::new(pt_guard);
583-
584594
},
585595
ChildRef::Frame(_, _, _) => unreached(),
586596
ChildRef::None => {

‎lock-protocol/src/exec/rcu/node/mod.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -613,7 +613,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
613613
self.guard->Some_0.stray_perm() == old(self).guard->Some_0.stray_perm(),
614614
self.guard->Some_0.perms() == old(self).guard->Some_0.perms(),
615615
self.guard->Some_0.in_protocol() == old(self).guard->Some_0.in_protocol(),
616-
self.guard->Some_0.handle == old(self).guard->Some_0.handle,
616+
self.guard->Some_0.handle() == old(self).guard->Some_0.handle(),
617617
self.inner == old(self).inner,
618618
self.guard is Some,
619619
{
@@ -634,7 +634,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
634634
self.guard->Some_0.stray_perm() == old(self).guard->Some_0.stray_perm(),
635635
self.guard->Some_0.perms() == old(self).guard->Some_0.perms(),
636636
self.guard->Some_0.in_protocol() == old(self).guard->Some_0.in_protocol(),
637-
self.guard->Some_0.handle == old(self).guard->Some_0.handle,
637+
self.guard->Some_0.handle() == old(self).guard->Some_0.handle(),
638638
self.inner == old(self).inner,
639639
self.guard is Some,
640640
{
@@ -652,7 +652,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
652652
self.guard->Some_0.pte_token() == old(self).guard->Some_0.pte_token(),
653653
self.guard->Some_0.stray_perm() == old(self).guard->Some_0.stray_perm(),
654654
self.guard->Some_0.perms() == old(self).guard->Some_0.perms(),
655-
self.guard->Some_0.handle == old(self).guard->Some_0.handle,
655+
self.guard->Some_0.handle() == old(self).guard->Some_0.handle(),
656656
self.inner == old(self).inner,
657657
self.guard is Some,
658658
{

‎lock-protocol/src/exec/rcu/node/spinlock/guard_forget.rs‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
use vstd::prelude::*;
2+
3+
use crate::spec::{common::*, utils::*, rcu::*};
4+
use super::super::{common::*, cpu::*};
5+
use super::SpinGuardGhostInner;
6+
7+
verus! {
8+
9+
pub tracked struct SubTreeForgotGuard<C: PageTableConfig> {
10+
pub guards: Map<NodeId, SpinGuardGhostInner<C>>,
11+
}
12+
13+
impl<C: PageTableConfig> SubTreeForgotGuard<C> {
14+
pub open spec fn wf(&self) -> bool {
15+
&&& forall |nid: NodeId| self.guards.dom().contains(nid) ==> {
16+
&&& NodeHelper::valid_nid(nid)
17+
&&& self.guards[nid].relate_nid(nid)
18+
}
19+
}
20+
21+
pub open spec fn put_spec(self, nid: NodeId, guard: SpinGuardGhostInner<C>) -> Self {
22+
Self {
23+
guards: self.guards.insert(nid, guard)
24+
}
25+
}
26+
27+
pub proof fn tracked_put(tracked &mut self, nid: NodeId, tracked guard: SpinGuardGhostInner<C>)
28+
requires
29+
old(self).wf(),
30+
!self.guards.dom().contains(nid),
31+
NodeHelper::valid_nid(nid),
32+
guard.relate_nid(nid),
33+
ensures
34+
self =~= old(self).put_spec(nid, guard),
35+
self.wf(),
36+
{
37+
self.guards.tracked_insert(nid, guard)
38+
}
39+
40+
pub open spec fn take_spec(self, nid: NodeId) -> Self {
41+
Self {
42+
guards: self.guards.remove(nid)
43+
}
44+
}
45+
46+
pub proof fn tracked_take(tracked &mut self, nid: NodeId) -> (tracked guard: SpinGuardGhostInner<C>)
47+
requires
48+
old(self).wf(),
49+
self.guards.dom().contains(nid),
50+
NodeHelper::valid_nid(nid),
51+
ensures
52+
self =~= old(self).take_spec(nid),
53+
self.wf(),
54+
guard.relate_nid(nid),
55+
{
56+
self.guards.tracked_remove(nid)
57+
}
58+
}
59+
60+
}

‎lock-protocol/src/exec/rcu/node/spinlock/mod.rs‎

Lines changed: 31 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,15 @@ impl<C: PageTableConfig> PageTableEntryPerms<C> {
123123
}
124124
}
125125

126+
pub open spec fn relate_nid(&self, nid: NodeId) -> bool {
127+
forall|i: int|
128+
#![trigger self.inner.value()[i]]
129+
0 <= i < 512 ==> {
130+
self.inner.value()[i].nid@ is Some ==>
131+
self.inner.value()[i].nid@->Some_0 == NodeHelper::get_child(nid, i as nat)
132+
}
133+
}
134+
126135
pub open spec fn addr(&self) -> Vaddr {
127136
self.inner.addr()
128137
}
@@ -247,6 +256,7 @@ struct_with_invariants! {
247256
}
248257

249258
pub tracked struct SpinGuardGhostInner<C: PageTableConfig> {
259+
pub handle: SpinGuardToken<C>,
250260
pub node_token: Option<NodeToken>,
251261
pub pte_token: Option<PteArrayToken>,
252262
pub stray_perm: StrayPerm,
@@ -313,25 +323,35 @@ impl<C: PageTableConfig> SpinGuardGhostInner<C> {
313323
&&& self.perms.wf(spinlock.paddr@, spinlock.level@, spinlock.pt_inst@.id(), spinlock.nid@)
314324
&&& self.perms.addr() == paddr_to_vaddr(spinlock.paddr@)
315325
}
326+
327+
pub open spec fn relate_nid(self, nid: NodeId) -> bool {
328+
&&& self.node_token is Some ==> self.node_token->Some_0.key() == nid
329+
&&& self.pte_token is Some ==> self.pte_token->Some_0.key() == nid
330+
&&& self.stray_perm.nid() == nid
331+
&&& self.perms.relate_nid(nid)
332+
}
316333
}
317334

318335
pub struct SpinGuard<C: PageTableConfig> {
319-
pub handle: Tracked<SpinGuardToken<C>>,
320336
pub inner: Tracked<SpinGuardGhostInner<C>>,
321337
}
322338

323339
impl<C: PageTableConfig> SpinGuard<C> {
324340
pub open spec fn wf(self, spinlock: &PageTablePageSpinLock<C>) -> bool {
325-
&&& self.handle@.instance_id() == spinlock.inst@.id()
341+
&&& self.handle().instance_id() == spinlock.inst@.id()
326342
&&& self.inner@.wf(spinlock)
327343
}
328344

329345
/// Used in PageTableGuard::write_pte
330346
pub open spec fn wf_except(self, spinlock: &PageTablePageSpinLock<C>, idx: nat) -> bool {
331-
&&& self.handle@.instance_id() == spinlock.inst@.id()
347+
&&& self.handle().instance_id() == spinlock.inst@.id()
332348
&&& self.inner@.wf_except(spinlock, idx)
333349
}
334350

351+
pub open spec fn handle(&self) -> SpinGuardToken<C> {
352+
self.inner@.handle
353+
}
354+
335355
pub open spec fn node_token(&self) -> Option<NodeToken> {
336356
self.inner@.node_token
337357
}
@@ -394,7 +414,7 @@ impl<C: PageTableConfig> SpinGuard<C> {
394414
self.stray_perm() == old(self).stray_perm(),
395415
self.perms() == old(self).perms(),
396416
self.in_protocol() == old(self).in_protocol(),
397-
self.handle == old(self).handle,
417+
self.handle() == old(self).handle(),
398418
{
399419
let tracked res = self.inner.borrow_mut().node_token.tracked_take();
400420
Tracked(res)
@@ -410,7 +430,7 @@ impl<C: PageTableConfig> SpinGuard<C> {
410430
self.stray_perm() == old(self).stray_perm(),
411431
self.perms() == old(self).perms(),
412432
self.in_protocol() == old(self).in_protocol(),
413-
self.handle == old(self).handle,
433+
self.handle() == old(self).handle(),
414434
{
415435
unimplemented!()
416436
}
@@ -423,7 +443,7 @@ impl<C: PageTableConfig> SpinGuard<C> {
423443
self.pte_token() == old(self).pte_token(),
424444
self.stray_perm() == old(self).stray_perm(),
425445
self.perms() == old(self).perms(),
426-
self.handle == old(self).handle,
446+
self.handle() == old(self).handle(),
427447
{
428448
proof {
429449
self.inner.borrow_mut().in_protocol = in_protocol.get();
@@ -527,8 +547,8 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
527547
}
528548
}
529549
let guard = SpinGuard {
530-
handle: Tracked(handle),
531550
inner: Tracked(SpinGuardGhostInner {
551+
handle: handle,
532552
node_token: node_token,
533553
pte_token: pte_token,
534554
stray_perm: stray_perm,
@@ -641,8 +661,8 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
641661
node_token = self.pt_inst.borrow().normal_lock(self.nid@, node_token);
642662
}
643663
let guard = SpinGuard {
644-
handle: Tracked(handle),
645664
inner: Tracked(SpinGuardGhostInner {
665+
handle: handle,
646666
node_token: Some(node_token),
647667
pte_token: Some(pte_token),
648668
stray_perm: stray_perm,
@@ -667,8 +687,8 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
667687
guard.wf(self),
668688
guard.in_protocol() == false,
669689
{
670-
let tracked handle = guard.handle.get();
671690
let tracked inner = guard.inner.get();
691+
let tracked handle = inner.handle;
672692
let tracked mut node_token: Option<NodeToken> = inner.node_token;
673693
let tracked pte_token: Option<PteArrayToken> = inner.pte_token;
674694
let tracked stray_perm: StrayPerm = inner.stray_perm;
@@ -819,8 +839,8 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
819839
m.token = res.1.get();
820840
}
821841
let guard = SpinGuard {
822-
handle: Tracked(handle),
823842
inner: Tracked(SpinGuardGhostInner {
843+
handle: handle,
824844
node_token: Some(node_token),
825845
pte_token: Some(pte_token),
826846
stray_perm: stray_perm,
@@ -860,8 +880,8 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
860880
res@.cur_node() == self.nid(),
861881
{
862882
let tracked m = m.get();
863-
let tracked handle = guard.handle.get();
864883
let tracked inner = guard.inner.get();
884+
let tracked handle = inner.handle;
865885
let tracked mut node_token: NodeToken = inner.node_token.tracked_unwrap();
866886
let tracked pte_token: PteArrayToken = inner.pte_token.tracked_unwrap();
867887
let tracked stray_perm: StrayPerm = inner.stray_perm;

‎lock-protocol/src/spec/sub_pt/mod.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,8 @@ pub tracked struct SubPageTable<C: PageTableConfig> {
5050
pub frames: SubPageTableStateMachine::frames<C>,
5151
pub i_ptes: SubPageTableStateMachine::i_ptes<C>,
5252
pub ptes: SubPageTableStateMachine::ptes<C>,
53+
54+
5355
}
5456

5557
impl<C: PageTableConfig> SubPageTable<C> {

0 commit comments

Comments
 (0)