Skip to content

Commit bb6b6ac

Browse files
rikosellicrikosellic
committed
Simplify
1 parent 2c7d18c commit bb6b6ac

2 files changed

Lines changed: 45 additions & 133 deletions

File tree

‎ostd/src/sync/rwlock.rs‎

Lines changed: 17 additions & 122 deletions
Original file line numberDiff line numberDiff line change
@@ -232,12 +232,6 @@ closed spec fn wf(self) -> bool {
232232
&&& has_upgrade_bit <==> (active_upgrade_guard || pending_failed_upread_attempt)
233233
// An active `RwLockUpgradeableGuard` cannot coexist with a pending failed `try_upread` attempt.
234234
&&& !(active_upgrade_guard && pending_failed_upread_attempt)
235-
// Make the two exclusive-token storages line up explicitly with the atomic bits.
236-
&&& g.upreader_guard_token.is_empty() ==> has_upgrade_bit
237-
&&& !has_upgrade_bit ==> g.upreader_guard_token.is_full()
238-
&&& !has_upgrade_bit ==> !pending_failed_upread_attempt
239-
&&& pending_failed_upread_attempt ==> has_upgrade_bit
240-
&&& pending_failed_upread_attempt ==> g.upreader_guard_token.is_full()
241235
// The `READER` bits count the number of all active readers and pending failed `try_read` attempts.
242236
&&& total_reader_bits + if active_upgrade_guard { 1int } else {0} == total_active_readers + failed_reader_attempts
243237
// There is an active `RwLockWriteGuard` iff the `WRITER` bit is set.
@@ -247,15 +241,13 @@ closed spec fn wf(self) -> bool {
247241
// The core invariant of `RwLock`: there are no simultaneous active writers and readers.
248242
&&& !(active_writer && total_active_readers > 0)
249243
&&& 0 <= g.read_retract_token.frac() <= V_MAX_READ_RETRACT_FRACS
250-
&&& g.upread_retract_token.is_empty() || g.upread_retract_token.is_full()
251-
&&& g.upreader_guard_token.is_empty() || g.upreader_guard_token.is_full()
244+
&&& g.upread_retract_token.wf()
245+
&&& g.upreader_guard_token.wf()
252246
&&& match g.cell_perm {
253247
Sum::Right(empty) => {
254-
&&& has_writer_bit
255248
&&& empty.id() == v_id@.cell_perm_id
256249
}
257250
Sum::Left(perm) => {
258-
&&& !has_writer_bit
259251
&&& perm.id() == v_id@.cell_perm_id
260252
&&& perm.resource().id() == val.id()
261253
}
@@ -329,20 +321,17 @@ impl<T, G> RwLock<T, G> {
329321
// Proof code
330322
proof {lemma_consts_properties();}
331323
let tracked frac_perm = RwFrac::<T>::new(perm);
332-
let tracked read_retract_token = TokenStorage::<V_MAX_READ_RETRACT_FRACS>::new(());
333-
let tracked upread_retract_token = UniqueTokenStorage::alloc(());
334-
let tracked upreader_guard_token = UniqueTokenStorage::alloc(());
335-
324+
proof_decl!{
325+
let tracked read_retract_token = TokenStorage::<V_MAX_READ_RETRACT_FRACS>::new(());
326+
let tracked upread_retract_token = UniqueTokenStorage::alloc(());
327+
let tracked upreader_guard_token = UniqueTokenStorage::alloc(());
328+
}
336329
let ghost v_id = RwId {
337330
cell_perm_id: frac_perm.id(),
338331
upread_retract_token_id: upread_retract_token.id(),
339332
upreader_guard_token_id: upreader_guard_token.id(),
340333
read_retract_token_id: read_retract_token.id(),
341334
};
342-
proof {
343-
upread_retract_token.validate();
344-
upreader_guard_token.validate();
345-
};
346335
let tracked perms = RwPerms {
347336
cell_perm: Sum::new_left(frac_perm),
348337
read_retract_token,
@@ -569,14 +558,7 @@ impl<T /*: ?Sized*/ , G: SpinGuardian> RwLock<T, G> {
569558
let next_usize = next as usize;
570559
lemma_consts_properties_value(prev_usize);
571560
lemma_consts_properties_prev_next(prev_usize, next_usize);
572-
let tracked token = retract_upgrade_token.tracked_unwrap();
573-
if g.upread_retract_token.is_full() {
574-
g.upread_retract_token.is_exclusive(&token);
575-
assert(false);
576-
} else {
577-
g.upread_retract_token.join(token);
578-
g.upread_retract_token.validate();
579-
}
561+
g.upread_retract_token.join(retract_upgrade_token.tracked_unwrap());
580562
}
581563
);
582564
}
@@ -949,82 +931,14 @@ impl<'a, T /*: ?Sized*/, G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G>
949931
ghost g => {
950932
lemma_consts_properties_prev_next(prev, next);
951933
if res is Ok {
952-
assert(prev == UPGRADEABLE_READER | BEING_UPGRADED);
953-
assert(next == WRITER | UPGRADEABLE_READER);
954-
assert((prev & WRITER) == 0) by (bit_vector)
955-
requires
956-
prev == UPGRADEABLE_READER | BEING_UPGRADED,
957-
;
958-
assert((prev & READER_MASK) == 0) by (bit_vector)
959-
requires
960-
prev == UPGRADEABLE_READER | BEING_UPGRADED,
961-
;
962-
assert((prev & MAX_READER_MASK) == 0) by (bit_vector)
963-
requires
964-
prev == UPGRADEABLE_READER | BEING_UPGRADED,
965-
;
966-
assert((prev & MAX_READER) == 0) by (bit_vector)
967-
requires
968-
prev == UPGRADEABLE_READER | BEING_UPGRADED,
969-
;
970-
if g.upreader_guard_token.is_full() {
971-
let tracked token = guard_token.tracked_unwrap();
972-
g.upreader_guard_token.is_exclusive(&token);
973-
assert(false);
974-
} else {
975-
g.upreader_guard_token.validate();
976-
assert(g.upreader_guard_token.is_empty());
977-
g.upreader_guard_token.join(guard_token.tracked_unwrap());
978-
g.upreader_guard_token.validate();
979-
assert(g.upreader_guard_token.is_full());
980-
assert(!g.upreader_guard_token.is_empty());
981-
}
982-
if g.upread_retract_token.is_empty() {
983-
assert(false);
984-
} else {
985-
retract_upgrade_token = Some(g.upread_retract_token.take());
986-
assert(g.upread_retract_token.is_empty());
987-
g.upread_retract_token.validate();
988-
assert(!g.upread_retract_token.is_full());
989-
}
990-
if g.cell_perm is Right {
991-
assert(false);
992-
}
993-
assert(g.cell_perm->Left_0.frac() == (V_MAX_PERM_FRACS as int) - 1int);
934+
g.upreader_guard_token.join(guard_token.tracked_unwrap());
935+
retract_upgrade_token = Some(g.upread_retract_token.take());
994936
let tracked mut rem = g.cell_perm.tracked_take_left();
995937
rem.combine(guard_perm.tracked_unwrap());
996-
assert(rem.frac() == V_MAX_PERM_FRACS as int);
997938
let tracked (full_perm, empty) = rem.take_resource();
998-
assert(full_perm.id() == inner.cell_id());
999-
assert(empty.id() == inner.cell_perm_id());
1000939
write_perm = Some(full_perm);
1001940
g.cell_perm = Sum::new_right(empty);
1002-
assert(g.cell_perm is Right);
1003-
assert(g.upreader_guard_token.is_full());
1004-
assert(!g.upreader_guard_token.is_empty());
1005-
assert(g.upread_retract_token.is_empty());
1006-
assert(!g.upread_retract_token.is_full());
1007-
assert((next & WRITER) != 0) by (bit_vector)
1008-
requires
1009-
next == WRITER | UPGRADEABLE_READER,
1010-
;
1011-
assert((next & UPGRADEABLE_READER) != 0) by (bit_vector)
1012-
requires
1013-
next == WRITER | UPGRADEABLE_READER,
1014-
;
1015-
assert((next & READER_MASK) == 0) by (bit_vector)
1016-
requires
1017-
next == WRITER | UPGRADEABLE_READER,
1018-
;
1019-
assert((next & MAX_READER_MASK) == 0) by (bit_vector)
1020-
requires
1021-
next == WRITER | UPGRADEABLE_READER,
1022-
;
1023-
assert((next & MAX_READER) == 0) by (bit_vector)
1024-
requires
1025-
next == WRITER | UPGRADEABLE_READER,
1026-
;
1027-
assert(g.read_retract_token.frac() == V_MAX_READ_RETRACT_FRACS);
941+
1028942
} else {
1029943
err_guard_perm = guard_perm;
1030944
err_guard_token = guard_token;
@@ -1044,20 +958,7 @@ impl<'a, T /*: ?Sized*/, G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G>
1044958
lemma_consts_properties_prev_next(prev_usize, next_usize);
1045959
let tracked token = retract_upgrade_token.tracked_unwrap();
1046960
let tracked mut perm = write_perm.tracked_unwrap();
1047-
if g.upread_retract_token.is_full() {
1048-
g.upread_retract_token.is_exclusive(&token);
1049-
assert(false);
1050-
} else {
1051-
g.upread_retract_token.validate();
1052-
assert(g.upread_retract_token.is_empty());
1053-
assert((prev_usize & UPGRADEABLE_READER) != 0);
1054-
if g.cell_perm is Left {
1055-
is_exclusive(&mut perm, g.cell_perm.tracked_borrow_left().borrow());
1056-
assert(false);
1057-
}
1058-
g.upread_retract_token.join(token);
1059-
g.upread_retract_token.validate();
1060-
}
961+
g.upread_retract_token.join(token);
1061962
write_perm = Some(perm);
1062963
}
1063964
);
@@ -1125,17 +1026,11 @@ impl<T /*: ?Sized*/, G: SpinGuardian> RwLockUpgradeableGuard<'_, T, G>
11251026
let next_usize = next as usize;
11261027
lemma_consts_properties_value(prev_usize);
11271028
lemma_consts_properties_prev_next(prev_usize, next_usize);
1128-
if g.upreader_guard_token.is_full() {
1129-
g.upreader_guard_token.is_exclusive(&token);
1130-
assert(false);
1131-
} else {
1132-
assert((prev_usize & UPGRADEABLE_READER) != 0);
1133-
let tracked mut rem = g.cell_perm.tracked_take_left();
1134-
rem.combine(perm);
1135-
g.cell_perm = Sum::new_left(rem);
1136-
g.upreader_guard_token.join(token);
1137-
g.upreader_guard_token.validate();
1138-
}
1029+
g.upreader_guard_token.join(token);
1030+
let tracked mut rem = g.cell_perm.tracked_take_left();
1031+
rem.combine(perm);
1032+
g.cell_perm = Sum::new_left(rem);
1033+
11391034
}
11401035
);
11411036
}

