1#![allow(unused_imports)]
4
5use super::atomic::*;
6use super::invariant::*;
7use super::modes::*;
8use super::prelude::*;
9
10verus! {
11
12pub trait AtomicInvariantPredicate<K, V, G> {
13 spec fn atomic_inv(k: K, v: V, g: G) -> bool;
14}
15
16} macro_rules! declare_atomic_type {
18 ($at_ident:ident, $patomic_ty:ident, $perm_ty:ty, $value_ty: ty, $atomic_pred_ty: ident) => {
19 verus!{
20
21 pub struct $atomic_pred_ty<Pred> { p: Pred }
22
23 impl<K, G, Pred> InvariantPredicate<(K, int), ($perm_ty, G)> for $atomic_pred_ty<Pred>
24 where Pred: AtomicInvariantPredicate<K, $value_ty, G>
25 {
26 open spec fn inv(k_loc: (K, int), perm_g: ($perm_ty, G)) -> bool {
27 let (k, loc) = k_loc;
28 let (perm, g) = perm_g;
29
30 perm.view().patomic == loc
31 && Pred::atomic_inv(k, perm.view().value, g)
32 }
33 }
34
35 #[doc = concat!(
36 "Sequentially-consistent atomic memory location storing a `",
37 stringify!($value_ty),
38 "` and associated ghost state."
39 )]
40 pub struct $at_ident<K, G, Pred>
44 {
46 #[doc(hidden)]
47 pub patomic: $patomic_ty,
48
49 #[doc(hidden)]
50 pub atomic_inv: Tracked<AtomicInvariant<(K, int), ($perm_ty, G), $atomic_pred_ty<Pred>>>,
51 }
52
53 impl<K, G, Pred> $at_ident<K, G, Pred>
54 where Pred: AtomicInvariantPredicate<K, $value_ty, G>
55 {
56 pub open spec fn well_formed(&self) -> bool {
57 self.atomic_inv@.constant().1 == self.patomic.id()
58 }
59
60 pub open spec fn constant(&self) -> K {
61 self.atomic_inv@.constant().0
62 }
63
64 #[inline(always)]
65 pub const fn new(Ghost(k): Ghost<K>, u: $value_ty, Tracked(g): Tracked<G>) -> (t: Self)
66 requires Pred::atomic_inv(k, u, g),
67 ensures t.well_formed() && t.constant() == k,
68 {
69
70 let (patomic, Tracked(perm)) = $patomic_ty::new(u);
71
72 let tracked pair = (perm, g);
73 assert(Pred::atomic_inv(k, u, g));
74 assert(perm.view().patomic == patomic.id());
75 let tracked atomic_inv = AtomicInvariant::new(
76 (k, patomic.id()), pair, 0);
77
78 $at_ident {
79 patomic,
80 atomic_inv: Tracked(atomic_inv),
81 }
82 }
83
84 #[inline(always)]
85 pub fn load(&self) -> $value_ty
86 requires self.well_formed(),
87 {
88 atomic_with_ghost!(self => load(); g => { })
89 }
90
91 #[inline(always)]
92 pub fn into_inner(self) -> (res: ($value_ty, Tracked<G>))
93 requires self.well_formed(),
94 ensures Pred::atomic_inv(self.constant(), res.0, res.1@),
95 {
96 let Self { patomic, atomic_inv: Tracked(atomic_inv) } = self;
97 let tracked (perm, g) = atomic_inv.into_inner();
98 let v = patomic.into_inner(Tracked(perm));
99 (v, Tracked(g))
100 }
101 }
102
103 }
104 };
105}
106macro_rules! declare_atomic_type_generic {
107 ($at_ident:ident, $patomic_ty:ident, $perm_ty:ty, $value_ty: ty, $atomic_pred_ty: ident) => {
108 verus!{
109
110 pub struct $atomic_pred_ty<T, Pred> { t: T, p: Pred }
111
112 impl<T, K, G, Pred> InvariantPredicate<(K, int), ($perm_ty, G)> for $atomic_pred_ty<T, Pred>
113 where Pred: AtomicInvariantPredicate<K, $value_ty, G>
114 {
115 open spec fn inv(k_loc: (K, int), perm_g: ($perm_ty, G)) -> bool {
116 let (k, loc) = k_loc;
117 let (perm, g) = perm_g;
118
119 perm.view().patomic == loc
120 && Pred::atomic_inv(k, perm.view().value, g)
121 }
122 }
123
124 #[doc = concat!(
125 "Sequentially-consistent atomic memory location storing a `",
126 stringify!($value_ty),
127 "` and associated ghost state."
128 )]
129 pub struct $at_ident<T, K, G, Pred>
133 {
135 #[doc(hidden)]
136 pub patomic: $patomic_ty<T>,
137
138 #[doc(hidden)]
139 pub atomic_inv: Tracked<AtomicInvariant<(K, int), ($perm_ty, G), $atomic_pred_ty<T, Pred>>>,
140 }
141
142 impl<T, K, G, Pred> $at_ident<T, K, G, Pred>
143 where Pred: AtomicInvariantPredicate<K, $value_ty, G>
144 {
145 pub open spec fn well_formed(&self) -> bool {
146 self.atomic_inv@.constant().1 == self.patomic.id()
147 }
148
149 pub open spec fn constant(&self) -> K {
150 self.atomic_inv@.constant().0
151 }
152
153 #[inline(always)]
154 pub const fn new(Ghost(k): Ghost<K>, u: $value_ty, Tracked(g): Tracked<G>) -> (t: Self)
155 requires Pred::atomic_inv(k, u, g),
156 ensures t.well_formed() && t.constant() == k,
157 {
158
159 let (patomic, Tracked(perm)) = $patomic_ty::<T>::new(u);
160
161 let tracked pair = (perm, g);
162 let tracked atomic_inv = AtomicInvariant::new(
163 (k, patomic.id()), pair, 0);
164
165 $at_ident {
166 patomic,
167 atomic_inv: Tracked(atomic_inv),
168 }
169 }
170
171 #[inline(always)]
172 pub fn load(&self) -> $value_ty
173 requires self.well_formed(),
174 {
175 atomic_with_ghost!(self => load(); g => { })
176 }
177
178 #[inline(always)]
179 pub fn into_inner(self) -> (res: ($value_ty, Tracked<G>))
180 requires self.well_formed(),
181 ensures Pred::atomic_inv(self.constant(), res.0, res.1@),
182 {
183 let Self { patomic, atomic_inv: Tracked(atomic_inv) } = self;
184 let tracked (perm, g) = atomic_inv.into_inner();
185 let v = patomic.into_inner(Tracked(perm));
186 (v, Tracked(g))
187 }
188 }
189
190 }
191 };
192}
193
194#[cfg(target_has_atomic = "64")]
195declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64);
196
197declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32);
198declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16);
199declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8);
200declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize);
201
202#[cfg(target_has_atomic = "64")]
203declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64);
204
205declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32);
206declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16);
207declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8);
208declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize);
209
210declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool);
211
212declare_atomic_type_generic!(AtomicPtr, PAtomicPtr, PermissionPtr<T>, *mut T, AtomicPredPtr);
213
214#[macro_export]
326macro_rules! atomic_with_ghost {
327 ($($tokens:tt)*) => {
328 ::builtin_macros::atomic_with_ghost_helper!(
331 $crate::vstd::atomic_ghost::atomic_with_ghost_inner,
332 $($tokens)*)
333 }
334}
335
336pub use atomic_with_ghost;
337
338#[doc(hidden)]
339#[macro_export]
340macro_rules! atomic_with_ghost_inner {
341 (load, $e:expr, (), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
342 $crate::vstd::atomic_ghost::atomic_with_ghost_load!($e, $prev, $next, $ret, $g, $b)
343 };
344 (store, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
345 $crate::vstd::atomic_ghost::atomic_with_ghost_store!(
346 $e, $operand, $prev, $next, $ret, $g, $b
347 )
348 };
349 (swap, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
350 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
351 swap, $e, $operand, $prev, $next, $ret, $g, $b
352 )
353 };
354
355 (fetch_or, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
356 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
357 fetch_or, $e, $operand, $prev, $next, $ret, $g, $b
358 )
359 };
360 (fetch_and, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
361 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
362 fetch_and, $e, $operand, $prev, $next, $ret, $g, $b
363 )
364 };
365 (fetch_xor, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
366 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
367 fetch_xor, $e, $operand, $prev, $next, $ret, $g, $b
368 )
369 };
370 (fetch_nand, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
371 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
372 fetch_nand, $e, $operand, $prev, $next, $ret, $g, $b
373 )
374 };
375 (fetch_max, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
376 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
377 fetch_max, $e, $operand, $prev, $next, $ret, $g, $b
378 )
379 };
380 (fetch_min, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
381 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
382 fetch_min, $e, $operand, $prev, $next, $ret, $g, $b
383 )
384 };
385 (fetch_add_wrapping, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
386 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
387 fetch_add_wrapping,
388 $e,
389 $operand,
390 $prev,
391 $next,
392 $ret,
393 $g,
394 $b
395 )
396 };
397 (fetch_sub_wrapping, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
398 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
399 fetch_sub_wrapping,
400 $e,
401 $operand,
402 $prev,
403 $next,
404 $ret,
405 $g,
406 $b
407 )
408 };
409
410 (fetch_add, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
411 $crate::vstd::atomic_ghost::atomic_with_ghost_update_fetch_add!(
412 $e, $operand, $prev, $next, $ret, $g, $b
413 )
414 };
415 (fetch_sub, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
416 $crate::vstd::atomic_ghost::atomic_with_ghost_update_fetch_sub!(
417 $e, $operand, $prev, $next, $ret, $g, $b
418 )
419 };
420
421 (compare_exchange, $e:expr, ($operand1:expr, $operand2:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
422 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_2_operand!(
423 compare_exchange,
424 $e,
425 $operand1,
426 $operand2,
427 $prev,
428 $next,
429 $ret,
430 $g,
431 $b
432 )
433 };
434 (compare_exchange_weak, $e:expr, ($operand1:expr, $operand2:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
435 $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_2_operand!(
436 compare_exchange_weak,
437 $e,
438 $operand1,
439 $operand2,
440 $prev,
441 $next,
442 $ret,
443 $g,
444 $b
445 )
446 };
447 (no_op, $e:expr, (), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
448 $crate::vstd::atomic_ghost::atomic_with_ghost_no_op!($e, $prev, $next, $ret, $g, $b)
449 };
450}
451
452pub use atomic_with_ghost_inner;
453
454#[doc(hidden)]
455#[macro_export]
456macro_rules! atomic_with_ghost_store {
457 ($e:expr, $operand:expr, $prev:pat, $next:pat, $res:pat, $g:ident, $b:block) => {
458 ::builtin_macros::verus_exec_expr! { {
459 let atomic = &($e);
460 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
461 #[allow(unused_mut)]
462 let tracked (mut perm, mut $g) = pair;
463 let ghost $prev = perm.view().value;
464 atomic.patomic.store(Tracked(&mut perm), $operand);
465 let ghost $next = perm.view().value;
466 let ghost $res = ();
467
468 proof { $b }
469
470 proof { pair = (perm, $g); }
471 });
472 } }
473 };
474}
475pub use atomic_with_ghost_store;
476
477#[doc(hidden)]
478#[macro_export]
479macro_rules! atomic_with_ghost_load {
480 ($e:expr, $prev:pat, $next: pat, $res: pat, $g:ident, $b:block) => {
481 ::builtin_macros::verus_exec_expr! { {
482 let result;
483 let atomic = &($e);
484 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
485 #[allow(unused_mut)]
486 let tracked (perm, mut $g) = pair;
487 result = atomic.patomic.load(Tracked(&perm));
488 let ghost $res = result;
489 let ghost $prev = result;
490 let ghost $next = result;
491
492 proof { $b }
493
494 proof { pair = (perm, $g); }
495 });
496 result
497 } }
498 };
499}
500
501pub use atomic_with_ghost_load;
502
503#[doc(hidden)]
504#[macro_export]
505macro_rules! atomic_with_ghost_no_op {
506 ($e:expr, $prev:pat, $next: pat, $res: pat, $g:ident, $b:block) => {
507 ::builtin_macros::verus_exec_expr! { {
508 let atomic = &($e);
509 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
510 #[allow(unused_mut)]
511 let tracked (perm, mut $g) = pair;
512 let ghost result = perm.view().value;
513 let ghost $res = result;
514 let ghost $prev = result;
515 let ghost $next = result;
516
517 proof { $b }
518
519 proof { pair = (perm, $g); }
520 });
521 } }
522 };
523}
524
525pub use atomic_with_ghost_no_op;
526
527#[doc(hidden)]
528#[macro_export]
529macro_rules! atomic_with_ghost_update_with_1_operand {
530 ($name:ident, $e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
531 ::builtin_macros::verus_exec_expr! { {
532 let result;
533 let atomic = &($e);
534 let operand = $operand;
535 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
536 #[allow(unused_mut)]
537 let tracked (mut perm, mut $g) = pair;
538 let ghost $prev = perm.view().value;
539 result = atomic.patomic.$name(Tracked(&mut perm), operand);
540 let ghost $res = result;
541 let ghost $next = perm.view().value;
542
543 proof { $b }
544
545 proof { pair = (perm, $g); }
546 });
547 result
548 } }
549 };
550}
551
552pub use atomic_with_ghost_update_with_1_operand;
553
554#[doc(hidden)]
555#[macro_export]
556macro_rules! atomic_with_ghost_update_with_2_operand {
557 ($name:ident, $e:expr, $operand1:expr, $operand2:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
558 ::builtin_macros::verus_exec_expr! { {
559 let result;
560 let atomic = &($e);
561 let operand1 = $operand1;
562 let operand2 = $operand2;
563 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
564 #[allow(unused_mut)]
565 let tracked (mut perm, mut $g) = pair;
566 let ghost $prev = perm.view().value;
567 result = atomic.patomic.$name(Tracked(&mut perm), operand1, operand2);
568 let ghost $res = result;
569 let ghost $next = perm.view().value;
570
571 proof { $b }
572
573 proof { pair = (perm, $g); }
574 });
575 result
576 } }
577 };
578}
579
580pub use atomic_with_ghost_update_with_2_operand;
581
582#[doc(hidden)]
583#[macro_export]
584macro_rules! atomic_with_ghost_update_fetch_add {
585 ($e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
586 (::builtin_macros::verus_exec_expr!( {
587 let result;
588 let atomic = &($e);
589 let operand = $operand;
590 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
591 #[allow(unused_mut)]
592 let tracked (mut perm, mut $g) = pair;
593
594 proof {
595 let $prev = perm.view().value as int;
596 let $res = perm.view().value as int;
597 let $next = perm.view().value as int + (operand as int);
598
599 { $b }
600 }
601
602 result = atomic.patomic.fetch_add(Tracked(&mut perm), operand);
603
604 proof { pair = (perm, $g); }
605 });
606 result
607 } ))
608 }
609}
610
611pub use atomic_with_ghost_update_fetch_add;
612
613#[doc(hidden)]
614#[macro_export]
615macro_rules! atomic_with_ghost_update_fetch_sub {
616 ($e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
617 ::builtin_macros::verus_exec_expr! { {
618 let result;
619 let atomic = &($e);
620 let operand = $operand;
621 $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
622 #[allow(unused_mut)]
623 let tracked (mut perm, mut $g) = pair;
624
625 proof {
626 let $prev = perm.view().value as int;
627 let $res = perm.view().value as int;
628 let $next = perm.view().value as int - (operand as int);
629
630 { $b }
631 }
632
633 result = atomic.patomic.fetch_sub(Tracked(&mut perm), operand);
634
635 proof { pair = (perm, $g); }
636 });
637 result
638 } }
639 };
640}
641
642pub use atomic_with_ghost_update_fetch_sub;