Skip to content

Commit 50f1f93

Browse files
Xungan2Xungan2
committed
fmt
1 parent 70f7fd4 commit 50f1f93

13 files changed

Lines changed: 107 additions & 107 deletions

File tree

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
// mod rcu;
22
// mod rw;
33
// mod test_map;
4-
54
use vstd::{invariant, prelude::*};
65
use core::num;
76
use std::collections::HashMap;

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

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,16 +12,15 @@ pub tracked struct SubTreeForgotGuard<C: PageTableConfig> {
1212

1313
impl<C: PageTableConfig> SubTreeForgotGuard<C> {
1414
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-
}
15+
&&& forall|nid: NodeId|
16+
self.guards.dom().contains(nid) ==> {
17+
&&& NodeHelper::valid_nid(nid)
18+
&&& self.guards[nid].relate_nid(nid)
19+
}
1920
}
2021

2122
pub open spec fn put_spec(self, nid: NodeId, guard: SpinGuardGhostInner<C>) -> Self {
22-
Self {
23-
guards: self.guards.insert(nid, guard)
24-
}
23+
Self { guards: self.guards.insert(nid, guard) }
2524
}
2625

2726
pub proof fn tracked_put(tracked &mut self, nid: NodeId, tracked guard: SpinGuardGhostInner<C>)
@@ -38,12 +37,11 @@ impl<C: PageTableConfig> SubTreeForgotGuard<C> {
3837
}
3938

4039
pub open spec fn take_spec(self, nid: NodeId) -> Self {
41-
Self {
42-
guards: self.guards.remove(nid)
43-
}
40+
Self { guards: self.guards.remove(nid) }
4441
}
4542

46-
pub proof fn tracked_take(tracked &mut self, nid: NodeId) -> (tracked guard: SpinGuardGhostInner<C>)
43+
pub proof fn tracked_take(tracked &mut self, nid: NodeId) -> (tracked guard:
44+
SpinGuardGhostInner<C>)
4745
requires
4846
old(self).wf(),
4947
self.guards.dom().contains(nid),
@@ -57,4 +55,4 @@ impl<C: PageTableConfig> SubTreeForgotGuard<C> {
5755
}
5856
}
5957

60-
}
58+
} // verus!

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

Lines changed: 32 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -127,8 +127,8 @@ impl<C: PageTableConfig> PageTableEntryPerms<C> {
127127
forall|i: int|
128128
#![trigger self.inner.value()[i]]
129129
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)
130+
self.inner.value()[i].nid@ is Some ==> self.inner.value()[i].nid@->Some_0
131+
== NodeHelper::get_child(nid, i as nat)
132132
}
133133
}
134134

@@ -547,14 +547,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
547547
}
548548
}
549549
let guard = SpinGuard {
550-
inner: Tracked(SpinGuardGhostInner {
551-
handle: handle,
552-
node_token: node_token,
553-
pte_token: pte_token,
554-
stray_perm: stray_perm,
555-
perms: perms,
556-
in_protocol: false,
557-
}),
550+
inner: Tracked(
551+
SpinGuardGhostInner {
552+
handle: handle,
553+
node_token: node_token,
554+
pte_token: pte_token,
555+
stray_perm: stray_perm,
556+
perms: perms,
557+
in_protocol: false,
558+
},
559+
),
558560
};
559561
assert(guard.wf(self));
560562
guard_opt = Some(guard);
@@ -661,14 +663,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
661663
node_token = self.pt_inst.borrow().normal_lock(self.nid@, node_token);
662664
}
663665
let guard = SpinGuard {
664-
inner: Tracked(SpinGuardGhostInner {
665-
handle: handle,
666-
node_token: Some(node_token),
667-
pte_token: Some(pte_token),
668-
stray_perm: stray_perm,
669-
perms: perms,
670-
in_protocol: false,
671-
})
666+
inner: Tracked(
667+
SpinGuardGhostInner {
668+
handle: handle,
669+
node_token: Some(node_token),
670+
pte_token: Some(pte_token),
671+
stray_perm: stray_perm,
672+
perms: perms,
673+
in_protocol: false,
674+
},
675+
),
672676
};
673677
assert(guard.wf(self));
674678
guard_opt = Some(guard);
@@ -839,14 +843,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
839843
m.token = res.1.get();
840844
}
841845
let guard = SpinGuard {
842-
inner: Tracked(SpinGuardGhostInner {
843-
handle: handle,
844-
node_token: Some(node_token),
845-
pte_token: Some(pte_token),
846-
stray_perm: stray_perm,
847-
perms: perms,
848-
in_protocol: true,
849-
}),
846+
inner: Tracked(
847+
SpinGuardGhostInner {
848+
handle: handle,
849+
node_token: Some(node_token),
850+
pte_token: Some(pte_token),
851+
stray_perm: stray_perm,
852+
perms: perms,
853+
in_protocol: true,
854+
},
855+
),
850856
};
851857
assert(guard.wf(self));
852858
guard_opt = Some(guard);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
pub mod meta;
1+
pub mod meta;

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
pub mod configs;
21
pub mod common;
2+
pub mod configs;
33