‎vstd_extra/src/resource/storage/excl.rs‎

Lines changed: 28 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,6 @@ impl<T> ExclusiveGhostResource<T> {
7575
old(self).is_full(),
7676
ensures
7777
res == *old(self),
78-
res.is_full(),
7978
old(self).id() == self.id(),
8079
self.is_empty(),
8180
{
@@ -91,7 +90,6 @@ impl<T> ExclusiveGhostResource<T> {
9190
old(self).id() == other.id(),
9291
ensures
9392
*self == other,
94-
self.is_full(),
9593
{
9694
let tracked mut other = other;
9795
tracked_swap(&mut self.r, &mut other.r);
@@ -184,10 +182,22 @@ impl<T> ExclusiveGhostStorage<T> {
184182
self.0.is_full()
185183
}
186184

185+
pub open spec fn wf(self) -> bool {
186+
&&& self.is_empty() || self.is_full()
187+
&&& self.is_empty() <==> !self.is_full()
188+
&&& self.is_full() <==> !self.is_empty()
189+
}
190+
191+
#[verifier::type_invariant]
192+
pub open spec fn type_inv(self) -> bool {
193+
self.wf()
194+
}
195+
187196
pub proof fn alloc(value: T) -> (tracked res: Self)
188197
ensures
189198
res.view() == value,
190199
res.is_full(),
200+
res.wf(),
191201
{
192202
Self(ExclusiveGhostResource::alloc(value))
193203
}
@@ -200,6 +210,7 @@ impl<T> ExclusiveGhostStorage<T> {
200210
self.is_empty(),
201211
res.id() == old(self).id(),
202212
res.view() == old(self).view(),
213+
self.wf(),
203214
{
204215
let tracked r = self.0.take();
205216
ExclusiveGhost(r)
@@ -210,29 +221,35 @@ impl<T> ExclusiveGhostStorage<T> {
210221
self.is_full() ==> self.id() != other.id(),
211222
*old(self) == *self,
212223
{
224+
use_type_invariant(&*self);
213225
use_type_invariant(other);
214226
self.0.is_exclusive(&other.0);
215227
}
216228

217229
pub proof fn join(tracked &mut self, tracked other: ExclusiveGhost<T>)
218230
requires
219-
old(self).is_empty(),
220231
old(self).id() == other.id(),
221232
ensures
222-
self.id() == old(self).id(),
223-
self.view() == other.view(),
224-
self.is_full(),
233+
old(self).is_empty() ==> {
234+
&&& self.id() == old(self).id()
235+
&&& self.view() == other.view()
236+
&&& self.is_full()
237+
&&& self.wf()
238+
},
239+
old(self).is_full() ==> false,
225240
{
226241
use_type_invariant(&other);
227-
self.validate();
228-
self.0.join(other.0);
242+
if self.is_full() {
243+
self.0.is_exclusive(&other.0);
244+
} else {
245+
self.validate();
246+
self.0.join(other.0);
247+
}
229248
}
230249

231250
pub proof fn validate(tracked &self)
232251
ensures
233-
self.is_empty() || self.is_full(),
234-
self.is_empty() <==> !self.is_full(),
235-
self.is_full() <==> !self.is_empty(),
252+
self.wf(),
236253
{
237254
self.0.validate();
238255
}

0 commit comments

Comments
 (0)