Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Atomic Types Challenge #82

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Open

Atomic Types Challenge #82

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
5ea1560
add challenge
carolynzech Sep 9, 2024
232fc37
add link to issue
carolynzech Sep 9, 2024
88263ed
Merge branch 'main' into atomic-challenge
carolynzech Sep 9, 2024
94f10a9
address (some) feedback
carolynzech Sep 13, 2024
2e02a7c
remove intrinsics paragraph
carolynzech Sep 13, 2024
809ba76
part 1 uses methods instead of helpers
carolynzech Sep 14, 2024
3de338c
contracts for unsafe helpers and intrinsics
carolynzech Sep 19, 2024
f4ed75e
address PR feedback
carolynzech Sep 25, 2024
8ff328e
safe abstractions
carolynzech Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions doc/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
126 changes: 126 additions & 0 deletions doc/src/challenges/0007-atomic-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,126 @@
# 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-19*
- **End date:** *2024-12-10*

-------------------

## Goal

(Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior").
carolynzech marked this conversation as resolved.
Show resolved Hide resolved

`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.

The goal of this challenge is to verify that these methods (and the intrinsincs they invoke) are safe.
carolynzech marked this conversation as resolved.
Show resolved Hide resolved

### Success Criteria

#### Part 1: `from_ptr` Method for Atomic Types
carolynzech marked this conversation as resolved.
Show resolved Hide resolved

First, verify that the unsafe `from_ptr` methods are safe.
carolynzech marked this conversation as resolved.
Show resolved Hide resolved

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 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
/// `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 `AtomicPtr` case only, we do not require that you verify safety for all possible values for the type pointed to.
carolynzech marked this conversation as resolved.
Show resolved Hide resolved
Concretely, below is the type signature for `AtomicPtr::from_ptr`:

```rust
pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr<T>
```

The type pointed to is a `*mut T`.
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.

#### Part 2: Unsafe Atomic Functions
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Safe abstractions?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure what this comment means -- are you asking me to change the title, or for something to be added?

Copy link
Author

@carolynzech carolynzech Sep 25, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And/Or are you asking that that this part:

Also write contracts enforcing that the functions are not invoked with orders that would cause them to panic.

Be changed so that the contracts are on the safe abstractions (the methods) instead of the unsafe methods?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For now, I added a new section called "Safe Abstractions" that changes the contracts about panicking to be on the safe methods. LMK if I misinterpreted.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I'll try to be more specific next time. I was adding the comment while waiting to board my flight. ☺️

I meant that this section is named unsafe functions, but the target functions are in fact safe. Instead, this is about verifying the usage of unsafe inside the safe function. Safe functions that invoke unsafe are known as safe abstractions. Let me know if that makes sense

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense. Made some changes.


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`
celinval marked this conversation as resolved.
Show resolved Hide resolved
- `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

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):
carolynzech marked this conversation as resolved.
Show resolved Hide resolved

* Data races.
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that adding data races means that we cannot complete this challenge with Kani. I can take this out if we'd prefer to leave data races out of scope for this challenge. Not sure the feasibility of adding a tool later that can reason about this.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The underlying CBMC supports concurrency, so perhaps Kani can do it?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think in principle we should keep this, since that is the main safety property of many safety guarantees offered by the type.

It's not clear to me what forms these proofs would take.

* 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.

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.
Loading