There was a problem fetching the pipeline mini graph.
Proove that RWlock is safe.
FIXME : we need to be able to end a lifetime when an invariant is still open.
Showing
- _CoqProject 6 additions, 0 deletions_CoqProject
- theories/typing/unsafe/rwlock/rwlock.v 194 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlock.v
- theories/typing/unsafe/rwlock/rwlock_code.v 313 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlock_code.v
- theories/typing/unsafe/rwlock/rwlockreadguard.v 112 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlockreadguard.v
- theories/typing/unsafe/rwlock/rwlockreadguard_code.v 148 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlockreadguard_code.v
- theories/typing/unsafe/rwlock/rwlockwriteguard.v 129 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlockwriteguard.v
- theories/typing/unsafe/rwlock/rwlockwriteguard_code.v 146 additions, 0 deletionstheories/typing/unsafe/rwlock/rwlockwriteguard_code.v
Loading
Please register or sign in to comment