44
pub use configs::*;
5-
pub use common::*;
5+
pub use common::*;

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
pub mod frame;
2+
pub mod frame_concurrent;
3+
pub mod lock_protocol_utils;
24
pub(crate) mod page_prop;
35
pub mod page_table;
46
pub mod vm_space;
5-
pub mod frame_concurrent;
6-
pub mod lock_protocol_utils;
77

88
use std::ops::Range;
99

‎lock-protocol/src/mm/page_table/cursor/locking.rs‎

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

219-
pub fn unlock_range(
220-
cursor: &mut Cursor<'_>,
221-
m: Tracked<LockProtocolModel>
222-
) -> (res: Tracked<LockProtocolModel>)
219+
pub fn unlock_range(cursor: &mut Cursor<'_>, m: Tracked<LockProtocolModel>) -> (res: Tracked<
220+
LockProtocolModel,
221+
>)
223222
requires
224223
old(cursor).wf(),
225224
m@.inv(),
@@ -487,9 +486,11 @@ fn dfs_acquire_lock(
487486
cur_node: &PageTableGuard<'_>,
488487
// cur_node_va: Vaddr,
489488
// va_range: Range<Vaddr>,
490-
m: Tracked<LockProtocolModel>,
489+
m: Tracked<
490+
LockProtocolModel,
491+
>,
491492
// forgot_guards: Tracked<SubTreeForgotGuard>,
492-
// ) -> (res: (Tracked<LockProtocolModel>, Tracked<SubTreeForgotGuard>))
493+
// ) -> (res: (Tracked<LockProtocolModel>, Tracked<SubTreeForgotGuard>))
493494
) -> (res: Tracked<LockProtocolModel>)
494495
requires
495496
cur_node.wf(),
@@ -501,11 +502,12 @@ fn dfs_acquire_lock(
501502
m@.cur_node() == cur_node.nid() + 1,
502503
m@.node_is_locked(cur_node.nid()),
503504
ensures
504-
// res.0@.inv(),
505-
// res.0@.inst_id() == cur_node.inst_id(),
506-
// res.0@.state() is Locking,
507-
// res.0@.sub_tree_rt() == m@.sub_tree_rt(),
508-
// res.0@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
505+
// res.0@.inv(),
506+
// res.0@.inst_id() == cur_node.inst_id(),
507+
// res.0@.state() is Locking,
508+
// res.0@.sub_tree_rt() == m@.sub_tree_rt(),
509+
// res.0@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
510+
509511
res@.inv(),
510512
res@.inst_id() == cur_node.inst_id(),
511513
res@.state() is Locking,
@@ -514,7 +516,6 @@ fn dfs_acquire_lock(
514516
decreases cur_node.deref().deref().level_spec(),
515517
{
516518
broadcast use crate::spec::utils::group_node_helper_lemmas;
517-
518519
// let tracked mut forgot_guards = forgot_guards.get();
519520

520521
let cur_level = cur_node.deref().deref().level();

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

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -39,10 +39,7 @@ use crate::{
3939
},
4040
task::DisabledPreemptGuard,
4141
sync::rcu::RcuDrop,
42-
spec::{
43-
sub_pt::level_is_in_range,
44-
rcu::*,
45-
},
42+
spec::{sub_pt::level_is_in_range, rcu::*},
4643
};
4744

4845
use super::{
@@ -154,14 +151,14 @@ impl<'a, C: PageTableConfig> Cursor<'a, C> {
154151
// }
155152
// &&& self.inst@.cpu_num() == GLOBAL_CPU_NUM
156153
// }
157-
158154
/// Well-formedness of the cursor.
159155
pub open spec fn wf(&self, spt: &SubPageTable<C>) -> bool {
160156
&&& spt.wf()
161157
&&& self.va_wf()
162158
&&& self.level_wf(spt)
163159
&&& self.path_wf(spt)
164160
// &&& self.wf_temp()
161+
165162
}
166163

167164
/// Well-formedness of the cursor's virtual address.
@@ -298,10 +295,8 @@ impl<'a, C: PageTableConfig> Cursor<'a, C> {
298295
// }
299296
// // TODO
300297
// // const { assert!(C::NR_LEVELS() as usize <= MAX_NR_LEVELS) };
301-
302298
// Ok(locking::lock_range(pt, va))
303299
// }
304-
305300
/// Queries the mapping at the current virtual address.
306301
///
307302
/// If the cursor is pointing to a valid virtual address that is locked,
@@ -664,7 +659,6 @@ impl<'a, C: PageTableConfig> CursorMut<'a, C> {
664659
// pub(super) fn new(pt: &'a PageTable<C>, va: &Range<Vaddr>) -> Result<Self, PageTableError> {
665660
// Cursor::new(pt, va).map(|inner| Self(inner))
666661
// }
667-
668662
/// Gets the current virtual address.
669663
pub fn virt_addr(&self) -> Vaddr {
670664
self.0.virt_addr()

‎lock-protocol/src/mm/page_table/node_concurrent/spinlock/guard_forget.rs‎

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,16 +12,15 @@ pub tracked struct SubTreeForgotGuard<C: PageTableConfig> {
1212

1313
impl<C: PageTableConfig> SubTreeForgotGuard<C> {
1414
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-
}
15+
&&& forall|nid: NodeId|
16+
self.guards.dom().contains(nid) ==> {
17+
&&& NodeHelper::valid_nid(nid)
18+
&&& self.guards[nid].relate_nid(nid)
19+
}
1920
}
2021

2122
pub open spec fn put_spec(self, nid: NodeId, guard: SpinGuardGhostInner<C>) -> Self {
22-
Self {
23-
guards: self.guards.insert(nid, guard)
24-
}
23+
Self { guards: self.guards.insert(nid, guard) }
2524
}
2625

2726
pub proof fn tracked_put(tracked &mut self, nid: NodeId, tracked guard: SpinGuardGhostInner<C>)
@@ -38,12 +37,11 @@ impl<C: PageTableConfig> SubTreeForgotGuard<C> {
3837
}
3938

4039
pub open spec fn take_spec(self, nid: NodeId) -> Self {
41-
Self {
42-
guards: self.guards.remove(nid)
43-
}
40+
Self { guards: self.guards.remove(nid) }
4441
}
4542

46-
pub proof fn tracked_take(tracked &mut self, nid: NodeId) -> (tracked guard: SpinGuardGhostInner<C>)
43+
pub proof fn tracked_take(tracked &mut self, nid: NodeId) -> (tracked guard:
44+
SpinGuardGhostInner<C>)
4745
requires
4846
old(self).wf(),
4947
self.guards.dom().contains(nid),
@@ -57,4 +55,4 @@ impl<C: PageTableConfig> SubTreeForgotGuard<C> {
5755
}
5856
}
5957

60-
}
58+
} // verus!

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

Lines changed: 32 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,8 @@ impl<C: PageTableConfig> PageTableEntryPerms<C> {
128128
forall|i: int|
129129
#![trigger self.inner.value()[i]]
130130
0 <= i < 512 ==> {
131-
self.inner.value()[i].nid@ is Some ==>
132-
self.inner.value()[i].nid@->Some_0 == NodeHelper::get_child(nid, i as nat)
131+
self.inner.value()[i].nid@ is Some ==> self.inner.value()[i].nid@->Some_0
132+
== NodeHelper::get_child(nid, i as nat)
133133
}
134134
}
135135

@@ -548,14 +548,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
548548
}
549549
}
550550
let guard = SpinGuard {
551-
inner: Tracked(SpinGuardGhostInner {
552-
handle: handle,
553-
node_token: node_token,
554-
pte_token: pte_token,
555-
stray_perm: stray_perm,
556-
perms: perms,
557-
in_protocol: false,
558-
}),
551+
inner: Tracked(
552+
SpinGuardGhostInner {
553+
handle: handle,
554+
node_token: node_token,
555+
pte_token: pte_token,
556+
stray_perm: stray_perm,
557+
perms: perms,
558+
in_protocol: false,
559+
},
560+
),
559561
};
560562
assert(guard.wf(self));
561563
guard_opt = Some(guard);
@@ -662,14 +664,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
662664
node_token = self.pt_inst.borrow().normal_lock(self.nid@, node_token);
663665
}
664666
let guard = SpinGuard {
665-
inner: Tracked(SpinGuardGhostInner {
666-
handle: handle,
667-
node_token: Some(node_token),
668-
pte_token: Some(pte_token),
669-
stray_perm: stray_perm,
670-
perms: perms,
671-
in_protocol: false,
672-
})
667+
inner: Tracked(
668+
SpinGuardGhostInner {
669+
handle: handle,
670+
node_token: Some(node_token),
671+
pte_token: Some(pte_token),
672+
stray_perm: stray_perm,
673+
perms: perms,
674+
in_protocol: false,
675+
},
676+
),
673677
};
674678
assert(guard.wf(self));
675679
guard_opt = Some(guard);
@@ -840,14 +844,16 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
840844
m.token = res.1.get();
841845
}
842846
let guard = SpinGuard {
843-
inner: Tracked(SpinGuardGhostInner {
844-
handle: handle,
845-
node_token: Some(node_token),
846-
pte_token: Some(pte_token),
847-
stray_perm: stray_perm,
848-
perms: perms,
849-
in_protocol: true,
850-
}),
847+
inner: Tracked(
848+
SpinGuardGhostInner {
849+
handle: handle,
850+
node_token: Some(node_token),
851+
pte_token: Some(pte_token),
852+
stray_perm: stray_perm,
853+
perms: perms,
854+
in_protocol: true,
855+
},
856+
),
851857
};
852858
assert(guard.wf(self));
853859
guard_opt = Some(guard);

0 commit comments

Comments
 (0)