vstd/
rwlock.rs

Help
1#![allow(non_snake_case)]
2#![allow(unused_imports)]
3#![allow(non_shorthand_field_patterns)]
4
5use super::atomic_ghost::*;
6use super::cell::{CellId, PCell, PointsTo};
7use super::invariant::InvariantPredicate;
8use super::modes::*;
9use super::multiset::*;
10use super::prelude::*;
11use super::set::*;
12use core::marker::PhantomData;
13use state_machines_macros::tokenized_state_machine_vstd;
14
15tokenized_state_machine_vstd!(
16RwLockToks<K, V, Pred: InvariantPredicate<K, V>> {
17    fields {
18        #[sharding(constant)]
19        pub k: K,
20
21        #[sharding(constant)]
22        pub pred: PhantomData<Pred>,
23
24        #[sharding(variable)]
25        pub flag_exc: bool,
26
27        #[sharding(variable)]
28        pub flag_rc: nat,
29
30        #[sharding(storage_option)]
31        pub storage: Option<V>,
32
33        #[sharding(option)]
34        pub pending_writer: Option<()>,
35
36        #[sharding(option)]
37        pub writer: Option<()>,
38
39        #[sharding(multiset)]
40        pub pending_reader: Multiset<()>,
41
42        #[sharding(multiset)]
43        pub reader: Multiset<V>,
44    }
45
46    init!{
47        initialize_full(k: K, t: V) {
48            require Pred::inv(k, t);
49            init k = k;
50            init pred = PhantomData;
51            init flag_exc = false;
52            init flag_rc = 0;
53            init storage = Option::Some(t);
54            init pending_writer = Option::None;
55            init writer = Option::None;
56            init pending_reader = Multiset::empty();
57            init reader = Multiset::empty();
58        }
59    }
60
61    #[inductive(initialize_full)]
62    fn initialize_full_inductive(post: Self, k: K, t: V) {
63        broadcast use group_multiset_axioms;
64    }
65
66    /// Increment the 'rc' counter, obtain a pending_reader
67    transition!{
68        acquire_read_start() {
69            update flag_rc = pre.flag_rc + 1;
70            add pending_reader += {()};
71        }
72    }
73
74    /// Exchange the pending_reader for a reader by checking
75    /// that the 'exc' bit is 0
76    transition!{
77        acquire_read_end() {
78            require(pre.flag_exc == false);
79
80            remove pending_reader -= {()};
81
82            birds_eye let x: V = pre.storage->0;
83            add reader += {x};
84
85            assert Pred::inv(pre.k, x);
86        }
87    }
88
89    /// Decrement the 'rc' counter, abandon the attempt to gain
90    /// the 'read' lock.
91    transition!{
92        acquire_read_abandon() {
93            remove pending_reader -= {()};
94            assert(pre.flag_rc >= 1);
95            update flag_rc = (pre.flag_rc - 1) as nat;
96        }
97    }
98
99    /// Atomically set 'exc' bit from 'false' to 'true'
100    /// Obtain a pending_writer
101    transition!{
102        acquire_exc_start() {
103            require(pre.flag_exc == false);
104            update flag_exc = true;
105            add pending_writer += Some(());
106        }
107    }
108
109    /// Finish obtaining the write lock by checking that 'rc' is 0.
110    /// Exchange the pending_writer for a writer and withdraw the
111    /// stored object.
112    transition!{
113        acquire_exc_end() {
114            require(pre.flag_rc == 0);
115
116            remove pending_writer -= Some(());
117
118            add writer += Some(());
119
120            birds_eye let x = pre.storage->0;
121            withdraw storage -= Some(x);
122
123            assert Pred::inv(pre.k, x);
124        }
125    }
126
127    /// Release the write-lock. Update the 'exc' bit back to 'false'.
128    /// Return the 'writer' and also deposit an object back into storage.
129    transition!{
130        release_exc(x: V) {
131            require Pred::inv(pre.k, x);
132            remove writer -= Some(());
133
134            update flag_exc = false;
135
136            deposit storage += Some(x);
137        }
138    }
139
140    /// Check that the 'reader' is actually a guard for the given object.
141    property!{
142        read_guard(x: V) {
143            have reader >= {x};
144            guard storage >= Some(x);
145        }
146    }
147
148    property!{
149        read_match(x: V, y: V) {
150            have reader >= {x};
151            have reader >= {y};
152            assert(equal(x, y));
153        }
154    }
155
156    /// Release the reader-lock. Decrement 'rc' and return the 'reader' object.
157    #[transition]
158    transition!{
159        release_shared(x: V) {
160            remove reader -= {x};
161
162            assert(pre.flag_rc >= 1) by {
163                //assert(pre.reader.count(x) >= 1);
164                assert(equal(pre.storage, Option::Some(x)));
165                //assert(equal(x, pre.storage->0));
166            };
167            update flag_rc = (pre.flag_rc - 1) as nat;
168        }
169    }
170
171    #[invariant]
172    pub fn exc_bit_matches(&self) -> bool {
173        (if self.flag_exc { 1 } else { 0 as int }) ==
174            (if self.pending_writer is Some { 1 } else { 0 as int }) as int
175            + (if self.writer is Some { 1 } else { 0 as int }) as int
176    }
177
178    #[invariant]
179    pub fn count_matches(&self) -> bool {
180        self.flag_rc == self.pending_reader.count(())
181            + self.reader.count(self.storage->0)
182    }
183
184    #[invariant]
185    pub fn reader_agrees_storage(&self) -> bool {
186        forall |t: V| imply(#[trigger] self.reader.count(t) > 0,
187            equal(self.storage, Option::Some(t)))
188    }
189
190    #[invariant]
191    pub fn writer_agrees_storage(&self) -> bool {
192        imply(self.writer is Some, self.storage is None)
193    }
194
195    #[invariant]
196    pub fn writer_agrees_storage_rev(&self) -> bool {
197        imply(self.storage is None, self.writer is Some)
198    }
199
200    #[invariant]
201    pub fn sto_user_inv(&self) -> bool {
202        self.storage.is_some() ==> Pred::inv(self.k, self.storage.unwrap())
203    }
204
205    #[inductive(acquire_read_start)]
206    fn acquire_read_start_inductive(pre: Self, post: Self) {
207        broadcast use group_multiset_axioms;
208    }
209
210    #[inductive(acquire_read_end)]
211    fn acquire_read_end_inductive(pre: Self, post: Self) {
212        broadcast use group_multiset_axioms;
213    }
214
215    #[inductive(acquire_read_abandon)]
216    fn acquire_read_abandon_inductive(pre: Self, post: Self) {
217        broadcast use group_multiset_axioms;
218    }
219
220    #[inductive(acquire_exc_start)]
221    fn acquire_exc_start_inductive(pre: Self, post: Self) { }
222
223    #[inductive(acquire_exc_end)]
224    fn acquire_exc_end_inductive(pre: Self, post: Self) { }
225
226    #[inductive(release_exc)]
227    fn release_exc_inductive(pre: Self, post: Self, x: V) { }
228
229    #[inductive(release_shared)]
230    fn release_shared_inductive(pre: Self, post: Self, x: V) {
231        broadcast use group_multiset_axioms;
232        assert(equal(pre.storage, Option::Some(x)));
233    }
234});
235
236verus! {
237
238pub trait RwLockPredicate<V>: Sized {
239    spec fn inv(self, v: V) -> bool;
240}
241
242impl<V> RwLockPredicate<V> for spec_fn(V) -> bool {
243    open spec fn inv(self, v: V) -> bool {
244        self(v)
245    }
246}
247
248ghost struct InternalPred<V, Pred> {
249    v: V,
250    pred: Pred,
251}
252
253impl<V, Pred: RwLockPredicate<V>> InvariantPredicate<(Pred, CellId), PointsTo<V>> for InternalPred<
254    V,
255    Pred,
256> {
257    closed spec fn inv(k: (Pred, CellId), v: PointsTo<V>) -> bool {
258        v.id() == k.1 && v.is_init() && k.0.inv(v.value())
259    }
260}
261
262struct_with_invariants_vstd!{
263    /** A verified implementation of a reader-writer lock,
264    implemented using atomics and a reference count.
265
266    When constructed, you can provide an invariant via the `Pred` parameter,
267    specifying the allowed values that can go in the lock.
268
269    Note that this specification does *not* verify the absence of dead-locks.
270
271    ### Examples
272
273    On construction of a lock, we can specify an invariant for the object that goes inside.
274    One way to do this is by providing a `spec_fn`, which implements the [`RwLockPredicate`]
275    trait.
276
277    ```rust,ignore
278    fn example1() {
279        // We can create a lock with an invariant: `v == 5 || v == 13`.
280        // Thus only 5 or 13 can be stored in the lock.
281        let lock = RwLock::<u64, spec_fn(u64) -> bool>::new(5, Ghost(|v| v == 5 || v == 13));
282
283        let (val, write_handle) = lock.acquire_write();
284        assert(val == 5 || val == 13);
285        write_handle.release_write(13);
286
287        let read_handle1 = lock.acquire_read();
288        let read_handle2 = lock.acquire_read();
289
290        // We can take multiple read handles at the same time:
291
292        let val1 = read_handle1.borrow();
293        let val2 = read_handle2.borrow();
294
295        // RwLock has a lemma that both read handles have the same value:
296
297        proof { ReadHandle::lemma_readers_match(&read_handle1, &read_handle2); }
298        assert(*val1 == *val2);
299
300        read_handle1.release_read();
301        read_handle2.release_read();
302    }
303    ```
304
305    It's often easier to implement the [`RwLockPredicate`] trait yourself. This way you can
306    have a configurable predicate without needing to work with higher-order functions.
307
308    ```rust,ignore
309    struct FixedParity {
310        pub parity: int,
311    }
312
313    impl RwLockPredicate<u64> for FixedParity {
314        open spec fn inv(self, v: u64) -> bool {
315            v % 2 == self.parity
316        }
317    }
318
319    fn example2() {
320        // Create a lock that can only store even integers
321        let lock_even = RwLock::<u64, FixedParity>::new(20, Ghost(FixedParity { parity: 0 }));
322
323        // Create a lock that can only store odd integers
324        let lock_odd = RwLock::<u64, FixedParity>::new(23, Ghost(FixedParity { parity: 1 }));
325
326        let read_handle_even = lock_even.acquire_read();
327        let val_even = *read_handle_even.borrow();
328        assert(val_even % 2 == 0);
329
330        let read_handle_odd = lock_odd.acquire_read();
331        let val_odd = *read_handle_odd.borrow();
332        assert(val_odd % 2 == 1);
333    }
334    ```
335    */
336
337    pub struct RwLock<V, Pred: RwLockPredicate<V>> {
338        cell: PCell<V>,
339        exc: AtomicBool<_, RwLockToks::flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, _>,
340        rc: AtomicUsize<_, RwLockToks::flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, _>,
341
342        inst: Tracked<RwLockToks::Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
343        pred: Ghost<Pred>,
344    }
345
346    #[verifier::type_invariant]
347    spec fn wf(&self) -> bool {
348        invariant on exc with (inst) is (v: bool, g: RwLockToks::flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
349            g.instance_id() == inst@.id()
350                && g.value() == v
351        }
352
353        invariant on rc with (inst) is (v: usize, g: RwLockToks::flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
354            g.instance_id() == inst@.id()
355                && g.value() == v
356        }
357
358        predicate {
359            self.inst@.k() == (self.pred@, self.cell.id())
360        }
361    }
362}
363
364/// Handle obtained for an exclusive write-lock from an [`RwLock`].
365///
366/// Note that this handle does not contain a reference to the lock-protected object;
367/// ownership of the object is obtained separately from [`RwLock::acquire_write`].
368/// This may be changed in the future.
369///
370/// **Warning:** The lock is _NOT_ released automatically when the handle
371/// is dropped. You must call [`release_write`](WriteHandle::release_write).
372/// Verus does not check that lock is released.
373pub struct WriteHandle<'a, V, Pred: RwLockPredicate<V>> {
374    handle: Tracked<RwLockToks::writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
375    perm: Tracked<PointsTo<V>>,
376    rwlock: &'a RwLock<V, Pred>,
377}
378
379/// Handle obtained for a shared read-lock from an [`RwLock`].
380///
381/// **Warning:** The lock is _NOT_ released automatically when the handle
382/// is dropped. You must call [`release_read`](ReadHandle::release_read).
383/// Verus does not check that lock is released.
384pub struct ReadHandle<'a, V, Pred: RwLockPredicate<V>> {
385    handle: Tracked<RwLockToks::reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
386    rwlock: &'a RwLock<V, Pred>,
387}
388
389impl<'a, V, Pred: RwLockPredicate<V>> WriteHandle<'a, V, Pred> {
390    #[verifier::type_invariant]
391    spec fn wf_write_handle(self) -> bool {
392        equal(self.perm@.id(), self.rwlock.cell.id()) && self.perm@.is_uninit() && equal(
393            self.handle@.instance_id(),
394            self.rwlock.inst@.id(),
395        ) && self.rwlock.wf()
396    }
397
398    pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
399        *self.rwlock
400    }
401
402    pub fn release_write(self, new_val: V)
403        requires
404            self.rwlock().inv(new_val),
405    {
406        proof {
407            use_type_invariant(&self);
408        }
409        let WriteHandle { handle: Tracked(handle), perm: Tracked(mut perm), rwlock } = self;
410        self.rwlock.cell.put(Tracked(&mut perm), new_val);
411
412        atomic_with_ghost!(
413            &rwlock.exc => store(false);
414            ghost g =>
415        {
416            self.rwlock.inst.borrow().release_exc(perm, &mut g, perm, handle);
417        });
418    }
419}
420
421impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
422    #[verifier::type_invariant]
423    spec fn wf_read_handle(self) -> bool {
424        equal(self.handle@.instance_id(), self.rwlock.inst@.id())
425            && self.handle@.element().is_init() && equal(
426            self.handle@.element().id(),
427            self.rwlock.cell.id(),
428        ) && self.rwlock.wf()
429    }
430
431    pub closed spec fn view(self) -> V {
432        self.handle@.element().value()
433    }
434
435    pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
436        *self.rwlock
437    }
438
439    /// Obtain a shared reference to the object contained in the lock.
440    pub fn borrow<'b>(&'b self) -> (val: &'b V)
441        ensures
442            val == self.view(),
443    {
444        proof {
445            use_type_invariant(self);
446        }
447        let tracked perm = self.rwlock.inst.borrow().read_guard(
448            self.handle@.element(),
449            self.handle.borrow(),
450        );
451        self.rwlock.cell.borrow(Tracked(&perm))
452    }
453
454    pub proof fn lemma_readers_match(
455        tracked read_handle1: &ReadHandle<V, Pred>,
456        tracked read_handle2: &ReadHandle<V, Pred>,
457    )
458        requires
459            read_handle1.rwlock() == read_handle2.rwlock(),
460        ensures
461            (equal(read_handle1.view(), read_handle2.view())),
462    {
463        use_type_invariant(read_handle1);
464        use_type_invariant(read_handle2);
465        read_handle1.rwlock.inst.borrow().read_match(
466            read_handle1.handle@.element(),
467            read_handle2.handle@.element(),
468            &read_handle1.handle.borrow(),
469            &read_handle2.handle.borrow(),
470        );
471    }
472
473    pub fn release_read(self) {
474        proof {
475            use_type_invariant(&self);
476        }
477        let ReadHandle { handle: Tracked(handle), rwlock } = self;
478
479        let _ =
480            atomic_with_ghost!(
481            &rwlock.rc => fetch_sub(1);
482            ghost g =>
483        {
484            rwlock.inst.borrow().release_shared(handle.element(), &mut g, handle);
485        });
486    }
487}
488
489impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred> {
490    /// Predicate configured for this lock instance.
491    pub closed spec fn pred(&self) -> Pred {
492        self.pred@
493    }
494
495    /// Indicates if the value `v` can be stored in the lock. Per the definition,
496    /// it depends on `[self.pred()]`, which is configured upon lock construction ([`RwLock::new`]).
497    pub open spec fn inv(&self, val: V) -> bool {
498        self.pred().inv(val)
499    }
500
501    pub fn new(val: V, Ghost(pred): Ghost<Pred>) -> (s: Self)
502        requires
503            pred.inv(val),
504        ensures
505            s.pred() == pred,
506    {
507        let (cell, Tracked(perm)) = PCell::<V>::new(val);
508
509        let tracked (Tracked(inst), Tracked(flag_exc), Tracked(flag_rc), _, _, _, _) =
510            RwLockToks::Instance::<
511            (Pred, CellId),
512            PointsTo<V>,
513            InternalPred<V, Pred>,
514        >::initialize_full((pred, cell.id()), perm, Option::Some(perm));
515        let inst = Tracked(inst);
516
517        let exc = AtomicBool::new(Ghost(inst), false, Tracked(flag_exc));
518        let rc = AtomicUsize::new(Ghost(inst), 0, Tracked(flag_rc));
519
520        RwLock { cell, exc, rc, inst, pred: Ghost(pred) }
521    }
522
523    /// Acquires an exclusive write-lock. To release it, use [`WriteHandle::release_write`].
524    ///
525    /// **Warning:** The lock is _NOT_ released automatically when the handle
526    /// is dropped. You must call [`WriteHandle::release_write`].
527    /// Verus does not check that lock is released.
528    #[verifier::exec_allows_no_decreases_clause]
529    pub fn acquire_write(&self) -> (ret: (V, WriteHandle<V, Pred>))
530        ensures
531            ({
532                let val = ret.0;
533                let write_handle = ret.1;
534                &&& write_handle.rwlock() == *self
535                &&& self.inv(val)
536            }),
537    {
538        proof {
539            use_type_invariant(self);
540        }
541        let mut done = false;
542        let tracked mut token: Option<
543            RwLockToks::pending_writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
544        > = Option::None;
545        while !done
546            invariant
547                done ==> token.is_some() && equal(token->0.instance_id(), self.inst@.id()),
548                self.wf(),
549        {
550            let result =
551                atomic_with_ghost!(
552                &self.exc => compare_exchange(false, true);
553                returning res;
554                ghost g =>
555            {
556                if res is Ok {
557                    token = Option::Some(self.inst.borrow().acquire_exc_start(&mut g));
558                }
559            });
560
561            done =
562            match result {
563                Result::Ok(_) => true,
564                _ => false,
565            };
566        }
567        loop
568            invariant
569                token is Some && equal(token->0.instance_id(), self.inst@.id()),
570                self.wf(),
571        {
572            let tracked mut perm_opt: Option<PointsTo<V>> = None;
573            let tracked mut handle_opt: Option<
574                RwLockToks::writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
575            > = None;
576
577            let result =
578                atomic_with_ghost!(
579                &self.rc => load();
580                returning res;
581                ghost g =>
582            {
583                if res == 0 {
584                    let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
585                    let tracked x = self.inst.borrow().acquire_exc_end(&g, tok);
586                    token = None;
587                    let tracked (_, Tracked(perm), Tracked(exc_handle)) = x;
588                    perm_opt = Some(perm);
589                    handle_opt = Some(exc_handle);
590                }
591            });
592
593            if result == 0 {
594                let tracked mut perm = match perm_opt {
595                    Option::Some(t) => t,
596                    Option::None => proof_from_false(),
597                };
598                let tracked handle = match handle_opt {
599                    Option::Some(t) => t,
600                    Option::None => proof_from_false(),
601                };
602                let t = self.cell.take(Tracked(&mut perm));
603                let write_handle = WriteHandle {
604                    perm: Tracked(perm),
605                    handle: Tracked(handle),
606                    rwlock: self,
607                };
608                return (t, write_handle);
609            }
610        }
611    }
612
613    /// Acquires a shared read-lock. To release it, use [`ReadHandle::release_read`].
614    ///
615    /// **Warning:** The lock is _NOT_ released automatically when the handle
616    /// is dropped. You must call [`ReadHandle::release_read`].
617    /// Verus does not check that lock is released.
618    #[verifier::exec_allows_no_decreases_clause]
619    pub fn acquire_read(&self) -> (read_handle: ReadHandle<V, Pred>)
620        ensures
621            read_handle.rwlock() == *self,
622            self.inv(read_handle.view()),
623    {
624        proof {
625            use_type_invariant(self);
626        }
627        loop
628            invariant
629                self.wf(),
630        {
631            let val = atomic_with_ghost!(&self.rc => load(); ghost g => { });
632
633            let tracked mut token: Option<
634                RwLockToks::pending_reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
635            > = Option::None;
636
637            if val < usize::MAX {
638                let result =
639                    atomic_with_ghost!(
640                    &self.rc => compare_exchange(val, val + 1);
641                    returning res;
642                    ghost g =>
643                {
644                    if res is Ok {
645                        token = Option::Some(self.inst.borrow().acquire_read_start(&mut g));
646                    }
647                });
648
649                match result {
650                    Result::Ok(_) => {
651                        let tracked mut handle_opt: Option<
652                            RwLockToks::reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
653                        > = None;
654
655                        let result =
656                            atomic_with_ghost!(
657                            &self.exc => load();
658                            returning res;
659                            ghost g =>
660                        {
661                            if res == false {
662                                let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
663                                let tracked x = self.inst.borrow().acquire_read_end(&g, tok);
664                                token = None;
665                                let tracked (_, Tracked(exc_handle)) = x;
666                                handle_opt = Some(exc_handle);
667                            }
668                        });
669
670                        if result == false {
671                            let tracked handle = match handle_opt {
672                                Option::Some(t) => t,
673                                Option::None => proof_from_false(),
674                            };
675                            let read_handle = ReadHandle { handle: Tracked(handle), rwlock: self };
676                            return read_handle;
677                        } else {
678                            let _ =
679                                atomic_with_ghost!(
680                                &self.rc => fetch_sub(1);
681                                ghost g =>
682                            {
683                                let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
684                                self.inst.borrow().acquire_read_abandon(&mut g, tok);
685                            });
686                        }
687                    },
688                    _ => {},
689                }
690            }
691        }
692    }
693
694    /// Destroys the lock and returns the inner object.
695    /// Note that this may deadlock if not all locks have been released.
696    #[verifier::exec_allows_no_decreases_clause]
697    pub fn into_inner(self) -> (v: V)
698        ensures
699            self.inv(v),
700    {
701        let (v, _write_handle) = self.acquire_write();
702        v
703    }
704}
705
706} // verus!
vstd/rwlock.rs

vstd/
rwlock.rs
