Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
69 commits
Select commit Hold shift + click to select a range
860e9bb
Add empty RwLock invariant
rikosellic Feb 9, 2026
0416d36
spec: add `wf` in rwlock
Marsman1996 Feb 9, 2026
1ac70ae
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 10, 2026
fa3f006
Merge fix
rikosellic Feb 10, 2026
912a8a8
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 11, 2026
466c701
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 12, 2026
2ada1a5
Try to prove new
rikosellic Feb 12, 2026
553f31a
Prove `RwLock::new`
rikosellic Feb 12, 2026
69f05fb
Add invariant for RwLockReadGuard
rikosellic Feb 12, 2026
a76eba6
Minor
rikosellic Feb 12, 2026
b048a9b
Fix invariant
rikosellic Feb 15, 2026
c05a9df
Rewrite `RwLock::get_mut` and `as_ptr`
Marsman1996 Feb 15, 2026
3069513
add commented original code
Marsman1996 Feb 16, 2026
ffa138b
verifiable: make code compilable for Verus
Marsman1996 Feb 24, 2026
3a51ac8
fix
Marsman1996 Feb 24, 2026
ed35579
format
Marsman1996 Feb 24, 2026
114895c
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 24, 2026
5e7c7c2
Merge branch 'RwLock-invariants' of https://github.com/rikosellic/vos…
rikosellic Feb 24, 2026
9324ad8
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 25, 2026
e6e7f55
Add try_write proof skeleton
rikosellic Feb 25, 2026
2f7f2a4
prove: admit in `RwLock::try_write`
Marsman1996 Feb 25, 2026
49a300e
Simplify try_wrtite proof
rikosellic Feb 25, 2026
a434813
prove: `try_write_arc`
Marsman1996 Feb 25, 2026
99bd09f
prove: `try_upread`
Marsman1996 Feb 25, 2026
ff56c04
Revert "prove: `try_upread`"
rikosellic Feb 25, 2026
de557a0
Add a permission field in UpgradeableGuard
rikosellic Feb 25, 2026
93d2636
prove: `RwLock::try_upread`
Marsman1996 Feb 25, 2026
66e3051
Revert "prove: `RwLock::try_upread`"
rikosellic Feb 25, 2026
a7e53bc
Some progress in try_upread
rikosellic Feb 25, 2026
a2a31f1
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 26, 2026
2c94240
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 26, 2026
d106920
Refine Inv
rikosellic Feb 26, 2026
a9860a5
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 26, 2026
4297c1f
rename
rikosellic Feb 26, 2026
fb0c58b
Prove admit in try_upread
rikosellic Feb 27, 2026
ede8054
Prove some admit in try_upread
rikosellic Feb 27, 2026
8c54446
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 27, 2026
f677acd
Prove try_upread
rikosellic Feb 27, 2026
eec1034
prove: try_upread_arc
Marsman1996 Feb 27, 2026
52a2c24
chore: remove external_body for upper API
Marsman1996 Feb 27, 2026
e237ef6
refine the inv
rikosellic Feb 27, 2026
69437c6
Refine the inv and add some doc
rikosellic Feb 28, 2026
cbf938b
Add bit lemma useful in proving try_read
rikosellic Feb 28, 2026
232936a
Add a helper function
rikosellic Feb 28, 2026
dc5bd04
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Feb 28, 2026
4409b4a
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Mar 2, 2026
fb91711
Merge remote-tracking branch 'upstream/main' into RwLock-invariants
rikosellic Mar 2, 2026
916e69c
Add try_read proof skeleton
rikosellic Mar 3, 2026
37e992d
Inv overhaul
rikosellic Mar 3, 2026
f92ad65
proof progress
rikosellic Mar 3, 2026
9f51a9c
prove: 1 admit in `try_read`
Marsman1996 Mar 3, 2026
06cfa31
prove: try_read
Marsman1996 Mar 3, 2026
1fe8520
Simplify proof
rikosellic Mar 3, 2026
7675180
Minor
rikosellic Mar 3, 2026
f09681f
fmt
Marsman1996 Mar 3, 2026
8695404
prove: try_read_arc
Marsman1996 Mar 3, 2026
450f3e6
Minor doc update
rikosellic Mar 4, 2026
a615a79
verifiable: all functions in rwlock
Marsman1996 Mar 4, 2026
0585000
verifiable: rwlock.rs
Marsman1996 Mar 4, 2026
38d002d
doc: enable doc for rwlock
Marsman1996 Mar 4, 2026
b5f3dba
Simplify proof
rikosellic Mar 4, 2026
0b1c8f7
prove: `try_upgrade` and `upgrade`
Marsman1996 Mar 4, 2026
d760d50
verifiable: add original code as the comment
Marsman1996 Mar 5, 2026
d13de48
Remove legacy `downgrade`
rikosellic Mar 5, 2026
548e038
Migrate to latest RwLock
rikosellic Mar 5, 2026
4724139
Deprecate deref_spec
rikosellic Mar 5, 2026
03c3476
prove: RwLock::new again
Marsman1996 Mar 5, 2026
4e6f58d
Prove deref and simplify
rikosellic Mar 6, 2026
65db0b7
Simplify proof
rikosellic Mar 6, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions ostd/src/sync/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,8 @@ pub use self::{
},
//mutex::{ArcMutexGuard, Mutex, MutexGuard},
rcu::{non_null /*, Rcu, RcuDrop, RcuOption, RcuOptionReadGuard, RcuReadGuard*/},
/*rwarc::{RoArc, RwArc},
rwlock::{
ArcRwLockReadGuard, ArcRwLockUpgradeableGuard, ArcRwLockWriteGuard, RwLock,
RwLockReadGuard, RwLockUpgradeableGuard, RwLockWriteGuard,
},
/*rwarc::{RoArc, RwArc},*/
rwlock::{RwLock, RwLockReadGuard, RwLockUpgradeableGuard, RwLockWriteGuard},/*
rwmutex::{
ArcRwMutexReadGuard, ArcRwMutexUpgradeableGuard, ArcRwMutexWriteGuard, RwMutex,
RwMutexReadGuard, RwMutexUpgradeableGuard, RwMutexWriteGuard,
Expand Down
Loading