Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics

• Status: Open
• Tracking Issue: #83
• Start date: 2024/10/30
• End date: 2025/04/10
• Reward: 10,000 USD

Goal

core::sync::atomic 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.

The goal of this challenge is to verify that these methods are safe.¹

Success Criteria

Part 1: Unsafe Methods

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:

• 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 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:

/// `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 types. Concretely, below is the type signature for AtomicPtr::from_ptr:

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

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.

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

Panicking (Optional)

Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with orders 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 orders.

This section is not required to complete the challenge, since panicking is not undefined behavior. However, it would be incorrect for someone to call these functions with the wrong arguments, so we encourage providing these specifications.

Part 3: Atomic Intrinsics

Write safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in core::intrinsics):

List of UBs

In addition to any safety properties mentioned in the API documentation, all proofs must automatically ensure the absence of the following undefined behaviors:

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

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book 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". ↩