vstd/
rwlock.rs

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

vstd/
rwlock.rs
