Skip to content

Finish RwLock#340

Draft
rikosellic wants to merge 34 commits intoasterinas:mainfrom
rikosellic:rwlock-drop
Draft

Finish RwLock#340
rikosellic wants to merge 34 commits intoasterinas:mainfrom
rikosellic:rwlock-drop

Conversation

@rikosellic
Copy link
Collaborator

@rikosellic rikosellic commented Mar 9, 2026

TODO

  • Polish the Inv.
  • RwLockUpgradeableGuard::drop.
  • RwLockWriteGuard::drop.
  • RwLockUpgradeableGuard::try_upgrade without ManuallyDrop.
  • Define an exclusive ghost resource and replace the frac-based UniqueTokenStorage.
  • Define a sum type resource that supports storage and borrowing.
  • Use this resource in the Inv and prove RwLockReadGuard::Drop.

@rikosellic
Copy link
Collaborator Author

Well done. KVerus has done what I have expected. I will futhur impove try_upgrade after I finish verifying drop.

@Marsman1996 Marsman1996 added AI-assist AI-aided proof or generation labels Mar 11, 2026
@rikosellic rikosellic added the exec code Proofs about execution code label Mar 12, 2026
@rikosellic rikosellic changed the title Drop in RwLock Finish RwLock Mar 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

AI-assist AI-aided proof or generation exec code Proofs about execution code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants