|
| 1 | +# Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics |
| 2 | + |
| 3 | +- **Status:** Open |
| 4 | +- **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) |
| 5 | +- **Start date:** *2024-10-30* |
| 6 | +- **End date:** *2024-12-10* |
| 7 | + |
| 8 | +------------------- |
| 9 | + |
| 10 | +## Goal |
| 11 | + |
| 12 | +[`core::sync::atomic`](https://doc.rust-lang.org/std/sync/atomic/index.html) provides methods that operate on atomic types. |
| 13 | +For example, `AtomicBool::store(&self, val: bool, order: Ordering)` stores `val` in the atomic boolean referenced by `self` according to the specified [atomic memory ordering](https://doc.rust-lang.org/std/sync/atomic/enum.Ordering.html). |
| 14 | + |
| 15 | +The goal of this challenge is to verify that these methods are safe.[^1] |
| 16 | + |
| 17 | +### Success Criteria |
| 18 | + |
| 19 | +#### Part 1: Unsafe Methods |
| 20 | + |
| 21 | +First, verify that the unsafe `from_ptr` methods are safe, given that their safety preconditions are met. |
| 22 | + |
| 23 | +Write safety contracts for each of the `from_ptr` methods: |
| 24 | + |
| 25 | +- `AtomicBool::from_ptr` |
| 26 | +- `AtomicPtr::from_ptr` |
| 27 | +- `AtomicI8::from_ptr` |
| 28 | +- `AtomicU8::from_ptr` |
| 29 | +- `AtomicI16::from_ptr` |
| 30 | +- `AtomicU16::from_ptr` |
| 31 | +- `AtomicI32::from_ptr` |
| 32 | +- `AtomicU32::from_ptr` |
| 33 | +- `AtomicI64::from_ptr` |
| 34 | +- `AtomicU64::from_ptr` |
| 35 | +- `AtomicI128::from_ptr` |
| 36 | +- `AtomicU128::from_ptr` |
| 37 | + |
| 38 | +Specifically, encode the conditions about `ptr`'s alignment and validity (marked `#Safety` in the methods' documentation) as preconditions. |
| 39 | +Then, verify that the methods are safe for all possible values for the type that `ptr` points to, given that `ptr` satisfies those preconditions. |
| 40 | + |
| 41 | +For example, `AtomicI8::from_ptr` is defined as: |
| 42 | +```rust |
| 43 | +/// `ptr` must be [valid] ... (comment continues; omitted for brevity) |
| 44 | +pub const unsafe fn from_ptr<'a>(ptr: *mut i8) -> &'a AtomicI8 { |
| 45 | + // SAFETY: guaranteed by the caller |
| 46 | + unsafe { &*ptr.cast() } |
| 47 | +} |
| 48 | +``` |
| 49 | + |
| 50 | +To verify this method, first encode the safety comments (e.g., about pointer validity) as preconditions, then verify the absence of undefined behavior for all possible `i8` values. |
| 51 | + |
| 52 | +For the `AtomicPtr` case only, we do not require that you verify safety for all possible types. |
| 53 | +Concretely, below is the type signature for `AtomicPtr::from_ptr`: |
| 54 | + |
| 55 | +```rust |
| 56 | +pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr<T> |
| 57 | +``` |
| 58 | + |
| 59 | +The type pointed to is a `*mut T`. |
| 60 | +Verify that for any arbitrary value for this `*mut T` (i.e., any arbitrary memory address), the method is safe. |
| 61 | +However, you need not verify the method for all possible instantiations of `T`. |
| 62 | +It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. |
| 63 | + |
| 64 | +#### Part 2: Safe Abstractions |
| 65 | + |
| 66 | +The atomic types expose safe abstractions for atomic operations. |
| 67 | +In this part, you will work toward verifying that these abstractions are indeed safe by writing and verifying safety contracts for the unsafe code in their bodies. |
| 68 | + |
| 69 | +For example, `AtomicBool::store` is the (public) safe method that atomically updates the boolean's value. |
| 70 | +This method invokes the unsafe function `atomic_store`, which in turn calls `intrinsics::atomic_store_relaxed`, `intrinsics::atomic_store_release`, or `intrinsics::atomic_store_seqcst`, depending on the provided ordering. |
| 71 | + |
| 72 | +Write and verify safety contracts for the unsafe functions: |
| 73 | + |
| 74 | +- `atomic_store` |
| 75 | +- `atomic_load` |
| 76 | +- `atomic_swap` |
| 77 | +- `atomic_add` |
| 78 | +- `atomic_sub` |
| 79 | +- `atomic_compare_exchange` |
| 80 | +- `atomic_compare_exchange_weak` |
| 81 | +- `atomic_and` |
| 82 | +- `atomic_nand` |
| 83 | +- `atomic_or` |
| 84 | +- `atomic_xor` |
| 85 | +- `atomic_max` |
| 86 | +- `atomic_umax` |
| 87 | +- `atomic_umin` |
| 88 | + |
| 89 | +Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with `order`s that would cause panics. |
| 90 | + |
| 91 | +For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering. |
| 92 | +In this case, you would write contracts on the safe `store` methods that enforce that they are not called with either of those `order`s. |
| 93 | + |
| 94 | +#### Part 3: Atomic Intrinsics |
| 95 | + |
| 96 | +Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`): |
| 97 | + |
| 98 | +| Operations | Functions | |
| 99 | +|-----------------------|-------------| |
| 100 | +| Store | `atomic_store_relaxed`, `atomic_store_release`, `atomic_store_seqcst` | |
| 101 | +| Load | `atomic_load_relaxed`, `atomic_load_acquire`, `atomic_load_seqcst` | |
| 102 | +| Swap | `atomic_xchg_relaxed`, `atomic_xchg_acquire`, `atomic_xchg_release`, `atomic_xchg_acqrel`, `atomic_xchg_seqcst` | |
| 103 | +| Add | `atomic_xadd_relaxed`, `atomic_xadd_acquire`, `atomic_xadd_release`, `atomic_xadd_acqrel`, `atomic_xadd_seqcst` | |
| 104 | +| Sub | `atomic_xsub_relaxed`, `atomic_xsub_acquire`, `atomic_xsub_release`, `atomic_xsub_acqrel`, `atomic_xsub_seqcst` | |
| 105 | +| Compare Exchange | `atomic_cxchg_relaxed_relaxed`, `atomic_cxchg_relaxed_acquire`, `atomic_cxchg_relaxed_seqcst`, `atomic_cxchg_acquire_relaxed`, `atomic_cxchg_acquire_acquire`, `atomic_cxchg_acquire_seqcst`, `atomic_cxchg_release_relaxed`, `atomic_cxchg_release_acquire`, `atomic_cxchg_release_seqcst`, `atomic_cxchg_acqrel_relaxed`, `atomic_cxchg_acqrel_acquire`, `atomic_cxchg_acqrel_seqcst`, `atomic_cxchg_seqcst_relaxed`, `atomic_cxchg_seqcst_acquire`, `atomic_cxchg_seqcst_seqcst` | |
| 106 | +| Compare Exchange Weak | `atomic_cxchgweak_relaxed_relaxed`, `atomic_cxchgweak_relaxed_acquire`, `atomic_cxchgweak_relaxed_seqcst`, `atomic_cxchgweak_acquire_relaxed`, `atomic_cxchgweak_acquire_acquire`, `atomic_cxchgweak_acquire_seqcst`, `atomic_cxchgweak_release_relaxed`, `atomic_cxchgweak_release_acquire`, `atomic_cxchgweak_release_seqcst`, `atomic_cxchgweak_acqrel_relaxed`, `atomic_cxchgweak_acqrel_acquire`, `atomic_cxchgweak_acqrel_seqcst`, `atomic_cxchgweak_seqcst_relaxed`, `atomic_cxchgweak_seqcst_acquire`, `atomic_cxchgweak_seqcst_seqcst` | |
| 107 | +| And | `atomic_and_relaxed`, `atomic_and_acquire`, `atomic_and_release`, `atomic_and_acqrel`, `atomic_and_seqcst` | |
| 108 | +| Nand | `atomic_nand_relaxed`, `atomic_nand_acquire`, `atomic_nand_release`, `atomic_nand_acqrel`, `atomic_nand_seqcst` | |
| 109 | +| Or | `atomic_or_seqcst`, `atomic_or_acquire`, `atomic_or_release`, `atomic_or_acqrel`, `atomic_or_relaxed` | |
| 110 | +| Xor | `atomic_xor_seqcst`, `atomic_xor_acquire`, `atomic_xor_release`, `atomic_xor_acqrel`, `atomic_xor_relaxed` | |
| 111 | +| Max | `atomic_max_relaxed`, `atomic_max_acquire`, `atomic_max_release`, `atomic_max_acqrel`, `atomic_max_seqcst` | |
| 112 | +| Min | `atomic_min_relaxed`, `atomic_min_acquire`, `atomic_min_release`, `atomic_min_acqrel`, `atomic_min_seqcst` | |
| 113 | +| Umax | `atomic_umax_relaxed`, `atomic_umax_acquire`, `atomic_umax_release`, `atomic_umax_acqrel`, `atomic_umax_seqcst` | |
| 114 | +| Umin | `atomic_umin_relaxed`, `atomic_umin_acquire`, `atomic_umin_release`, `atomic_umin_acqrel`, `atomic_umin_seqcst` | |
| 115 | + |
| 116 | +## List of UBs |
| 117 | + |
| 118 | +In addition to any safety properties mentioned in the API documentation, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): |
| 119 | + |
| 120 | +* Data races. |
| 121 | +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. |
| 122 | +* Reading from uninitialized memory. |
| 123 | +* Invoking undefined behavior via compiler intrinsics. |
| 124 | +* Producing an invalid value. |
| 125 | + |
| 126 | +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. |
| 127 | + |
| 128 | +[^1]: Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior". |
0 commit comments