From 5ea1560fcafa49a5c99540b61b4016b95113ef7e Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 9 Sep 2024 14:31:09 -0400 Subject: [PATCH 1/9] add challenge --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0007-atomic-types.md | 83 +++++++++++++++++++++++++ 2 files changed, 84 insertions(+) create mode 100644 doc/src/challenges/0007-atomic-types.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index db5018121be02..3f4134de1a543 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -19,6 +19,7 @@ - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md) - [6: Safety of `NonNull`](./challenges/0006-nonnull.md) + - [7: Safety of Methods for Atomic Types and `ReentrantLock`](./challenges/0007-atomic-types.md) - [8: Contracts for SmallSort](./challenges/0008-smallsort.md) - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - [10: Memory safety of String](./challenges/0010-string.md) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md new file mode 100644 index 0000000000000..a100c8093904d --- /dev/null +++ b/doc/src/challenges/0007-atomic-types.md @@ -0,0 +1,83 @@ +# Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock` + +- **Status:** Open +- **Tracking Issue:** *Link to issue* +- **Start date:** *2024-09-09* +- **End date:** *2024-12-10* + +------------------- + +## Goal + +Verify the safety of: +- The methods for atomic types in `core::sync::atomic` +- The implementation of `ReentrantLock` in `std::sync::reentrant_lock` + +### Success Criteria + + +#### Part 1: Atomic Types + +First, verify the safety of methods on atomic types. + +Write safety contracts for each of the `from_ptr` methods: + +- `AtomicBool::from_ptr` +- `AtomicPtr::from_ptr` +- `AtomicI8::from_ptr` +- `AtomicU8::from_ptr` +- `AtomicI16::from_ptr` +- `AtomicU16::from_ptr` +- `AtomicI32::from_ptr` +- `AtomicU32::from_ptr` +- `AtomicI64::from_ptr` +- `AtomicU64::from_ptr` +- `AtomicI128::from_ptr` +- `AtomicU128::from_ptr` + +Specifically, encode the safety conditions marked `#Safety` in the comments above the methods. + +For the integer and boolean atomics, verify that these contracts hold on all bit-valid values. For `AtomicPtr`, verify that the contracts hold for pointees of size 0, 8, 16, 32, 64, 128, and at least one non-power-of-two. + +Then, write and verify safety contracts for the remaining unsafe functions: + +- `atomic_store` +- `atomic_load` +- `atomic_swap` +- `atomic_add` +- `atomic_sub` +- `atomic_compare_exchange` +- `atomic_compare_exchange_weak` +- `atomic_and` +- `atomic_nand` +- `atomic_or` +- `atomic_xor` +- `atomic_max` +- `atomic_umax` +- `atomic_umin` + +These functions are wrappers around compiler intrinsics. Thus, your task is to ensure that we cannot cause undefined behavior by invoking the intrinsics on these inputs. For instance, if the intrinsic takes as input a raw pointer and reads the value at that pointer, your contracts should ensure that we would not cause UB by performing the read. For the purpose of this challenge, you may assume that any UB in the intrinsics would be a direct consequence of malformed inputs. + +You are not required to write correctness contracts for these functions (e.g., that `atomic_sub` correctly subtracts the operands and stores the result), but it would be great to do so! + +#### Part 2: Reentrant Lock + +Verify that the `ReentrantLock` implementation in `std::sync::reentrant_lock` is safe. In particular, verify: + +* That all uses of the methods on atomic types uphold the safety contracts you wrote in Part 1, and +* No other unsafe code in `ReentrantLock` causes UB or arithmetic overflow. + +## List of UBs + +In addition to any properties called out as SAFETY comments in the source code, 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): + +* Data races. +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Invoking undefined behavior via compiler intrinsics. +* Producing an invalid value. +* Breaking the aliasing or conversion rules of `UnsafeCell` (defined [here](https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html)). + +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. + + From 232fc3710ae7e55ac4d249ee31dcffceef457ef7 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 9 Sep 2024 14:32:51 -0400 Subject: [PATCH 2/9] add link to issue --- doc/src/challenges/0007-atomic-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index a100c8093904d..f232d79cc6887 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -1,7 +1,7 @@ # Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock` - **Status:** Open -- **Tracking Issue:** *Link to issue* +- **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) - **Start date:** *2024-09-09* - **End date:** *2024-12-10* From 94f10a999aa2d5379bae63178aaccd7862110253 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Sep 2024 18:11:17 -0400 Subject: [PATCH 3/9] address (some) feedback --- doc/src/challenges/0007-atomic-types.md | 49 +++++++++++++++++++------ 1 file changed, 38 insertions(+), 11 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index f232d79cc6887..e80fda53d657a 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -9,16 +9,20 @@ ## Goal -Verify the safety of: -- The methods for atomic types in `core::sync::atomic` -- The implementation of `ReentrantLock` in `std::sync::reentrant_lock` +(Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior"). -### Success Criteria +`core::sync::atomic` provides methods that operate on atomic types. +For example, `atomic_store(dst: *mut T, val: T, order: Ordering)` stores `val` at the memory location pointed to by `dst` according to the specified [atomic memory ordering](https://doc.rust-lang.org/std/sync/atomic/enum.Ordering.html). +Rust developers can use these methods to ensure that their concurrent code is thread-safe. +They can also leverage these types to implement other, more complex atomic data structures. + +The goal of this challenge is first to verify that the methods for atomic types are safe, then to verify that the implementation of `ReentrantLock` (which uses atomic types) is safe. +### Success Criteria #### Part 1: Atomic Types -First, verify the safety of methods on atomic types. +First, verify that methods on atomic types (in `core::sync::atomic`) are safe. Write safety contracts for each of the `from_ptr` methods: @@ -35,9 +39,31 @@ Write safety contracts for each of the `from_ptr` methods: - `AtomicI128::from_ptr` - `AtomicU128::from_ptr` -Specifically, encode the safety conditions marked `#Safety` in the comments above the methods. +Specifically, encode the conditions marked `#Safety` in the comments above the methods as preconditions. +Then, verify that the methods are safe for all possible values for the type that `ptr` points to. + +For example, `AtomicI8::from_ptr` is defined as: +```rust +/// `ptr` must be [valid] ... (comment continues; omitted for brevity) +pub const unsafe fn from_ptr<'a>(ptr: *mut i8) -> &'a AtomicI8 { + // SAFETY: guaranteed by the caller + unsafe { &*ptr.cast() } +} +``` + +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. -For the integer and boolean atomics, verify that these contracts hold on all bit-valid values. For `AtomicPtr`, verify that the contracts hold for pointees of size 0, 8, 16, 32, 64, 128, and at least one non-power-of-two. +For the `AtomicPtr` case only, we do not require that you verify safety for all possible values for the type pointed to. +Concretely, below is the type signature for `AtomicPtr::from_ptr`: + +```rust +pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr +``` + +The type pointed to is a `*mut T`. +Verify that for any arbitrary value for this inner pointer (i.e., any arbitrary memory address), the method is safe. +However, you need not verify the method for all possible instantiations of `T`. +It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. Then, write and verify safety contracts for the remaining unsafe functions: @@ -56,7 +82,10 @@ Then, write and verify safety contracts for the remaining unsafe functions: - `atomic_umax` - `atomic_umin` -These functions are wrappers around compiler intrinsics. Thus, your task is to ensure that we cannot cause undefined behavior by invoking the intrinsics on these inputs. For instance, if the intrinsic takes as input a raw pointer and reads the value at that pointer, your contracts should ensure that we would not cause UB by performing the read. For the purpose of this challenge, you may assume that any UB in the intrinsics would be a direct consequence of malformed inputs. +These functions are wrappers around compiler intrinsics. +Thus, your task is to ensure that we cannot cause undefined behavior by invoking the intrinsics on these inputs. +For instance, if the intrinsic takes as input a raw pointer and reads the value at that pointer, your contracts should ensure that we would not cause UB by performing the read. +For the purpose of this challenge, you may assume that any UB in the intrinsics would be a direct consequence of malformed inputs. You are not required to write correctness contracts for these functions (e.g., that `atomic_sub` correctly subtracts the operands and stores the result), but it would be great to do so! @@ -65,7 +94,7 @@ You are not required to write correctness contracts for these functions (e.g., t Verify that the `ReentrantLock` implementation in `std::sync::reentrant_lock` is safe. In particular, verify: * That all uses of the methods on atomic types uphold the safety contracts you wrote in Part 1, and -* No other unsafe code in `ReentrantLock` causes UB or arithmetic overflow. +* No other unsafe code in `ReentrantLock` causes undefined behavior or arithmetic overflow. ## List of UBs @@ -79,5 +108,3 @@ In addition to any properties called out as SAFETY comments in the source code, * Breaking the aliasing or conversion rules of `UnsafeCell` (defined [here](https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html)). 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. - - From 2e02a7c592735da26d65b909cf82a10019348a8b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Sep 2024 18:31:33 -0400 Subject: [PATCH 4/9] remove intrinsics paragraph --- doc/src/challenges/0007-atomic-types.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index e80fda53d657a..5581809f68516 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -82,11 +82,6 @@ Then, write and verify safety contracts for the remaining unsafe functions: - `atomic_umax` - `atomic_umin` -These functions are wrappers around compiler intrinsics. -Thus, your task is to ensure that we cannot cause undefined behavior by invoking the intrinsics on these inputs. -For instance, if the intrinsic takes as input a raw pointer and reads the value at that pointer, your contracts should ensure that we would not cause UB by performing the read. -For the purpose of this challenge, you may assume that any UB in the intrinsics would be a direct consequence of malformed inputs. - You are not required to write correctness contracts for these functions (e.g., that `atomic_sub` correctly subtracts the operands and stores the result), but it would be great to do so! #### Part 2: Reentrant Lock From 809ba7624459511eca7e388bf7b9463d819b0487 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Sep 2024 20:08:25 -0400 Subject: [PATCH 5/9] part 1 uses methods instead of helpers --- doc/src/challenges/0007-atomic-types.md | 48 +++++++++++++++---------- 1 file changed, 30 insertions(+), 18 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index 5581809f68516..1f2add753b2fb 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -65,24 +65,36 @@ Verify that for any arbitrary value for this inner pointer (i.e., any arbitrary However, you need not verify the method for all possible instantiations of `T`. It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. -Then, write and verify safety contracts for the remaining unsafe functions: - -- `atomic_store` -- `atomic_load` -- `atomic_swap` -- `atomic_add` -- `atomic_sub` -- `atomic_compare_exchange` -- `atomic_compare_exchange_weak` -- `atomic_and` -- `atomic_nand` -- `atomic_or` -- `atomic_xor` -- `atomic_max` -- `atomic_umax` -- `atomic_umin` - -You are not required to write correctness contracts for these functions (e.g., that `atomic_sub` correctly subtracts the operands and stores the result), but it would be great to do so! +Then, write and verify safety contracts for the remaining methods that use `unsafe`: + +| Method | Types | +| :--- | :--- +| `from_mut` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `get_mut_slice` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `from_mut_slice` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `load` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `store` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `swap` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `compare_exchange` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `compare_exchange_weak` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_update` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_and` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_xor` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_nand` | `AtomicBool`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128`| +| `fetch_or` | `AtomicBool`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_add` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_sub` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_max` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `fetch_min` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | +| `get_mut` | `AtomicBool`| +| `fetch_not` | `AtomicBool`| +| `fetch_ptr_add` | `AtomicPtr`| +| `fetch_ptr_sub` | `AtomicPtr`| +| `fetch_byte_add` | `AtomicPtr`| +| `fetch_byte_sub` | `AtomicPtr`| +| `fetch_or` | `AtomicPtr`| + +You are not required to write correctness contracts for these functions (e.g., that `AtomicI8::fetch_sub` correctly subtracts the operands and stores the result), but it would be great to do so! #### Part 2: Reentrant Lock From 3de338c2b856682f2fff21ba67a14d2fb2e6afd9 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Sep 2024 16:38:13 -0400 Subject: [PATCH 6/9] contracts for unsafe helpers and intrinsics --- doc/src/challenges/0007-atomic-types.md | 103 +++++++++++++----------- 1 file changed, 56 insertions(+), 47 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index 1f2add753b2fb..deb75f7e25de7 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -1,8 +1,8 @@ -# Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock` +# Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics - **Status:** Open - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) -- **Start date:** *2024-09-09* +- **Start date:** *2024-09-19* - **End date:** *2024-12-10* ------------------- @@ -14,15 +14,14 @@ `core::sync::atomic` provides methods that operate on atomic types. For example, `atomic_store(dst: *mut T, val: T, order: Ordering)` stores `val` at the memory location pointed to by `dst` according to the specified [atomic memory ordering](https://doc.rust-lang.org/std/sync/atomic/enum.Ordering.html). Rust developers can use these methods to ensure that their concurrent code is thread-safe. -They can also leverage these types to implement other, more complex atomic data structures. -The goal of this challenge is first to verify that the methods for atomic types are safe, then to verify that the implementation of `ReentrantLock` (which uses atomic types) is safe. +The goal of this challenge is to verify that these methods (and the intrinsincs they invoke) are safe. ### Success Criteria -#### Part 1: Atomic Types +#### Part 1: `from_ptr` Method for Atomic Types -First, verify that methods on atomic types (in `core::sync::atomic`) are safe. +First, verify that the unsafe `from_ptr` methods are safe. Write safety contracts for each of the `from_ptr` methods: @@ -39,8 +38,8 @@ Write safety contracts for each of the `from_ptr` methods: - `AtomicI128::from_ptr` - `AtomicU128::from_ptr` -Specifically, encode the conditions marked `#Safety` in the comments above the methods as preconditions. -Then, verify that the methods are safe for all possible values for the type that `ptr` points to. +Specifically, encode the conditions about `ptr`'s alignment and validity (marked `#Safety` in the comments above the methods) as preconditions. +Then, verify that the methods are safe for all possible values for the type that `ptr` points to, given that `ptr` satisfies those preconditions. For example, `AtomicI8::from_ptr` is defined as: ```rust @@ -61,47 +60,58 @@ pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr ``` The type pointed to is a `*mut T`. -Verify that for any arbitrary value for this inner pointer (i.e., any arbitrary memory address), the method is safe. +Verify that for any arbitrary value for this `*mut T` (i.e., any arbitrary memory address), the method is safe. However, you need not verify the method for all possible instantiations of `T`. It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. -Then, write and verify safety contracts for the remaining methods that use `unsafe`: - -| Method | Types | -| :--- | :--- -| `from_mut` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `get_mut_slice` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `from_mut_slice` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `load` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `store` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `swap` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `compare_exchange` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `compare_exchange_weak` | `AtomicBool`, `AtomicPtr`, `AtomicI8`,`AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_update` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_and` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_xor` | `AtomicBool`, `AtomicPtr`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_nand` | `AtomicBool`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128`| -| `fetch_or` | `AtomicBool`, `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_add` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_sub` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_max` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `fetch_min` | `AtomicI8`, `AtomicU8`,`AtomicI16`,`AtomicU16` `AtomicI32`, `AtomicU32`, `AtomicI64`, `AtomicU64`, `AtomicI128`,`AtomicU128` | -| `get_mut` | `AtomicBool`| -| `fetch_not` | `AtomicBool`| -| `fetch_ptr_add` | `AtomicPtr`| -| `fetch_ptr_sub` | `AtomicPtr`| -| `fetch_byte_add` | `AtomicPtr`| -| `fetch_byte_sub` | `AtomicPtr`| -| `fetch_or` | `AtomicPtr`| - -You are not required to write correctness contracts for these functions (e.g., that `AtomicI8::fetch_sub` correctly subtracts the operands and stores the result), but it would be great to do so! - -#### Part 2: Reentrant Lock - -Verify that the `ReentrantLock` implementation in `std::sync::reentrant_lock` is safe. In particular, verify: - -* That all uses of the methods on atomic types uphold the safety contracts you wrote in Part 1, and -* No other unsafe code in `ReentrantLock` causes undefined behavior or arithmetic overflow. +#### Part 2: Unsafe Atomic Functions + +The atomic types expose safe methods for atomic operations. +These safe methods call unsafe private helper functions, which in turn invoke atomic instrinsics. +For example, `AtomicBool::store` is the (public) safe method that atomically updates the boolean's value. +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. +In this part, you will write safety contracts for each of the the unsafe helper functions. + +Write and verify safety contracts for the unsafe functions: + +- `atomic_store` +- `atomic_load` +- `atomic_swap` +- `atomic_add` +- `atomic_sub` +- `atomic_compare_exchange` +- `atomic_compare_exchange_weak` +- `atomic_and` +- `atomic_nand` +- `atomic_or` +- `atomic_xor` +- `atomic_max` +- `atomic_umax` +- `atomic_umin` + +Also write contracts enforcing that the functions are not invoked with `order`s that would cause them to panic. + +#### Part 3: Atomic Intrinsics + +Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`): + +| Operations | Functions | +|-----------------------|-------------| +| Store | `atomic_store_relaxed`, `atomic_store_release`, `atomic_store_seqcst` | +| Load | `atomic_load_relaxed`, `atomic_load_acquire`, `atomic_load_seqcst` | +| Swap | `atomic_xchg_relaxed`, `atomic_xchg_acquire`, `atomic_xchg_release`, `atomic_xchg_acqrel`, `atomic_xchg_seqcst` | +| Add | `atomic_xadd_relaxed`, `atomic_xadd_acquire`, `atomic_xadd_release`, `atomic_xadd_acqrel`, `atomic_xadd_seqcst` | +| Sub | `atomic_xsub_relaxed`, `atomic_xsub_acquire`, `atomic_xsub_release`, `atomic_xsub_acqrel`, `atomic_xsub_seqcst` | +| 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` | +| 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` | +| And | `atomic_and_relaxed`, `atomic_and_acquire`, `atomic_and_release`, `atomic_and_acqrel`, `atomic_and_seqcst` | +| Nand | `atomic_nand_relaxed`, `atomic_nand_acquire`, `atomic_nand_release`, `atomic_nand_acqrel`, `atomic_nand_seqcst` | +| Or | `atomic_or_seqcst`, `atomic_or_acquire`, `atomic_or_release`, `atomic_or_acqrel`, `atomic_or_relaxed` | +| Xor | `atomic_xor_seqcst`, `atomic_xor_acquire`, `atomic_xor_release`, `atomic_xor_acqrel`, `atomic_xor_relaxed` | +| Max | `atomic_max_relaxed`, `atomic_max_acquire`, `atomic_max_release`, `atomic_max_acqrel`, `atomic_max_seqcst` | +| Min | `atomic_min_relaxed`, `atomic_min_acquire`, `atomic_min_release`, `atomic_min_acqrel`, `atomic_min_seqcst` | +| Umax | `atomic_umax_relaxed`, `atomic_umax_acquire`, `atomic_umax_release`, `atomic_umax_acqrel`, `atomic_umax_seqcst` | +| Umin | `atomic_umin_relaxed`, `atomic_umin_acquire`, `atomic_umin_release`, `atomic_umin_acqrel`, `atomic_umin_seqcst` | ## List of UBs @@ -112,6 +122,5 @@ In addition to any properties called out as SAFETY comments in the source code, * Reading from uninitialized memory. * Invoking undefined behavior via compiler intrinsics. * Producing an invalid value. -* Breaking the aliasing or conversion rules of `UnsafeCell` (defined [here](https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html)). 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. From f4ed75ee0a9834411dcebfa8f25c64f42922e887 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 25 Sep 2024 15:08:41 -0400 Subject: [PATCH 7/9] address PR feedback --- doc/src/challenges/0007-atomic-types.md | 28 ++++++++++++++----------- 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index deb75f7e25de7..5091e8c04d13a 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -9,19 +9,16 @@ ## Goal -(Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior"). - `core::sync::atomic` provides methods that operate on atomic types. -For example, `atomic_store(dst: *mut T, val: T, order: Ordering)` stores `val` at the memory location pointed to by `dst` according to the specified [atomic memory ordering](https://doc.rust-lang.org/std/sync/atomic/enum.Ordering.html). -Rust developers can use these methods to ensure that their concurrent code is thread-safe. +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). -The goal of this challenge is to verify that these methods (and the intrinsincs they invoke) are safe. +The goal of this challenge is to verify that these methods are safe.[^1] ### Success Criteria -#### Part 1: `from_ptr` Method for Atomic Types +#### Part 1: Unsafe Methods -First, verify that the unsafe `from_ptr` methods are safe. +First, verify that the unsafe `from_ptr` methods are safe, given that their safety preconditions are met. Write safety contracts for each of the `from_ptr` methods: @@ -38,7 +35,7 @@ Write safety contracts for each of the `from_ptr` methods: - `AtomicI128::from_ptr` - `AtomicU128::from_ptr` -Specifically, encode the conditions about `ptr`'s alignment and validity (marked `#Safety` in the comments above the methods) as preconditions. +Specifically, encode the conditions about `ptr`'s alignment and validity (marked `#Safety` in the methods' documentation) as preconditions. Then, verify that the methods are safe for all possible values for the type that `ptr` points to, given that `ptr` satisfies those preconditions. For example, `AtomicI8::from_ptr` is defined as: @@ -52,7 +49,7 @@ pub const unsafe fn from_ptr<'a>(ptr: *mut i8) -> &'a AtomicI8 { 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. -For the `AtomicPtr` case only, we do not require that you verify safety for all possible values for the type pointed to. +For the `AtomicPtr` case only, we do not require that you verify safety for all possible types. Concretely, below is the type signature for `AtomicPtr::from_ptr`: ```rust @@ -89,9 +86,14 @@ Write and verify safety contracts for the unsafe functions: - `atomic_umax` - `atomic_umin` -Also write contracts enforcing that the functions are not invoked with `order`s that would cause them to panic. +#### Part 3: Safe Abstractions + +For each of the safe methods that invoke an unsafe function from Part 2, write contracts that ensure that they are not invoked with `order`s that would cause panics. -#### Part 3: Atomic Intrinsics +For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering. +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. + +#### Part 4: Atomic Intrinsics Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`): @@ -115,7 +117,7 @@ Write and verify safety contracts for the intrinsics invoked by the unsafe funct ## List of UBs -In addition to any properties called out as SAFETY comments in the source code, 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): +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): * Data races. * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. @@ -124,3 +126,5 @@ In addition to any properties called out as SAFETY comments in the source code, * Producing an invalid value. 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. + +[^1]: Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior". \ No newline at end of file From 8ff328e8e2f1cc966840e6dbd19e989ba485eb50 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 25 Sep 2024 17:10:07 -0400 Subject: [PATCH 8/9] safe abstractions --- doc/src/challenges/0007-atomic-types.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index 5091e8c04d13a..c869fcebf40c2 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -61,13 +61,13 @@ Verify that for any arbitrary value for this `*mut T` (i.e., any arbitrary memor However, you need not verify the method for all possible instantiations of `T`. It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. -#### Part 2: Unsafe Atomic Functions +#### Part 2: Safe Abstractions + +The atomic types expose safe abstractions for atomic operations. +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. -The atomic types expose safe methods for atomic operations. -These safe methods call unsafe private helper functions, which in turn invoke atomic instrinsics. For example, `AtomicBool::store` is the (public) safe method that atomically updates the boolean's value. 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. -In this part, you will write safety contracts for each of the the unsafe helper functions. Write and verify safety contracts for the unsafe functions: @@ -86,14 +86,12 @@ Write and verify safety contracts for the unsafe functions: - `atomic_umax` - `atomic_umin` -#### Part 3: Safe Abstractions - -For each of the safe methods that invoke an unsafe function from Part 2, write contracts that ensure that they are not invoked with `order`s that would cause panics. +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. For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering. 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. -#### Part 4: Atomic Intrinsics +#### Part 3: Atomic Intrinsics Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`): From 7ecabf1b417f6b6fe1203c8aea6816860377b0a6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 30 Oct 2024 12:51:45 -0400 Subject: [PATCH 9/9] update date and add link --- doc/src/challenges/0007-atomic-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index c869fcebf40c2..69bff582f7751 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -2,14 +2,14 @@ - **Status:** Open - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) -- **Start date:** *2024-09-19* +- **Start date:** *2024-10-30* - **End date:** *2024-12-10* ------------------- ## Goal -`core::sync::atomic` provides methods that operate on atomic types. +[`core::sync::atomic`](https://doc.rust-lang.org/std/sync/atomic/index.html) provides methods that operate on atomic types. 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). The goal of this challenge is to verify that these methods are safe.[^1]